Proof of Theorem asymref2
Step | Hyp | Ref
| Expression |
1 | | asymref 6021 |
. 2
⊢ ((𝑅 ∩ ◡𝑅) = ( I ↾ ∪
∪ 𝑅) ↔ ∀𝑥 ∈ ∪ ∪ 𝑅∀𝑦((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥) ↔ 𝑥 = 𝑦)) |
2 | | albiim 1892 |
. . 3
⊢
(∀𝑦((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥) ↔ 𝑥 = 𝑦) ↔ (∀𝑦((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥) → 𝑥 = 𝑦) ∧ ∀𝑦(𝑥 = 𝑦 → (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥)))) |
3 | 2 | ralbii 3092 |
. 2
⊢
(∀𝑥 ∈
∪ ∪ 𝑅∀𝑦((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥) ↔ 𝑥 = 𝑦) ↔ ∀𝑥 ∈ ∪ ∪ 𝑅(∀𝑦((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥) → 𝑥 = 𝑦) ∧ ∀𝑦(𝑥 = 𝑦 → (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥)))) |
4 | | r19.26 3095 |
. . 3
⊢
(∀𝑥 ∈
∪ ∪ 𝑅(∀𝑦((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥) → 𝑥 = 𝑦) ∧ ∀𝑦(𝑥 = 𝑦 → (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥))) ↔ (∀𝑥 ∈ ∪ ∪ 𝑅∀𝑦((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥) → 𝑥 = 𝑦) ∧ ∀𝑥 ∈ ∪ ∪ 𝑅∀𝑦(𝑥 = 𝑦 → (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥)))) |
5 | | ancom 461 |
. . 3
⊢
((∀𝑥 ∈
∪ ∪ 𝑅∀𝑦((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥) → 𝑥 = 𝑦) ∧ ∀𝑥 ∈ ∪ ∪ 𝑅∀𝑦(𝑥 = 𝑦 → (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥))) ↔ (∀𝑥 ∈ ∪ ∪ 𝑅∀𝑦(𝑥 = 𝑦 → (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥)) ∧ ∀𝑥 ∈ ∪ ∪ 𝑅∀𝑦((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥) → 𝑥 = 𝑦))) |
6 | | equcom 2021 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 ↔ 𝑦 = 𝑥) |
7 | 6 | imbi1i 350 |
. . . . . . 7
⊢ ((𝑥 = 𝑦 → (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥)) ↔ (𝑦 = 𝑥 → (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥))) |
8 | 7 | albii 1822 |
. . . . . 6
⊢
(∀𝑦(𝑥 = 𝑦 → (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥)) ↔ ∀𝑦(𝑦 = 𝑥 → (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥))) |
9 | | breq2 5078 |
. . . . . . . . 9
⊢ (𝑦 = 𝑥 → (𝑥𝑅𝑦 ↔ 𝑥𝑅𝑥)) |
10 | | breq1 5077 |
. . . . . . . . 9
⊢ (𝑦 = 𝑥 → (𝑦𝑅𝑥 ↔ 𝑥𝑅𝑥)) |
11 | 9, 10 | anbi12d 631 |
. . . . . . . 8
⊢ (𝑦 = 𝑥 → ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥) ↔ (𝑥𝑅𝑥 ∧ 𝑥𝑅𝑥))) |
12 | | anidm 565 |
. . . . . . . 8
⊢ ((𝑥𝑅𝑥 ∧ 𝑥𝑅𝑥) ↔ 𝑥𝑅𝑥) |
13 | 11, 12 | bitrdi 287 |
. . . . . . 7
⊢ (𝑦 = 𝑥 → ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥) ↔ 𝑥𝑅𝑥)) |
14 | 13 | equsalvw 2007 |
. . . . . 6
⊢
(∀𝑦(𝑦 = 𝑥 → (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥)) ↔ 𝑥𝑅𝑥) |
15 | 8, 14 | bitri 274 |
. . . . 5
⊢
(∀𝑦(𝑥 = 𝑦 → (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥)) ↔ 𝑥𝑅𝑥) |
16 | 15 | ralbii 3092 |
. . . 4
⊢
(∀𝑥 ∈
∪ ∪ 𝑅∀𝑦(𝑥 = 𝑦 → (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥)) ↔ ∀𝑥 ∈ ∪ ∪ 𝑅𝑥𝑅𝑥) |
17 | | df-ral 3069 |
. . . . 5
⊢
(∀𝑥 ∈
∪ ∪ 𝑅∀𝑦((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥) → 𝑥 = 𝑦) ↔ ∀𝑥(𝑥 ∈ ∪ ∪ 𝑅
→ ∀𝑦((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥) → 𝑥 = 𝑦))) |
18 | | df-br 5075 |
. . . . . . . . . . . . 13
⊢ (𝑥𝑅𝑦 ↔ 〈𝑥, 𝑦〉 ∈ 𝑅) |
19 | | vex 3436 |
. . . . . . . . . . . . . . 15
⊢ 𝑥 ∈ V |
20 | | vex 3436 |
. . . . . . . . . . . . . . 15
⊢ 𝑦 ∈ V |
21 | 19, 20 | opeluu 5385 |
. . . . . . . . . . . . . 14
⊢
(〈𝑥, 𝑦〉 ∈ 𝑅 → (𝑥 ∈ ∪ ∪ 𝑅
∧ 𝑦 ∈ ∪ ∪ 𝑅)) |
22 | 21 | simpld 495 |
. . . . . . . . . . . . 13
⊢
(〈𝑥, 𝑦〉 ∈ 𝑅 → 𝑥 ∈ ∪ ∪ 𝑅) |
23 | 18, 22 | sylbi 216 |
. . . . . . . . . . . 12
⊢ (𝑥𝑅𝑦 → 𝑥 ∈ ∪ ∪ 𝑅) |
24 | 23 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥) → 𝑥 ∈ ∪ ∪ 𝑅) |
25 | 24 | pm2.24d 151 |
. . . . . . . . . 10
⊢ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥) → (¬ 𝑥 ∈ ∪ ∪ 𝑅
→ 𝑥 = 𝑦)) |
26 | 25 | com12 32 |
. . . . . . . . 9
⊢ (¬
𝑥 ∈ ∪ ∪ 𝑅 → ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥) → 𝑥 = 𝑦)) |
27 | 26 | alrimiv 1930 |
. . . . . . . 8
⊢ (¬
𝑥 ∈ ∪ ∪ 𝑅 → ∀𝑦((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥) → 𝑥 = 𝑦)) |
28 | | id 22 |
. . . . . . . 8
⊢
(∀𝑦((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥) → 𝑥 = 𝑦) → ∀𝑦((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥) → 𝑥 = 𝑦)) |
29 | 27, 28 | ja 186 |
. . . . . . 7
⊢ ((𝑥 ∈ ∪ ∪ 𝑅 → ∀𝑦((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥) → 𝑥 = 𝑦)) → ∀𝑦((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥) → 𝑥 = 𝑦)) |
30 | | ax-1 6 |
. . . . . . 7
⊢
(∀𝑦((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥) → 𝑥 = 𝑦) → (𝑥 ∈ ∪ ∪ 𝑅
→ ∀𝑦((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥) → 𝑥 = 𝑦))) |
31 | 29, 30 | impbii 208 |
. . . . . 6
⊢ ((𝑥 ∈ ∪ ∪ 𝑅 → ∀𝑦((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥) → 𝑥 = 𝑦)) ↔ ∀𝑦((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥) → 𝑥 = 𝑦)) |
32 | 31 | albii 1822 |
. . . . 5
⊢
(∀𝑥(𝑥 ∈ ∪ ∪ 𝑅 → ∀𝑦((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥) → 𝑥 = 𝑦)) ↔ ∀𝑥∀𝑦((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥) → 𝑥 = 𝑦)) |
33 | 17, 32 | bitri 274 |
. . . 4
⊢
(∀𝑥 ∈
∪ ∪ 𝑅∀𝑦((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥) → 𝑥 = 𝑦) ↔ ∀𝑥∀𝑦((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥) → 𝑥 = 𝑦)) |
34 | 16, 33 | anbi12i 627 |
. . 3
⊢
((∀𝑥 ∈
∪ ∪ 𝑅∀𝑦(𝑥 = 𝑦 → (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥)) ∧ ∀𝑥 ∈ ∪ ∪ 𝑅∀𝑦((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥) → 𝑥 = 𝑦)) ↔ (∀𝑥 ∈ ∪ ∪ 𝑅𝑥𝑅𝑥 ∧ ∀𝑥∀𝑦((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥) → 𝑥 = 𝑦))) |
35 | 4, 5, 34 | 3bitri 297 |
. 2
⊢
(∀𝑥 ∈
∪ ∪ 𝑅(∀𝑦((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥) → 𝑥 = 𝑦) ∧ ∀𝑦(𝑥 = 𝑦 → (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥))) ↔ (∀𝑥 ∈ ∪ ∪ 𝑅𝑥𝑅𝑥 ∧ ∀𝑥∀𝑦((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥) → 𝑥 = 𝑦))) |
36 | 1, 3, 35 | 3bitri 297 |
1
⊢ ((𝑅 ∩ ◡𝑅) = ( I ↾ ∪
∪ 𝑅) ↔ (∀𝑥 ∈ ∪ ∪ 𝑅𝑥𝑅𝑥 ∧ ∀𝑥∀𝑦((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥) → 𝑥 = 𝑦))) |