Step | Hyp | Ref
| Expression |
1 | | cnvpom 4803 |
. . 3
⊢ (∃x x ∈ A → (𝑅 Po A
↔ ◡𝑅 Po A)) |
2 | | vex 2554 |
. . . . . . . . 9
⊢ y ∈
V |
3 | | vex 2554 |
. . . . . . . . 9
⊢ x ∈
V |
4 | 2, 3 | brcnv 4461 |
. . . . . . . 8
⊢ (y◡𝑅x ↔ x𝑅y) |
5 | | vex 2554 |
. . . . . . . . . . 11
⊢ z ∈
V |
6 | 2, 5 | brcnv 4461 |
. . . . . . . . . 10
⊢ (y◡𝑅z ↔ z𝑅y) |
7 | 5, 3 | brcnv 4461 |
. . . . . . . . . 10
⊢ (z◡𝑅x ↔ x𝑅z) |
8 | 6, 7 | orbi12i 680 |
. . . . . . . . 9
⊢
((y◡𝑅z ∨ z◡𝑅x)
↔ (z𝑅y ∨ x𝑅z)) |
9 | | orcom 646 |
. . . . . . . . 9
⊢
((z𝑅y ∨ x𝑅z) ↔ (x𝑅z ∨ z𝑅y)) |
10 | 8, 9 | bitri 173 |
. . . . . . . 8
⊢
((y◡𝑅z ∨ z◡𝑅x)
↔ (x𝑅z ∨ z𝑅y)) |
11 | 4, 10 | imbi12i 228 |
. . . . . . 7
⊢
((y◡𝑅x →
(y◡𝑅z ∨ z◡𝑅x))
↔ (x𝑅y →
(x𝑅z ∨ z𝑅y))) |
12 | 11 | ralbii 2324 |
. . . . . 6
⊢ (∀z ∈ A (y◡𝑅x → (y◡𝑅z ∨ z◡𝑅x))
↔ ∀z ∈ A (x𝑅y → (x𝑅z ∨ z𝑅y))) |
13 | 12 | 2ralbii 2326 |
. . . . 5
⊢ (∀x ∈ A ∀y ∈ A ∀z ∈ A (y◡𝑅x → (y◡𝑅z ∨ z◡𝑅x))
↔ ∀x ∈ A ∀y ∈ A ∀z ∈ A (x𝑅y → (x𝑅z ∨ z𝑅y))) |
14 | | ralcom 2467 |
. . . . 5
⊢ (∀x ∈ A ∀y ∈ A ∀z ∈ A (y◡𝑅x → (y◡𝑅z ∨ z◡𝑅x))
↔ ∀y ∈ A ∀x ∈ A ∀z ∈ A (y◡𝑅x →
(y◡𝑅z ∨ z◡𝑅x))) |
15 | 13, 14 | bitr3i 175 |
. . . 4
⊢ (∀x ∈ A ∀y ∈ A ∀z ∈ A (x𝑅y →
(x𝑅z ∨ z𝑅y)) ↔ ∀y ∈ A ∀x ∈ A ∀z ∈ A (y◡𝑅x → (y◡𝑅z ∨ z◡𝑅x))) |
16 | 15 | a1i 9 |
. . 3
⊢ (∃x x ∈ A → (∀x ∈ A ∀y ∈ A ∀z ∈ A (x𝑅y →
(x𝑅z ∨ z𝑅y)) ↔ ∀y ∈ A ∀x ∈ A ∀z ∈ A (y◡𝑅x → (y◡𝑅z ∨ z◡𝑅x)))) |
17 | 1, 16 | anbi12d 442 |
. 2
⊢ (∃x x ∈ A → ((𝑅 Po A
∧ ∀x ∈ A ∀y ∈ A ∀z ∈ A (x𝑅y →
(x𝑅z ∨ z𝑅y))) ↔ (◡𝑅 Po A
∧ ∀y ∈ A ∀x ∈ A ∀z ∈ A (y◡𝑅x → (y◡𝑅z ∨ z◡𝑅x))))) |
18 | | df-iso 4025 |
. 2
⊢ (𝑅 Or A ↔ (𝑅 Po A
∧ ∀x ∈ A ∀y ∈ A ∀z ∈ A (x𝑅y →
(x𝑅z ∨ z𝑅y)))) |
19 | | df-iso 4025 |
. 2
⊢ (◡𝑅 Or A
↔ (◡𝑅 Po A
∧ ∀y ∈ A ∀x ∈ A ∀z ∈ A (y◡𝑅x → (y◡𝑅z ∨ z◡𝑅x)))) |
20 | 17, 18, 19 | 3bitr4g 212 |
1
⊢ (∃x x ∈ A → (𝑅 Or A
↔ ◡𝑅 Or A)) |