Step | Hyp | Ref
| Expression |
1 | | sopo 4976 |
. . 3
⊢ (𝑅 Or 𝐴 → 𝑅 Po 𝐴) |
2 | | pocnv 30907 |
. . 3
⊢ (𝑅 Po 𝐴 → ◡𝑅 Po 𝐴) |
3 | 1, 2 | syl 17 |
. 2
⊢ (𝑅 Or 𝐴 → ◡𝑅 Po 𝐴) |
4 | | solin 4982 |
. . 3
⊢ ((𝑅 Or 𝐴 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)) |
5 | | vex 3176 |
. . . . . 6
⊢ 𝑥 ∈ V |
6 | | vex 3176 |
. . . . . 6
⊢ 𝑦 ∈ V |
7 | 5, 6 | brcnv 5227 |
. . . . 5
⊢ (𝑥◡𝑅𝑦 ↔ 𝑦𝑅𝑥) |
8 | | biid 250 |
. . . . 5
⊢ (𝑥 = 𝑦 ↔ 𝑥 = 𝑦) |
9 | 6, 5 | brcnv 5227 |
. . . . 5
⊢ (𝑦◡𝑅𝑥 ↔ 𝑥𝑅𝑦) |
10 | 7, 8, 9 | 3orbi123i 1245 |
. . . 4
⊢ ((𝑥◡𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦◡𝑅𝑥) ↔ (𝑦𝑅𝑥 ∨ 𝑥 = 𝑦 ∨ 𝑥𝑅𝑦)) |
11 | | orcom 401 |
. . . . . 6
⊢ ((𝑦𝑅𝑥 ∨ 𝑥𝑅𝑦) ↔ (𝑥𝑅𝑦 ∨ 𝑦𝑅𝑥)) |
12 | 11 | orbi2i 540 |
. . . . 5
⊢ ((𝑥 = 𝑦 ∨ (𝑦𝑅𝑥 ∨ 𝑥𝑅𝑦)) ↔ (𝑥 = 𝑦 ∨ (𝑥𝑅𝑦 ∨ 𝑦𝑅𝑥))) |
13 | | 3orass 1034 |
. . . . . 6
⊢ ((𝑦𝑅𝑥 ∨ 𝑥 = 𝑦 ∨ 𝑥𝑅𝑦) ↔ (𝑦𝑅𝑥 ∨ (𝑥 = 𝑦 ∨ 𝑥𝑅𝑦))) |
14 | | or12 544 |
. . . . . 6
⊢ ((𝑦𝑅𝑥 ∨ (𝑥 = 𝑦 ∨ 𝑥𝑅𝑦)) ↔ (𝑥 = 𝑦 ∨ (𝑦𝑅𝑥 ∨ 𝑥𝑅𝑦))) |
15 | 13, 14 | bitri 263 |
. . . . 5
⊢ ((𝑦𝑅𝑥 ∨ 𝑥 = 𝑦 ∨ 𝑥𝑅𝑦) ↔ (𝑥 = 𝑦 ∨ (𝑦𝑅𝑥 ∨ 𝑥𝑅𝑦))) |
16 | | 3orass 1034 |
. . . . . 6
⊢ ((𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥) ↔ (𝑥𝑅𝑦 ∨ (𝑥 = 𝑦 ∨ 𝑦𝑅𝑥))) |
17 | | or12 544 |
. . . . . 6
⊢ ((𝑥𝑅𝑦 ∨ (𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)) ↔ (𝑥 = 𝑦 ∨ (𝑥𝑅𝑦 ∨ 𝑦𝑅𝑥))) |
18 | 16, 17 | bitri 263 |
. . . . 5
⊢ ((𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥) ↔ (𝑥 = 𝑦 ∨ (𝑥𝑅𝑦 ∨ 𝑦𝑅𝑥))) |
19 | 12, 15, 18 | 3bitr4i 291 |
. . . 4
⊢ ((𝑦𝑅𝑥 ∨ 𝑥 = 𝑦 ∨ 𝑥𝑅𝑦) ↔ (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)) |
20 | 10, 19 | bitri 263 |
. . 3
⊢ ((𝑥◡𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦◡𝑅𝑥) ↔ (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)) |
21 | 4, 20 | sylibr 223 |
. 2
⊢ ((𝑅 Or 𝐴 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → (𝑥◡𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦◡𝑅𝑥)) |
22 | 3, 21 | issod 4989 |
1
⊢ (𝑅 Or 𝐴 → ◡𝑅 Or 𝐴) |