Step | Hyp | Ref
| Expression |
1 | | df-so 5500 |
. 2
⊢ (𝑅 Or 𝐴 ↔ (𝑅 Po 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥))) |
2 | | opelxp 5621 |
. . . . . 6
⊢
(〈𝑥, 𝑦〉 ∈ (𝐴 × 𝐴) ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) |
3 | | brun 5125 |
. . . . . . . . . 10
⊢ (𝑥( I ∪ ◡𝑅)𝑦 ↔ (𝑥 I 𝑦 ∨ 𝑥◡𝑅𝑦)) |
4 | | vex 3434 |
. . . . . . . . . . . 12
⊢ 𝑦 ∈ V |
5 | 4 | ideq 5755 |
. . . . . . . . . . 11
⊢ (𝑥 I 𝑦 ↔ 𝑥 = 𝑦) |
6 | | vex 3434 |
. . . . . . . . . . . 12
⊢ 𝑥 ∈ V |
7 | 6, 4 | brcnv 5785 |
. . . . . . . . . . 11
⊢ (𝑥◡𝑅𝑦 ↔ 𝑦𝑅𝑥) |
8 | 5, 7 | orbi12i 912 |
. . . . . . . . . 10
⊢ ((𝑥 I 𝑦 ∨ 𝑥◡𝑅𝑦) ↔ (𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)) |
9 | 3, 8 | bitr2i 275 |
. . . . . . . . 9
⊢ ((𝑥 = 𝑦 ∨ 𝑦𝑅𝑥) ↔ 𝑥( I ∪ ◡𝑅)𝑦) |
10 | 9 | orbi2i 910 |
. . . . . . . 8
⊢ ((𝑥𝑅𝑦 ∨ (𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)) ↔ (𝑥𝑅𝑦 ∨ 𝑥( I ∪ ◡𝑅)𝑦)) |
11 | | 3orass 1089 |
. . . . . . . 8
⊢ ((𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥) ↔ (𝑥𝑅𝑦 ∨ (𝑥 = 𝑦 ∨ 𝑦𝑅𝑥))) |
12 | | brun 5125 |
. . . . . . . 8
⊢ (𝑥(𝑅 ∪ ( I ∪ ◡𝑅))𝑦 ↔ (𝑥𝑅𝑦 ∨ 𝑥( I ∪ ◡𝑅)𝑦)) |
13 | 10, 11, 12 | 3bitr4i 303 |
. . . . . . 7
⊢ ((𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥) ↔ 𝑥(𝑅 ∪ ( I ∪ ◡𝑅))𝑦) |
14 | | df-br 5075 |
. . . . . . 7
⊢ (𝑥(𝑅 ∪ ( I ∪ ◡𝑅))𝑦 ↔ 〈𝑥, 𝑦〉 ∈ (𝑅 ∪ ( I ∪ ◡𝑅))) |
15 | 13, 14 | bitr2i 275 |
. . . . . 6
⊢
(〈𝑥, 𝑦〉 ∈ (𝑅 ∪ ( I ∪ ◡𝑅)) ↔ (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)) |
16 | 2, 15 | imbi12i 351 |
. . . . 5
⊢
((〈𝑥, 𝑦〉 ∈ (𝐴 × 𝐴) → 〈𝑥, 𝑦〉 ∈ (𝑅 ∪ ( I ∪ ◡𝑅))) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥))) |
17 | 16 | 2albii 1823 |
. . . 4
⊢
(∀𝑥∀𝑦(〈𝑥, 𝑦〉 ∈ (𝐴 × 𝐴) → 〈𝑥, 𝑦〉 ∈ (𝑅 ∪ ( I ∪ ◡𝑅))) ↔ ∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥))) |
18 | | relxp 5603 |
. . . . 5
⊢ Rel
(𝐴 × 𝐴) |
19 | | ssrel 5688 |
. . . . 5
⊢ (Rel
(𝐴 × 𝐴) → ((𝐴 × 𝐴) ⊆ (𝑅 ∪ ( I ∪ ◡𝑅)) ↔ ∀𝑥∀𝑦(〈𝑥, 𝑦〉 ∈ (𝐴 × 𝐴) → 〈𝑥, 𝑦〉 ∈ (𝑅 ∪ ( I ∪ ◡𝑅))))) |
20 | 18, 19 | ax-mp 5 |
. . . 4
⊢ ((𝐴 × 𝐴) ⊆ (𝑅 ∪ ( I ∪ ◡𝑅)) ↔ ∀𝑥∀𝑦(〈𝑥, 𝑦〉 ∈ (𝐴 × 𝐴) → 〈𝑥, 𝑦〉 ∈ (𝑅 ∪ ( I ∪ ◡𝑅)))) |
21 | | r2al 3125 |
. . . 4
⊢
(∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥) ↔ ∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥))) |
22 | 17, 20, 21 | 3bitr4i 303 |
. . 3
⊢ ((𝐴 × 𝐴) ⊆ (𝑅 ∪ ( I ∪ ◡𝑅)) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)) |
23 | 22 | anbi2i 623 |
. 2
⊢ ((𝑅 Po 𝐴 ∧ (𝐴 × 𝐴) ⊆ (𝑅 ∪ ( I ∪ ◡𝑅))) ↔ (𝑅 Po 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥))) |
24 | 1, 23 | bitr4i 277 |
1
⊢ (𝑅 Or 𝐴 ↔ (𝑅 Po 𝐴 ∧ (𝐴 × 𝐴) ⊆ (𝑅 ∪ ( I ∪ ◡𝑅)))) |