Step | Hyp | Ref
| Expression |
1 | | ssralv 2998 |
. . 3
⊢ (A ⊆ B
→ (∀x ∈ B ∀y ∈ B ∀z ∈ B (¬ x𝑅x ∧ ((x𝑅y ∧ y𝑅z) → x𝑅z)) → ∀x ∈ A ∀y ∈ B ∀z ∈ B (¬
x𝑅x ∧ ((x𝑅y ∧ y𝑅z)
→ x𝑅z)))) |
2 | | ssralv 2998 |
. . . . 5
⊢ (A ⊆ B
→ (∀y ∈ B ∀z ∈ B (¬ x𝑅x ∧ ((x𝑅y ∧ y𝑅z) → x𝑅z)) → ∀y ∈ A ∀z ∈ B (¬
x𝑅x ∧ ((x𝑅y ∧ y𝑅z)
→ x𝑅z)))) |
3 | | ssralv 2998 |
. . . . . 6
⊢ (A ⊆ B
→ (∀z ∈ B (¬ x𝑅x ∧ ((x𝑅y ∧ y𝑅z) → x𝑅z)) → ∀z ∈ A (¬
x𝑅x ∧ ((x𝑅y ∧ y𝑅z)
→ x𝑅z)))) |
4 | 3 | ralimdv 2382 |
. . . . 5
⊢ (A ⊆ B
→ (∀y ∈ A ∀z ∈ B (¬ x𝑅x ∧ ((x𝑅y ∧ y𝑅z) → x𝑅z)) → ∀y ∈ A ∀z ∈ A (¬
x𝑅x ∧ ((x𝑅y ∧ y𝑅z)
→ x𝑅z)))) |
5 | 2, 4 | syld 40 |
. . . 4
⊢ (A ⊆ B
→ (∀y ∈ B ∀z ∈ B (¬ x𝑅x ∧ ((x𝑅y ∧ y𝑅z) → x𝑅z)) → ∀y ∈ A ∀z ∈ A (¬
x𝑅x ∧ ((x𝑅y ∧ y𝑅z)
→ x𝑅z)))) |
6 | 5 | ralimdv 2382 |
. . 3
⊢ (A ⊆ B
→ (∀x ∈ A ∀y ∈ B ∀z ∈ B (¬ x𝑅x ∧ ((x𝑅y ∧ y𝑅z) → x𝑅z)) → ∀x ∈ A ∀y ∈ A ∀z ∈ A (¬
x𝑅x ∧ ((x𝑅y ∧ y𝑅z)
→ x𝑅z)))) |
7 | 1, 6 | syld 40 |
. 2
⊢ (A ⊆ B
→ (∀x ∈ B ∀y ∈ B ∀z ∈ B (¬ x𝑅x ∧ ((x𝑅y ∧ y𝑅z) → x𝑅z)) → ∀x ∈ A ∀y ∈ A ∀z ∈ A (¬
x𝑅x ∧ ((x𝑅y ∧ y𝑅z)
→ x𝑅z)))) |
8 | | df-po 4024 |
. 2
⊢ (𝑅 Po B ↔ ∀x ∈ B ∀y ∈ B ∀z ∈ B (¬
x𝑅x ∧ ((x𝑅y ∧ y𝑅z)
→ x𝑅z))) |
9 | | df-po 4024 |
. 2
⊢ (𝑅 Po A ↔ ∀x ∈ A ∀y ∈ A ∀z ∈ A (¬
x𝑅x ∧ ((x𝑅y ∧ y𝑅z)
→ x𝑅z))) |
10 | 7, 8, 9 | 3imtr4g 194 |
1
⊢ (A ⊆ B
→ (𝑅 Po B → 𝑅 Po A)) |