Step | Hyp | Ref
| Expression |
1 | | simpl 108 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐴𝑅𝐵) → 𝜑) |
2 | | erth.1 |
. . . . . . . . 9
⊢ (𝜑 → 𝑅 Er 𝑋) |
3 | 2 | ersymb 6527 |
. . . . . . . 8
⊢ (𝜑 → (𝐴𝑅𝐵 ↔ 𝐵𝑅𝐴)) |
4 | 3 | biimpa 294 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐴𝑅𝐵) → 𝐵𝑅𝐴) |
5 | 1, 4 | jca 304 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐴𝑅𝐵) → (𝜑 ∧ 𝐵𝑅𝐴)) |
6 | 2 | ertr 6528 |
. . . . . . 7
⊢ (𝜑 → ((𝐵𝑅𝐴 ∧ 𝐴𝑅𝑥) → 𝐵𝑅𝑥)) |
7 | 6 | impl 378 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐵𝑅𝐴) ∧ 𝐴𝑅𝑥) → 𝐵𝑅𝑥) |
8 | 5, 7 | sylan 281 |
. . . . 5
⊢ (((𝜑 ∧ 𝐴𝑅𝐵) ∧ 𝐴𝑅𝑥) → 𝐵𝑅𝑥) |
9 | 2 | ertr 6528 |
. . . . . 6
⊢ (𝜑 → ((𝐴𝑅𝐵 ∧ 𝐵𝑅𝑥) → 𝐴𝑅𝑥)) |
10 | 9 | impl 378 |
. . . . 5
⊢ (((𝜑 ∧ 𝐴𝑅𝐵) ∧ 𝐵𝑅𝑥) → 𝐴𝑅𝑥) |
11 | 8, 10 | impbida 591 |
. . . 4
⊢ ((𝜑 ∧ 𝐴𝑅𝐵) → (𝐴𝑅𝑥 ↔ 𝐵𝑅𝑥)) |
12 | | vex 2733 |
. . . . 5
⊢ 𝑥 ∈ V |
13 | | erth.2 |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ 𝑋) |
14 | 13 | adantr 274 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴𝑅𝐵) → 𝐴 ∈ 𝑋) |
15 | | elecg 6551 |
. . . . 5
⊢ ((𝑥 ∈ V ∧ 𝐴 ∈ 𝑋) → (𝑥 ∈ [𝐴]𝑅 ↔ 𝐴𝑅𝑥)) |
16 | 12, 14, 15 | sylancr 412 |
. . . 4
⊢ ((𝜑 ∧ 𝐴𝑅𝐵) → (𝑥 ∈ [𝐴]𝑅 ↔ 𝐴𝑅𝑥)) |
17 | | errel 6522 |
. . . . . . 7
⊢ (𝑅 Er 𝑋 → Rel 𝑅) |
18 | 2, 17 | syl 14 |
. . . . . 6
⊢ (𝜑 → Rel 𝑅) |
19 | | brrelex2 4652 |
. . . . . 6
⊢ ((Rel
𝑅 ∧ 𝐴𝑅𝐵) → 𝐵 ∈ V) |
20 | 18, 19 | sylan 281 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴𝑅𝐵) → 𝐵 ∈ V) |
21 | | elecg 6551 |
. . . . 5
⊢ ((𝑥 ∈ V ∧ 𝐵 ∈ V) → (𝑥 ∈ [𝐵]𝑅 ↔ 𝐵𝑅𝑥)) |
22 | 12, 20, 21 | sylancr 412 |
. . . 4
⊢ ((𝜑 ∧ 𝐴𝑅𝐵) → (𝑥 ∈ [𝐵]𝑅 ↔ 𝐵𝑅𝑥)) |
23 | 11, 16, 22 | 3bitr4d 219 |
. . 3
⊢ ((𝜑 ∧ 𝐴𝑅𝐵) → (𝑥 ∈ [𝐴]𝑅 ↔ 𝑥 ∈ [𝐵]𝑅)) |
24 | 23 | eqrdv 2168 |
. 2
⊢ ((𝜑 ∧ 𝐴𝑅𝐵) → [𝐴]𝑅 = [𝐵]𝑅) |
25 | 2 | adantr 274 |
. . 3
⊢ ((𝜑 ∧ [𝐴]𝑅 = [𝐵]𝑅) → 𝑅 Er 𝑋) |
26 | 2, 13 | erref 6533 |
. . . . . . 7
⊢ (𝜑 → 𝐴𝑅𝐴) |
27 | 26 | adantr 274 |
. . . . . 6
⊢ ((𝜑 ∧ [𝐴]𝑅 = [𝐵]𝑅) → 𝐴𝑅𝐴) |
28 | 13 | adantr 274 |
. . . . . . 7
⊢ ((𝜑 ∧ [𝐴]𝑅 = [𝐵]𝑅) → 𝐴 ∈ 𝑋) |
29 | | elecg 6551 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋) → (𝐴 ∈ [𝐴]𝑅 ↔ 𝐴𝑅𝐴)) |
30 | 28, 28, 29 | syl2anc 409 |
. . . . . 6
⊢ ((𝜑 ∧ [𝐴]𝑅 = [𝐵]𝑅) → (𝐴 ∈ [𝐴]𝑅 ↔ 𝐴𝑅𝐴)) |
31 | 27, 30 | mpbird 166 |
. . . . 5
⊢ ((𝜑 ∧ [𝐴]𝑅 = [𝐵]𝑅) → 𝐴 ∈ [𝐴]𝑅) |
32 | | simpr 109 |
. . . . 5
⊢ ((𝜑 ∧ [𝐴]𝑅 = [𝐵]𝑅) → [𝐴]𝑅 = [𝐵]𝑅) |
33 | 31, 32 | eleqtrd 2249 |
. . . 4
⊢ ((𝜑 ∧ [𝐴]𝑅 = [𝐵]𝑅) → 𝐴 ∈ [𝐵]𝑅) |
34 | 25, 32 | ereldm 6556 |
. . . . . 6
⊢ ((𝜑 ∧ [𝐴]𝑅 = [𝐵]𝑅) → (𝐴 ∈ 𝑋 ↔ 𝐵 ∈ 𝑋)) |
35 | 28, 34 | mpbid 146 |
. . . . 5
⊢ ((𝜑 ∧ [𝐴]𝑅 = [𝐵]𝑅) → 𝐵 ∈ 𝑋) |
36 | | elecg 6551 |
. . . . 5
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴 ∈ [𝐵]𝑅 ↔ 𝐵𝑅𝐴)) |
37 | 28, 35, 36 | syl2anc 409 |
. . . 4
⊢ ((𝜑 ∧ [𝐴]𝑅 = [𝐵]𝑅) → (𝐴 ∈ [𝐵]𝑅 ↔ 𝐵𝑅𝐴)) |
38 | 33, 37 | mpbid 146 |
. . 3
⊢ ((𝜑 ∧ [𝐴]𝑅 = [𝐵]𝑅) → 𝐵𝑅𝐴) |
39 | 25, 38 | ersym 6525 |
. 2
⊢ ((𝜑 ∧ [𝐴]𝑅 = [𝐵]𝑅) → 𝐴𝑅𝐵) |
40 | 24, 39 | impbida 591 |
1
⊢ (𝜑 → (𝐴𝑅𝐵 ↔ [𝐴]𝑅 = [𝐵]𝑅)) |