| Step | Hyp | Ref
| Expression |
| 1 | | df-so 5593 |
. 2
⊢ (𝑅 Or 𝐴 ↔ (𝑅 Po 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥))) |
| 2 | | opelxp 5721 |
. . . . . 6
⊢
(〈𝑥, 𝑦〉 ∈ (𝐴 × 𝐴) ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) |
| 3 | | brun 5194 |
. . . . . . . . . 10
⊢ (𝑥( I ∪ ◡𝑅)𝑦 ↔ (𝑥 I 𝑦 ∨ 𝑥◡𝑅𝑦)) |
| 4 | | vex 3484 |
. . . . . . . . . . . 12
⊢ 𝑦 ∈ V |
| 5 | 4 | ideq 5863 |
. . . . . . . . . . 11
⊢ (𝑥 I 𝑦 ↔ 𝑥 = 𝑦) |
| 6 | | vex 3484 |
. . . . . . . . . . . 12
⊢ 𝑥 ∈ V |
| 7 | 6, 4 | brcnv 5893 |
. . . . . . . . . . 11
⊢ (𝑥◡𝑅𝑦 ↔ 𝑦𝑅𝑥) |
| 8 | 5, 7 | orbi12i 915 |
. . . . . . . . . 10
⊢ ((𝑥 I 𝑦 ∨ 𝑥◡𝑅𝑦) ↔ (𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)) |
| 9 | 3, 8 | bitr2i 276 |
. . . . . . . . 9
⊢ ((𝑥 = 𝑦 ∨ 𝑦𝑅𝑥) ↔ 𝑥( I ∪ ◡𝑅)𝑦) |
| 10 | 9 | orbi2i 913 |
. . . . . . . 8
⊢ ((𝑥𝑅𝑦 ∨ (𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)) ↔ (𝑥𝑅𝑦 ∨ 𝑥( I ∪ ◡𝑅)𝑦)) |
| 11 | | 3orass 1090 |
. . . . . . . 8
⊢ ((𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥) ↔ (𝑥𝑅𝑦 ∨ (𝑥 = 𝑦 ∨ 𝑦𝑅𝑥))) |
| 12 | | brun 5194 |
. . . . . . . 8
⊢ (𝑥(𝑅 ∪ ( I ∪ ◡𝑅))𝑦 ↔ (𝑥𝑅𝑦 ∨ 𝑥( I ∪ ◡𝑅)𝑦)) |
| 13 | 10, 11, 12 | 3bitr4i 303 |
. . . . . . 7
⊢ ((𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥) ↔ 𝑥(𝑅 ∪ ( I ∪ ◡𝑅))𝑦) |
| 14 | | df-br 5144 |
. . . . . . 7
⊢ (𝑥(𝑅 ∪ ( I ∪ ◡𝑅))𝑦 ↔ 〈𝑥, 𝑦〉 ∈ (𝑅 ∪ ( I ∪ ◡𝑅))) |
| 15 | 13, 14 | bitr2i 276 |
. . . . . 6
⊢
(〈𝑥, 𝑦〉 ∈ (𝑅 ∪ ( I ∪ ◡𝑅)) ↔ (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)) |
| 16 | 2, 15 | imbi12i 350 |
. . . . 5
⊢
((〈𝑥, 𝑦〉 ∈ (𝐴 × 𝐴) → 〈𝑥, 𝑦〉 ∈ (𝑅 ∪ ( I ∪ ◡𝑅))) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥))) |
| 17 | 16 | 2albii 1820 |
. . . 4
⊢
(∀𝑥∀𝑦(〈𝑥, 𝑦〉 ∈ (𝐴 × 𝐴) → 〈𝑥, 𝑦〉 ∈ (𝑅 ∪ ( I ∪ ◡𝑅))) ↔ ∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥))) |
| 18 | | relxp 5703 |
. . . . 5
⊢ Rel
(𝐴 × 𝐴) |
| 19 | | ssrel 5792 |
. . . . 5
⊢ (Rel
(𝐴 × 𝐴) → ((𝐴 × 𝐴) ⊆ (𝑅 ∪ ( I ∪ ◡𝑅)) ↔ ∀𝑥∀𝑦(〈𝑥, 𝑦〉 ∈ (𝐴 × 𝐴) → 〈𝑥, 𝑦〉 ∈ (𝑅 ∪ ( I ∪ ◡𝑅))))) |
| 20 | 18, 19 | ax-mp 5 |
. . . 4
⊢ ((𝐴 × 𝐴) ⊆ (𝑅 ∪ ( I ∪ ◡𝑅)) ↔ ∀𝑥∀𝑦(〈𝑥, 𝑦〉 ∈ (𝐴 × 𝐴) → 〈𝑥, 𝑦〉 ∈ (𝑅 ∪ ( I ∪ ◡𝑅)))) |
| 21 | | r2al 3195 |
. . . 4
⊢
(∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥) ↔ ∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥))) |
| 22 | 17, 20, 21 | 3bitr4i 303 |
. . 3
⊢ ((𝐴 × 𝐴) ⊆ (𝑅 ∪ ( I ∪ ◡𝑅)) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)) |
| 23 | 22 | anbi2i 623 |
. 2
⊢ ((𝑅 Po 𝐴 ∧ (𝐴 × 𝐴) ⊆ (𝑅 ∪ ( I ∪ ◡𝑅))) ↔ (𝑅 Po 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥))) |
| 24 | 1, 23 | bitr4i 278 |
1
⊢ (𝑅 Or 𝐴 ↔ (𝑅 Po 𝐴 ∧ (𝐴 × 𝐴) ⊆ (𝑅 ∪ ( I ∪ ◡𝑅)))) |