Proof of Theorem asymref
Step | Hyp | Ref
| Expression |
1 | | df-br 3968 |
. . . . . . . . . . 11
⊢ (𝑥𝑅𝑦 ↔ 〈𝑥, 𝑦〉 ∈ 𝑅) |
2 | | vex 2715 |
. . . . . . . . . . . 12
⊢ 𝑥 ∈ V |
3 | | vex 2715 |
. . . . . . . . . . . 12
⊢ 𝑦 ∈ V |
4 | 2, 3 | opeluu 4413 |
. . . . . . . . . . 11
⊢
(〈𝑥, 𝑦〉 ∈ 𝑅 → (𝑥 ∈ ∪ ∪ 𝑅
∧ 𝑦 ∈ ∪ ∪ 𝑅)) |
5 | 1, 4 | sylbi 120 |
. . . . . . . . . 10
⊢ (𝑥𝑅𝑦 → (𝑥 ∈ ∪ ∪ 𝑅
∧ 𝑦 ∈ ∪ ∪ 𝑅)) |
6 | 5 | simpld 111 |
. . . . . . . . 9
⊢ (𝑥𝑅𝑦 → 𝑥 ∈ ∪ ∪ 𝑅) |
7 | 6 | adantr 274 |
. . . . . . . 8
⊢ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥) → 𝑥 ∈ ∪ ∪ 𝑅) |
8 | 7 | pm4.71ri 390 |
. . . . . . 7
⊢ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥) ↔ (𝑥 ∈ ∪ ∪ 𝑅
∧ (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥))) |
9 | 8 | bibi1i 227 |
. . . . . 6
⊢ (((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥) ↔ (𝑥 ∈ ∪ ∪ 𝑅
∧ 𝑥 = 𝑦)) ↔ ((𝑥 ∈ ∪ ∪ 𝑅
∧ (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥)) ↔ (𝑥 ∈ ∪ ∪ 𝑅
∧ 𝑥 = 𝑦))) |
10 | | elin 3291 |
. . . . . . . 8
⊢
(〈𝑥, 𝑦〉 ∈ (𝑅 ∩ ◡𝑅) ↔ (〈𝑥, 𝑦〉 ∈ 𝑅 ∧ 〈𝑥, 𝑦〉 ∈ ◡𝑅)) |
11 | 2, 3 | brcnv 4772 |
. . . . . . . . . 10
⊢ (𝑥◡𝑅𝑦 ↔ 𝑦𝑅𝑥) |
12 | | df-br 3968 |
. . . . . . . . . 10
⊢ (𝑥◡𝑅𝑦 ↔ 〈𝑥, 𝑦〉 ∈ ◡𝑅) |
13 | 11, 12 | bitr3i 185 |
. . . . . . . . 9
⊢ (𝑦𝑅𝑥 ↔ 〈𝑥, 𝑦〉 ∈ ◡𝑅) |
14 | 1, 13 | anbi12i 456 |
. . . . . . . 8
⊢ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥) ↔ (〈𝑥, 𝑦〉 ∈ 𝑅 ∧ 〈𝑥, 𝑦〉 ∈ ◡𝑅)) |
15 | 10, 14 | bitr4i 186 |
. . . . . . 7
⊢
(〈𝑥, 𝑦〉 ∈ (𝑅 ∩ ◡𝑅) ↔ (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥)) |
16 | 3 | opelres 4874 |
. . . . . . . 8
⊢
(〈𝑥, 𝑦〉 ∈ ( I ↾ ∪ ∪ 𝑅) ↔ (〈𝑥, 𝑦〉 ∈ I ∧ 𝑥 ∈ ∪ ∪ 𝑅)) |
17 | | df-br 3968 |
. . . . . . . . . 10
⊢ (𝑥 I 𝑦 ↔ 〈𝑥, 𝑦〉 ∈ I ) |
18 | 3 | ideq 4741 |
. . . . . . . . . 10
⊢ (𝑥 I 𝑦 ↔ 𝑥 = 𝑦) |
19 | 17, 18 | bitr3i 185 |
. . . . . . . . 9
⊢
(〈𝑥, 𝑦〉 ∈ I ↔ 𝑥 = 𝑦) |
20 | 19 | anbi2ci 455 |
. . . . . . . 8
⊢
((〈𝑥, 𝑦〉 ∈ I ∧ 𝑥 ∈ ∪ ∪ 𝑅) ↔ (𝑥 ∈ ∪ ∪ 𝑅
∧ 𝑥 = 𝑦)) |
21 | 16, 20 | bitri 183 |
. . . . . . 7
⊢
(〈𝑥, 𝑦〉 ∈ ( I ↾ ∪ ∪ 𝑅) ↔ (𝑥 ∈ ∪ ∪ 𝑅
∧ 𝑥 = 𝑦)) |
22 | 15, 21 | bibi12i 228 |
. . . . . 6
⊢
((〈𝑥, 𝑦〉 ∈ (𝑅 ∩ ◡𝑅) ↔ 〈𝑥, 𝑦〉 ∈ ( I ↾ ∪ ∪ 𝑅)) ↔ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥) ↔ (𝑥 ∈ ∪ ∪ 𝑅
∧ 𝑥 = 𝑦))) |
23 | | pm5.32 449 |
. . . . . 6
⊢ ((𝑥 ∈ ∪ ∪ 𝑅 → ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥) ↔ 𝑥 = 𝑦)) ↔ ((𝑥 ∈ ∪ ∪ 𝑅
∧ (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥)) ↔ (𝑥 ∈ ∪ ∪ 𝑅
∧ 𝑥 = 𝑦))) |
24 | 9, 22, 23 | 3bitr4i 211 |
. . . . 5
⊢
((〈𝑥, 𝑦〉 ∈ (𝑅 ∩ ◡𝑅) ↔ 〈𝑥, 𝑦〉 ∈ ( I ↾ ∪ ∪ 𝑅)) ↔ (𝑥 ∈ ∪ ∪ 𝑅
→ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥) ↔ 𝑥 = 𝑦))) |
25 | 24 | albii 1450 |
. . . 4
⊢
(∀𝑦(〈𝑥, 𝑦〉 ∈ (𝑅 ∩ ◡𝑅) ↔ 〈𝑥, 𝑦〉 ∈ ( I ↾ ∪ ∪ 𝑅)) ↔ ∀𝑦(𝑥 ∈ ∪ ∪ 𝑅
→ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥) ↔ 𝑥 = 𝑦))) |
26 | | 19.21v 1853 |
. . . 4
⊢
(∀𝑦(𝑥 ∈ ∪ ∪ 𝑅 → ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥) ↔ 𝑥 = 𝑦)) ↔ (𝑥 ∈ ∪ ∪ 𝑅
→ ∀𝑦((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥) ↔ 𝑥 = 𝑦))) |
27 | 25, 26 | bitri 183 |
. . 3
⊢
(∀𝑦(〈𝑥, 𝑦〉 ∈ (𝑅 ∩ ◡𝑅) ↔ 〈𝑥, 𝑦〉 ∈ ( I ↾ ∪ ∪ 𝑅)) ↔ (𝑥 ∈ ∪ ∪ 𝑅
→ ∀𝑦((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥) ↔ 𝑥 = 𝑦))) |
28 | 27 | albii 1450 |
. 2
⊢
(∀𝑥∀𝑦(〈𝑥, 𝑦〉 ∈ (𝑅 ∩ ◡𝑅) ↔ 〈𝑥, 𝑦〉 ∈ ( I ↾ ∪ ∪ 𝑅)) ↔ ∀𝑥(𝑥 ∈ ∪ ∪ 𝑅
→ ∀𝑦((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥) ↔ 𝑥 = 𝑦))) |
29 | | relcnv 4967 |
. . . 4
⊢ Rel ◡𝑅 |
30 | | relin2 4708 |
. . . 4
⊢ (Rel
◡𝑅 → Rel (𝑅 ∩ ◡𝑅)) |
31 | 29, 30 | ax-mp 5 |
. . 3
⊢ Rel
(𝑅 ∩ ◡𝑅) |
32 | | relres 4897 |
. . 3
⊢ Rel ( I
↾ ∪ ∪ 𝑅) |
33 | | eqrel 4678 |
. . 3
⊢ ((Rel
(𝑅 ∩ ◡𝑅) ∧ Rel ( I ↾ ∪ ∪ 𝑅)) → ((𝑅 ∩ ◡𝑅) = ( I ↾ ∪
∪ 𝑅) ↔ ∀𝑥∀𝑦(〈𝑥, 𝑦〉 ∈ (𝑅 ∩ ◡𝑅) ↔ 〈𝑥, 𝑦〉 ∈ ( I ↾ ∪ ∪ 𝑅)))) |
34 | 31, 32, 33 | mp2an 423 |
. 2
⊢ ((𝑅 ∩ ◡𝑅) = ( I ↾ ∪
∪ 𝑅) ↔ ∀𝑥∀𝑦(〈𝑥, 𝑦〉 ∈ (𝑅 ∩ ◡𝑅) ↔ 〈𝑥, 𝑦〉 ∈ ( I ↾ ∪ ∪ 𝑅))) |
35 | | df-ral 2440 |
. 2
⊢
(∀𝑥 ∈
∪ ∪ 𝑅∀𝑦((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥) ↔ 𝑥 = 𝑦) ↔ ∀𝑥(𝑥 ∈ ∪ ∪ 𝑅
→ ∀𝑦((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥) ↔ 𝑥 = 𝑦))) |
36 | 28, 34, 35 | 3bitr4i 211 |
1
⊢ ((𝑅 ∩ ◡𝑅) = ( I ↾ ∪
∪ 𝑅) ↔ ∀𝑥 ∈ ∪ ∪ 𝑅∀𝑦((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥) ↔ 𝑥 = 𝑦)) |