Step | Hyp | Ref
| Expression |
1 | | simpl 473 |
. . . . . 6
⊢ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) → 𝑎 = 𝐴) |
2 | 1 | neeq1d 2853 |
. . . . 5
⊢ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) → (𝑎 ≠ 𝐶 ↔ 𝐴 ≠ 𝐶)) |
3 | | simpr 477 |
. . . . . 6
⊢ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) → 𝑏 = 𝐵) |
4 | 3 | neeq1d 2853 |
. . . . 5
⊢ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) → (𝑏 ≠ 𝐶 ↔ 𝐵 ≠ 𝐶)) |
5 | 3 | oveq2d 6666 |
. . . . . . 7
⊢ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) → (𝐶𝐼𝑏) = (𝐶𝐼𝐵)) |
6 | 1, 5 | eleq12d 2695 |
. . . . . 6
⊢ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) → (𝑎 ∈ (𝐶𝐼𝑏) ↔ 𝐴 ∈ (𝐶𝐼𝐵))) |
7 | 1 | oveq2d 6666 |
. . . . . . 7
⊢ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) → (𝐶𝐼𝑎) = (𝐶𝐼𝐴)) |
8 | 3, 7 | eleq12d 2695 |
. . . . . 6
⊢ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) → (𝑏 ∈ (𝐶𝐼𝑎) ↔ 𝐵 ∈ (𝐶𝐼𝐴))) |
9 | 6, 8 | orbi12d 746 |
. . . . 5
⊢ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) → ((𝑎 ∈ (𝐶𝐼𝑏) ∨ 𝑏 ∈ (𝐶𝐼𝑎)) ↔ (𝐴 ∈ (𝐶𝐼𝐵) ∨ 𝐵 ∈ (𝐶𝐼𝐴)))) |
10 | 2, 4, 9 | 3anbi123d 1399 |
. . . 4
⊢ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) → ((𝑎 ≠ 𝐶 ∧ 𝑏 ≠ 𝐶 ∧ (𝑎 ∈ (𝐶𝐼𝑏) ∨ 𝑏 ∈ (𝐶𝐼𝑎))) ↔ (𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ∧ (𝐴 ∈ (𝐶𝐼𝐵) ∨ 𝐵 ∈ (𝐶𝐼𝐴))))) |
11 | | eqid 2622 |
. . . 4
⊢
{〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) ∧ (𝑎 ≠ 𝐶 ∧ 𝑏 ≠ 𝐶 ∧ (𝑎 ∈ (𝐶𝐼𝑏) ∨ 𝑏 ∈ (𝐶𝐼𝑎))))} = {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) ∧ (𝑎 ≠ 𝐶 ∧ 𝑏 ≠ 𝐶 ∧ (𝑎 ∈ (𝐶𝐼𝑏) ∨ 𝑏 ∈ (𝐶𝐼𝑎))))} |
12 | 10, 11 | brab2a 5194 |
. . 3
⊢ (𝐴{〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) ∧ (𝑎 ≠ 𝐶 ∧ 𝑏 ≠ 𝐶 ∧ (𝑎 ∈ (𝐶𝐼𝑏) ∨ 𝑏 ∈ (𝐶𝐼𝑎))))}𝐵 ↔ ((𝐴 ∈ 𝑃 ∧ 𝐵 ∈ 𝑃) ∧ (𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ∧ (𝐴 ∈ (𝐶𝐼𝐵) ∨ 𝐵 ∈ (𝐶𝐼𝐴))))) |
13 | 12 | a1i 11 |
. 2
⊢ (𝜑 → (𝐴{〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) ∧ (𝑎 ≠ 𝐶 ∧ 𝑏 ≠ 𝐶 ∧ (𝑎 ∈ (𝐶𝐼𝑏) ∨ 𝑏 ∈ (𝐶𝐼𝑎))))}𝐵 ↔ ((𝐴 ∈ 𝑃 ∧ 𝐵 ∈ 𝑃) ∧ (𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ∧ (𝐴 ∈ (𝐶𝐼𝐵) ∨ 𝐵 ∈ (𝐶𝐼𝐴)))))) |
14 | | ishlg.k |
. . . . 5
⊢ 𝐾 = (hlG‘𝐺) |
15 | | ishlg.g |
. . . . . 6
⊢ (𝜑 → 𝐺 ∈ 𝑉) |
16 | | elex 3212 |
. . . . . 6
⊢ (𝐺 ∈ 𝑉 → 𝐺 ∈ V) |
17 | | fveq2 6191 |
. . . . . . . . 9
⊢ (𝑔 = 𝐺 → (Base‘𝑔) = (Base‘𝐺)) |
18 | | ishlg.p |
. . . . . . . . 9
⊢ 𝑃 = (Base‘𝐺) |
19 | 17, 18 | syl6eqr 2674 |
. . . . . . . 8
⊢ (𝑔 = 𝐺 → (Base‘𝑔) = 𝑃) |
20 | 19 | eleq2d 2687 |
. . . . . . . . . . 11
⊢ (𝑔 = 𝐺 → (𝑎 ∈ (Base‘𝑔) ↔ 𝑎 ∈ 𝑃)) |
21 | 19 | eleq2d 2687 |
. . . . . . . . . . 11
⊢ (𝑔 = 𝐺 → (𝑏 ∈ (Base‘𝑔) ↔ 𝑏 ∈ 𝑃)) |
22 | 20, 21 | anbi12d 747 |
. . . . . . . . . 10
⊢ (𝑔 = 𝐺 → ((𝑎 ∈ (Base‘𝑔) ∧ 𝑏 ∈ (Base‘𝑔)) ↔ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃))) |
23 | | fveq2 6191 |
. . . . . . . . . . . . . . 15
⊢ (𝑔 = 𝐺 → (Itv‘𝑔) = (Itv‘𝐺)) |
24 | | ishlg.i |
. . . . . . . . . . . . . . 15
⊢ 𝐼 = (Itv‘𝐺) |
25 | 23, 24 | syl6eqr 2674 |
. . . . . . . . . . . . . 14
⊢ (𝑔 = 𝐺 → (Itv‘𝑔) = 𝐼) |
26 | 25 | oveqd 6667 |
. . . . . . . . . . . . 13
⊢ (𝑔 = 𝐺 → (𝑐(Itv‘𝑔)𝑏) = (𝑐𝐼𝑏)) |
27 | 26 | eleq2d 2687 |
. . . . . . . . . . . 12
⊢ (𝑔 = 𝐺 → (𝑎 ∈ (𝑐(Itv‘𝑔)𝑏) ↔ 𝑎 ∈ (𝑐𝐼𝑏))) |
28 | 25 | oveqd 6667 |
. . . . . . . . . . . . 13
⊢ (𝑔 = 𝐺 → (𝑐(Itv‘𝑔)𝑎) = (𝑐𝐼𝑎)) |
29 | 28 | eleq2d 2687 |
. . . . . . . . . . . 12
⊢ (𝑔 = 𝐺 → (𝑏 ∈ (𝑐(Itv‘𝑔)𝑎) ↔ 𝑏 ∈ (𝑐𝐼𝑎))) |
30 | 27, 29 | orbi12d 746 |
. . . . . . . . . . 11
⊢ (𝑔 = 𝐺 → ((𝑎 ∈ (𝑐(Itv‘𝑔)𝑏) ∨ 𝑏 ∈ (𝑐(Itv‘𝑔)𝑎)) ↔ (𝑎 ∈ (𝑐𝐼𝑏) ∨ 𝑏 ∈ (𝑐𝐼𝑎)))) |
31 | 30 | 3anbi3d 1405 |
. . . . . . . . . 10
⊢ (𝑔 = 𝐺 → ((𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ∧ (𝑎 ∈ (𝑐(Itv‘𝑔)𝑏) ∨ 𝑏 ∈ (𝑐(Itv‘𝑔)𝑎))) ↔ (𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ∧ (𝑎 ∈ (𝑐𝐼𝑏) ∨ 𝑏 ∈ (𝑐𝐼𝑎))))) |
32 | 22, 31 | anbi12d 747 |
. . . . . . . . 9
⊢ (𝑔 = 𝐺 → (((𝑎 ∈ (Base‘𝑔) ∧ 𝑏 ∈ (Base‘𝑔)) ∧ (𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ∧ (𝑎 ∈ (𝑐(Itv‘𝑔)𝑏) ∨ 𝑏 ∈ (𝑐(Itv‘𝑔)𝑎)))) ↔ ((𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) ∧ (𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ∧ (𝑎 ∈ (𝑐𝐼𝑏) ∨ 𝑏 ∈ (𝑐𝐼𝑎)))))) |
33 | 32 | opabbidv 4716 |
. . . . . . . 8
⊢ (𝑔 = 𝐺 → {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (Base‘𝑔) ∧ 𝑏 ∈ (Base‘𝑔)) ∧ (𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ∧ (𝑎 ∈ (𝑐(Itv‘𝑔)𝑏) ∨ 𝑏 ∈ (𝑐(Itv‘𝑔)𝑎))))} = {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) ∧ (𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ∧ (𝑎 ∈ (𝑐𝐼𝑏) ∨ 𝑏 ∈ (𝑐𝐼𝑎))))}) |
34 | 19, 33 | mpteq12dv 4733 |
. . . . . . 7
⊢ (𝑔 = 𝐺 → (𝑐 ∈ (Base‘𝑔) ↦ {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (Base‘𝑔) ∧ 𝑏 ∈ (Base‘𝑔)) ∧ (𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ∧ (𝑎 ∈ (𝑐(Itv‘𝑔)𝑏) ∨ 𝑏 ∈ (𝑐(Itv‘𝑔)𝑎))))}) = (𝑐 ∈ 𝑃 ↦ {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) ∧ (𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ∧ (𝑎 ∈ (𝑐𝐼𝑏) ∨ 𝑏 ∈ (𝑐𝐼𝑎))))})) |
35 | | df-hlg 25496 |
. . . . . . 7
⊢ hlG =
(𝑔 ∈ V ↦ (𝑐 ∈ (Base‘𝑔) ↦ {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (Base‘𝑔) ∧ 𝑏 ∈ (Base‘𝑔)) ∧ (𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ∧ (𝑎 ∈ (𝑐(Itv‘𝑔)𝑏) ∨ 𝑏 ∈ (𝑐(Itv‘𝑔)𝑎))))})) |
36 | | fvex 6201 |
. . . . . . . . 9
⊢
(Base‘𝐺)
∈ V |
37 | 18, 36 | eqeltri 2697 |
. . . . . . . 8
⊢ 𝑃 ∈ V |
38 | 37 | mptex 6486 |
. . . . . . 7
⊢ (𝑐 ∈ 𝑃 ↦ {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) ∧ (𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ∧ (𝑎 ∈ (𝑐𝐼𝑏) ∨ 𝑏 ∈ (𝑐𝐼𝑎))))}) ∈ V |
39 | 34, 35, 38 | fvmpt 6282 |
. . . . . 6
⊢ (𝐺 ∈ V →
(hlG‘𝐺) = (𝑐 ∈ 𝑃 ↦ {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) ∧ (𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ∧ (𝑎 ∈ (𝑐𝐼𝑏) ∨ 𝑏 ∈ (𝑐𝐼𝑎))))})) |
40 | 15, 16, 39 | 3syl 18 |
. . . . 5
⊢ (𝜑 → (hlG‘𝐺) = (𝑐 ∈ 𝑃 ↦ {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) ∧ (𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ∧ (𝑎 ∈ (𝑐𝐼𝑏) ∨ 𝑏 ∈ (𝑐𝐼𝑎))))})) |
41 | 14, 40 | syl5eq 2668 |
. . . 4
⊢ (𝜑 → 𝐾 = (𝑐 ∈ 𝑃 ↦ {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) ∧ (𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ∧ (𝑎 ∈ (𝑐𝐼𝑏) ∨ 𝑏 ∈ (𝑐𝐼𝑎))))})) |
42 | | neeq2 2857 |
. . . . . . . 8
⊢ (𝑐 = 𝐶 → (𝑎 ≠ 𝑐 ↔ 𝑎 ≠ 𝐶)) |
43 | | neeq2 2857 |
. . . . . . . 8
⊢ (𝑐 = 𝐶 → (𝑏 ≠ 𝑐 ↔ 𝑏 ≠ 𝐶)) |
44 | | oveq1 6657 |
. . . . . . . . . 10
⊢ (𝑐 = 𝐶 → (𝑐𝐼𝑏) = (𝐶𝐼𝑏)) |
45 | 44 | eleq2d 2687 |
. . . . . . . . 9
⊢ (𝑐 = 𝐶 → (𝑎 ∈ (𝑐𝐼𝑏) ↔ 𝑎 ∈ (𝐶𝐼𝑏))) |
46 | | oveq1 6657 |
. . . . . . . . . 10
⊢ (𝑐 = 𝐶 → (𝑐𝐼𝑎) = (𝐶𝐼𝑎)) |
47 | 46 | eleq2d 2687 |
. . . . . . . . 9
⊢ (𝑐 = 𝐶 → (𝑏 ∈ (𝑐𝐼𝑎) ↔ 𝑏 ∈ (𝐶𝐼𝑎))) |
48 | 45, 47 | orbi12d 746 |
. . . . . . . 8
⊢ (𝑐 = 𝐶 → ((𝑎 ∈ (𝑐𝐼𝑏) ∨ 𝑏 ∈ (𝑐𝐼𝑎)) ↔ (𝑎 ∈ (𝐶𝐼𝑏) ∨ 𝑏 ∈ (𝐶𝐼𝑎)))) |
49 | 42, 43, 48 | 3anbi123d 1399 |
. . . . . . 7
⊢ (𝑐 = 𝐶 → ((𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ∧ (𝑎 ∈ (𝑐𝐼𝑏) ∨ 𝑏 ∈ (𝑐𝐼𝑎))) ↔ (𝑎 ≠ 𝐶 ∧ 𝑏 ≠ 𝐶 ∧ (𝑎 ∈ (𝐶𝐼𝑏) ∨ 𝑏 ∈ (𝐶𝐼𝑎))))) |
50 | 49 | anbi2d 740 |
. . . . . 6
⊢ (𝑐 = 𝐶 → (((𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) ∧ (𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ∧ (𝑎 ∈ (𝑐𝐼𝑏) ∨ 𝑏 ∈ (𝑐𝐼𝑎)))) ↔ ((𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) ∧ (𝑎 ≠ 𝐶 ∧ 𝑏 ≠ 𝐶 ∧ (𝑎 ∈ (𝐶𝐼𝑏) ∨ 𝑏 ∈ (𝐶𝐼𝑎)))))) |
51 | 50 | opabbidv 4716 |
. . . . 5
⊢ (𝑐 = 𝐶 → {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) ∧ (𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ∧ (𝑎 ∈ (𝑐𝐼𝑏) ∨ 𝑏 ∈ (𝑐𝐼𝑎))))} = {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) ∧ (𝑎 ≠ 𝐶 ∧ 𝑏 ≠ 𝐶 ∧ (𝑎 ∈ (𝐶𝐼𝑏) ∨ 𝑏 ∈ (𝐶𝐼𝑎))))}) |
52 | 51 | adantl 482 |
. . . 4
⊢ ((𝜑 ∧ 𝑐 = 𝐶) → {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) ∧ (𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ∧ (𝑎 ∈ (𝑐𝐼𝑏) ∨ 𝑏 ∈ (𝑐𝐼𝑎))))} = {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) ∧ (𝑎 ≠ 𝐶 ∧ 𝑏 ≠ 𝐶 ∧ (𝑎 ∈ (𝐶𝐼𝑏) ∨ 𝑏 ∈ (𝐶𝐼𝑎))))}) |
53 | | ishlg.c |
. . . 4
⊢ (𝜑 → 𝐶 ∈ 𝑃) |
54 | 37, 37 | xpex 6962 |
. . . . . 6
⊢ (𝑃 × 𝑃) ∈ V |
55 | | opabssxp 5193 |
. . . . . 6
⊢
{〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) ∧ (𝑎 ≠ 𝐶 ∧ 𝑏 ≠ 𝐶 ∧ (𝑎 ∈ (𝐶𝐼𝑏) ∨ 𝑏 ∈ (𝐶𝐼𝑎))))} ⊆ (𝑃 × 𝑃) |
56 | 54, 55 | ssexi 4803 |
. . . . 5
⊢
{〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) ∧ (𝑎 ≠ 𝐶 ∧ 𝑏 ≠ 𝐶 ∧ (𝑎 ∈ (𝐶𝐼𝑏) ∨ 𝑏 ∈ (𝐶𝐼𝑎))))} ∈ V |
57 | 56 | a1i 11 |
. . . 4
⊢ (𝜑 → {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) ∧ (𝑎 ≠ 𝐶 ∧ 𝑏 ≠ 𝐶 ∧ (𝑎 ∈ (𝐶𝐼𝑏) ∨ 𝑏 ∈ (𝐶𝐼𝑎))))} ∈ V) |
58 | 41, 52, 53, 57 | fvmptd 6288 |
. . 3
⊢ (𝜑 → (𝐾‘𝐶) = {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) ∧ (𝑎 ≠ 𝐶 ∧ 𝑏 ≠ 𝐶 ∧ (𝑎 ∈ (𝐶𝐼𝑏) ∨ 𝑏 ∈ (𝐶𝐼𝑎))))}) |
59 | 58 | breqd 4664 |
. 2
⊢ (𝜑 → (𝐴(𝐾‘𝐶)𝐵 ↔ 𝐴{〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) ∧ (𝑎 ≠ 𝐶 ∧ 𝑏 ≠ 𝐶 ∧ (𝑎 ∈ (𝐶𝐼𝑏) ∨ 𝑏 ∈ (𝐶𝐼𝑎))))}𝐵)) |
60 | | ishlg.a |
. . . 4
⊢ (𝜑 → 𝐴 ∈ 𝑃) |
61 | | ishlg.b |
. . . 4
⊢ (𝜑 → 𝐵 ∈ 𝑃) |
62 | 60, 61 | jca 554 |
. . 3
⊢ (𝜑 → (𝐴 ∈ 𝑃 ∧ 𝐵 ∈ 𝑃)) |
63 | 62 | biantrurd 529 |
. 2
⊢ (𝜑 → ((𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ∧ (𝐴 ∈ (𝐶𝐼𝐵) ∨ 𝐵 ∈ (𝐶𝐼𝐴))) ↔ ((𝐴 ∈ 𝑃 ∧ 𝐵 ∈ 𝑃) ∧ (𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ∧ (𝐴 ∈ (𝐶𝐼𝐵) ∨ 𝐵 ∈ (𝐶𝐼𝐴)))))) |
64 | 13, 59, 63 | 3bitr4d 300 |
1
⊢ (𝜑 → (𝐴(𝐾‘𝐶)𝐵 ↔ (𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ∧ (𝐴 ∈ (𝐶𝐼𝐵) ∨ 𝐵 ∈ (𝐶𝐼𝐴))))) |