Step | Hyp | Ref
| Expression |
1 | | poss 4026 |
. . 3
⊢ (A ⊆ B
→ (𝑅 Po B → 𝑅 Po A)) |
2 | | ssel 2933 |
. . . . . . . 8
⊢ (A ⊆ B
→ (x ∈ A →
x ∈
B)) |
3 | | ssel 2933 |
. . . . . . . 8
⊢ (A ⊆ B
→ (y ∈ A →
y ∈
B)) |
4 | | ssel 2933 |
. . . . . . . 8
⊢ (A ⊆ B
→ (z ∈ A →
z ∈
B)) |
5 | 2, 3, 4 | 3anim123d 1213 |
. . . . . . 7
⊢ (A ⊆ B
→ ((x ∈ A ∧ y ∈ A ∧ z ∈ A) →
(x ∈
B ∧
y ∈
B ∧
z ∈
B))) |
6 | 5 | imim1d 69 |
. . . . . 6
⊢ (A ⊆ B
→ (((x ∈ B ∧ y ∈ B ∧ z ∈ B) →
(x𝑅y →
(x𝑅z ∨ z𝑅y))) → ((x
∈ A ∧ y ∈ A ∧ z ∈ A) →
(x𝑅y →
(x𝑅z ∨ z𝑅y))))) |
7 | 6 | 2alimdv 1758 |
. . . . 5
⊢ (A ⊆ B
→ (∀y∀z((x ∈ B ∧ y ∈ B ∧ z ∈ B) →
(x𝑅y →
(x𝑅z ∨ z𝑅y))) → ∀y∀z((x ∈ A ∧ y ∈ A ∧ z ∈ A) → (x𝑅y →
(x𝑅z ∨ z𝑅y))))) |
8 | 7 | alimdv 1756 |
. . . 4
⊢ (A ⊆ B
→ (∀x∀y∀z((x ∈ B ∧ y ∈ B ∧ z ∈ B) →
(x𝑅y →
(x𝑅z ∨ z𝑅y))) → ∀x∀y∀z((x ∈ A ∧ y ∈ A ∧ z ∈ A) → (x𝑅y →
(x𝑅z ∨ z𝑅y))))) |
9 | | r3al 2360 |
. . . 4
⊢ (∀x ∈ B ∀y ∈ B ∀z ∈ B (x𝑅y →
(x𝑅z ∨ z𝑅y)) ↔ ∀x∀y∀z((x ∈ B ∧ y ∈ B ∧ z ∈ B) → (x𝑅y →
(x𝑅z ∨ z𝑅y)))) |
10 | | r3al 2360 |
. . . 4
⊢ (∀x ∈ A ∀y ∈ A ∀z ∈ A (x𝑅y →
(x𝑅z ∨ z𝑅y)) ↔ ∀x∀y∀z((x ∈ A ∧ y ∈ A ∧ z ∈ A) → (x𝑅y →
(x𝑅z ∨ z𝑅y)))) |
11 | 8, 9, 10 | 3imtr4g 194 |
. . 3
⊢ (A ⊆ B
→ (∀x ∈ B ∀y ∈ B ∀z ∈ B (x𝑅y → (x𝑅z ∨ z𝑅y))
→ ∀x ∈ A ∀y ∈ A ∀z ∈ A (x𝑅y → (x𝑅z ∨ z𝑅y)))) |
12 | 1, 11 | anim12d 318 |
. 2
⊢ (A ⊆ B
→ ((𝑅 Po B ∧ ∀x ∈ B ∀y ∈ B ∀z ∈ B (x𝑅y →
(x𝑅z ∨ z𝑅y))) → (𝑅 Po A
∧ ∀x ∈ A ∀y ∈ A ∀z ∈ A (x𝑅y →
(x𝑅z ∨ z𝑅y))))) |
13 | | df-iso 4025 |
. 2
⊢ (𝑅 Or B ↔ (𝑅 Po B
∧ ∀x ∈ B ∀y ∈ B ∀z ∈ B (x𝑅y →
(x𝑅z ∨ z𝑅y)))) |
14 | | df-iso 4025 |
. 2
⊢ (𝑅 Or A ↔ (𝑅 Po A
∧ ∀x ∈ A ∀y ∈ A ∀z ∈ A (x𝑅y →
(x𝑅z ∨ z𝑅y)))) |
15 | 12, 13, 14 | 3imtr4g 194 |
1
⊢ (A ⊆ B
→ (𝑅 Or B → 𝑅 Or A)) |