Step | Hyp | Ref
| Expression |
1 | | simpl 484 |
. . . . . 6
β’ ((π = π΄ β§ π = π΅) β π = π΄) |
2 | 1 | neeq1d 3001 |
. . . . 5
β’ ((π = π΄ β§ π = π΅) β (π β πΆ β π΄ β πΆ)) |
3 | | simpr 486 |
. . . . . 6
β’ ((π = π΄ β§ π = π΅) β π = π΅) |
4 | 3 | neeq1d 3001 |
. . . . 5
β’ ((π = π΄ β§ π = π΅) β (π β πΆ β π΅ β πΆ)) |
5 | 3 | oveq2d 7420 |
. . . . . . 7
β’ ((π = π΄ β§ π = π΅) β (πΆπΌπ) = (πΆπΌπ΅)) |
6 | 1, 5 | eleq12d 2828 |
. . . . . 6
β’ ((π = π΄ β§ π = π΅) β (π β (πΆπΌπ) β π΄ β (πΆπΌπ΅))) |
7 | 1 | oveq2d 7420 |
. . . . . . 7
β’ ((π = π΄ β§ π = π΅) β (πΆπΌπ) = (πΆπΌπ΄)) |
8 | 3, 7 | eleq12d 2828 |
. . . . . 6
β’ ((π = π΄ β§ π = π΅) β (π β (πΆπΌπ) β π΅ β (πΆπΌπ΄))) |
9 | 6, 8 | orbi12d 918 |
. . . . 5
β’ ((π = π΄ β§ π = π΅) β ((π β (πΆπΌπ) β¨ π β (πΆπΌπ)) β (π΄ β (πΆπΌπ΅) β¨ π΅ β (πΆπΌπ΄)))) |
10 | 2, 4, 9 | 3anbi123d 1437 |
. . . 4
β’ ((π = π΄ β§ π = π΅) β ((π β πΆ β§ π β πΆ β§ (π β (πΆπΌπ) β¨ π β (πΆπΌπ))) β (π΄ β πΆ β§ π΅ β πΆ β§ (π΄ β (πΆπΌπ΅) β¨ π΅ β (πΆπΌπ΄))))) |
11 | | eqid 2733 |
. . . 4
β’
{β¨π, πβ© β£ ((π β π β§ π β π) β§ (π β πΆ β§ π β πΆ β§ (π β (πΆπΌπ) β¨ π β (πΆπΌπ))))} = {β¨π, πβ© β£ ((π β π β§ π β π) β§ (π β πΆ β§ π β πΆ β§ (π β (πΆπΌπ) β¨ π β (πΆπΌπ))))} |
12 | 10, 11 | brab2a 5767 |
. . 3
β’ (π΄{β¨π, πβ© β£ ((π β π β§ π β π) β§ (π β πΆ β§ π β πΆ β§ (π β (πΆπΌπ) β¨ π β (πΆπΌπ))))}π΅ β ((π΄ β π β§ π΅ β π) β§ (π΄ β πΆ β§ π΅ β πΆ β§ (π΄ β (πΆπΌπ΅) β¨ π΅ β (πΆπΌπ΄))))) |
13 | 12 | a1i 11 |
. 2
β’ (π β (π΄{β¨π, πβ© β£ ((π β π β§ π β π) β§ (π β πΆ β§ π β πΆ β§ (π β (πΆπΌπ) β¨ π β (πΆπΌπ))))}π΅ β ((π΄ β π β§ π΅ β π) β§ (π΄ β πΆ β§ π΅ β πΆ β§ (π΄ β (πΆπΌπ΅) β¨ π΅ β (πΆπΌπ΄)))))) |
14 | | ishlg.k |
. . . . 5
β’ πΎ = (hlGβπΊ) |
15 | | ishlg.g |
. . . . . 6
β’ (π β πΊ β π) |
16 | | elex 3493 |
. . . . . 6
β’ (πΊ β π β πΊ β V) |
17 | | fveq2 6888 |
. . . . . . . . 9
β’ (π = πΊ β (Baseβπ) = (BaseβπΊ)) |
18 | | ishlg.p |
. . . . . . . . 9
β’ π = (BaseβπΊ) |
19 | 17, 18 | eqtr4di 2791 |
. . . . . . . 8
β’ (π = πΊ β (Baseβπ) = π) |
20 | 19 | eleq2d 2820 |
. . . . . . . . . . 11
β’ (π = πΊ β (π β (Baseβπ) β π β π)) |
21 | 19 | eleq2d 2820 |
. . . . . . . . . . 11
β’ (π = πΊ β (π β (Baseβπ) β π β π)) |
22 | 20, 21 | anbi12d 632 |
. . . . . . . . . 10
β’ (π = πΊ β ((π β (Baseβπ) β§ π β (Baseβπ)) β (π β π β§ π β π))) |
23 | | fveq2 6888 |
. . . . . . . . . . . . . . 15
β’ (π = πΊ β (Itvβπ) = (ItvβπΊ)) |
24 | | ishlg.i |
. . . . . . . . . . . . . . 15
β’ πΌ = (ItvβπΊ) |
25 | 23, 24 | eqtr4di 2791 |
. . . . . . . . . . . . . 14
β’ (π = πΊ β (Itvβπ) = πΌ) |
26 | 25 | oveqd 7421 |
. . . . . . . . . . . . 13
β’ (π = πΊ β (π(Itvβπ)π) = (ππΌπ)) |
27 | 26 | eleq2d 2820 |
. . . . . . . . . . . 12
β’ (π = πΊ β (π β (π(Itvβπ)π) β π β (ππΌπ))) |
28 | 25 | oveqd 7421 |
. . . . . . . . . . . . 13
β’ (π = πΊ β (π(Itvβπ)π) = (ππΌπ)) |
29 | 28 | eleq2d 2820 |
. . . . . . . . . . . 12
β’ (π = πΊ β (π β (π(Itvβπ)π) β π β (ππΌπ))) |
30 | 27, 29 | orbi12d 918 |
. . . . . . . . . . 11
β’ (π = πΊ β ((π β (π(Itvβπ)π) β¨ π β (π(Itvβπ)π)) β (π β (ππΌπ) β¨ π β (ππΌπ)))) |
31 | 30 | 3anbi3d 1443 |
. . . . . . . . . 10
β’ (π = πΊ β ((π β π β§ π β π β§ (π β (π(Itvβπ)π) β¨ π β (π(Itvβπ)π))) β (π β π β§ π β π β§ (π β (ππΌπ) β¨ π β (ππΌπ))))) |
32 | 22, 31 | anbi12d 632 |
. . . . . . . . 9
β’ (π = πΊ β (((π β (Baseβπ) β§ π β (Baseβπ)) β§ (π β π β§ π β π β§ (π β (π(Itvβπ)π) β¨ π β (π(Itvβπ)π)))) β ((π β π β§ π β π) β§ (π β π β§ π β π β§ (π β (ππΌπ) β¨ π β (ππΌπ)))))) |
33 | 32 | opabbidv 5213 |
. . . . . . . 8
β’ (π = πΊ β {β¨π, πβ© β£ ((π β (Baseβπ) β§ π β (Baseβπ)) β§ (π β π β§ π β π β§ (π β (π(Itvβπ)π) β¨ π β (π(Itvβπ)π))))} = {β¨π, πβ© β£ ((π β π β§ π β π) β§ (π β π β§ π β π β§ (π β (ππΌπ) β¨ π β (ππΌπ))))}) |
34 | 19, 33 | mpteq12dv 5238 |
. . . . . . 7
β’ (π = πΊ β (π β (Baseβπ) β¦ {β¨π, πβ© β£ ((π β (Baseβπ) β§ π β (Baseβπ)) β§ (π β π β§ π β π β§ (π β (π(Itvβπ)π) β¨ π β (π(Itvβπ)π))))}) = (π β π β¦ {β¨π, πβ© β£ ((π β π β§ π β π) β§ (π β π β§ π β π β§ (π β (ππΌπ) β¨ π β (ππΌπ))))})) |
35 | | df-hlg 27832 |
. . . . . . 7
β’ hlG =
(π β V β¦ (π β (Baseβπ) β¦ {β¨π, πβ© β£ ((π β (Baseβπ) β§ π β (Baseβπ)) β§ (π β π β§ π β π β§ (π β (π(Itvβπ)π) β¨ π β (π(Itvβπ)π))))})) |
36 | 34, 35, 18 | mptfvmpt 7225 |
. . . . . 6
β’ (πΊ β V β
(hlGβπΊ) = (π β π β¦ {β¨π, πβ© β£ ((π β π β§ π β π) β§ (π β π β§ π β π β§ (π β (ππΌπ) β¨ π β (ππΌπ))))})) |
37 | 15, 16, 36 | 3syl 18 |
. . . . 5
β’ (π β (hlGβπΊ) = (π β π β¦ {β¨π, πβ© β£ ((π β π β§ π β π) β§ (π β π β§ π β π β§ (π β (ππΌπ) β¨ π β (ππΌπ))))})) |
38 | 14, 37 | eqtrid 2785 |
. . . 4
β’ (π β πΎ = (π β π β¦ {β¨π, πβ© β£ ((π β π β§ π β π) β§ (π β π β§ π β π β§ (π β (ππΌπ) β¨ π β (ππΌπ))))})) |
39 | | neeq2 3005 |
. . . . . . . 8
β’ (π = πΆ β (π β π β π β πΆ)) |
40 | | neeq2 3005 |
. . . . . . . 8
β’ (π = πΆ β (π β π β π β πΆ)) |
41 | | oveq1 7411 |
. . . . . . . . . 10
β’ (π = πΆ β (ππΌπ) = (πΆπΌπ)) |
42 | 41 | eleq2d 2820 |
. . . . . . . . 9
β’ (π = πΆ β (π β (ππΌπ) β π β (πΆπΌπ))) |
43 | | oveq1 7411 |
. . . . . . . . . 10
β’ (π = πΆ β (ππΌπ) = (πΆπΌπ)) |
44 | 43 | eleq2d 2820 |
. . . . . . . . 9
β’ (π = πΆ β (π β (ππΌπ) β π β (πΆπΌπ))) |
45 | 42, 44 | orbi12d 918 |
. . . . . . . 8
β’ (π = πΆ β ((π β (ππΌπ) β¨ π β (ππΌπ)) β (π β (πΆπΌπ) β¨ π β (πΆπΌπ)))) |
46 | 39, 40, 45 | 3anbi123d 1437 |
. . . . . . 7
β’ (π = πΆ β ((π β π β§ π β π β§ (π β (ππΌπ) β¨ π β (ππΌπ))) β (π β πΆ β§ π β πΆ β§ (π β (πΆπΌπ) β¨ π β (πΆπΌπ))))) |
47 | 46 | anbi2d 630 |
. . . . . 6
β’ (π = πΆ β (((π β π β§ π β π) β§ (π β π β§ π β π β§ (π β (ππΌπ) β¨ π β (ππΌπ)))) β ((π β π β§ π β π) β§ (π β πΆ β§ π β πΆ β§ (π β (πΆπΌπ) β¨ π β (πΆπΌπ)))))) |
48 | 47 | opabbidv 5213 |
. . . . 5
β’ (π = πΆ β {β¨π, πβ© β£ ((π β π β§ π β π) β§ (π β π β§ π β π β§ (π β (ππΌπ) β¨ π β (ππΌπ))))} = {β¨π, πβ© β£ ((π β π β§ π β π) β§ (π β πΆ β§ π β πΆ β§ (π β (πΆπΌπ) β¨ π β (πΆπΌπ))))}) |
49 | 48 | adantl 483 |
. . . 4
β’ ((π β§ π = πΆ) β {β¨π, πβ© β£ ((π β π β§ π β π) β§ (π β π β§ π β π β§ (π β (ππΌπ) β¨ π β (ππΌπ))))} = {β¨π, πβ© β£ ((π β π β§ π β π) β§ (π β πΆ β§ π β πΆ β§ (π β (πΆπΌπ) β¨ π β (πΆπΌπ))))}) |
50 | | ishlg.c |
. . . 4
β’ (π β πΆ β π) |
51 | 18 | fvexi 6902 |
. . . . . . 7
β’ π β V |
52 | 51, 51 | xpex 7735 |
. . . . . 6
β’ (π Γ π) β V |
53 | | opabssxp 5766 |
. . . . . 6
β’
{β¨π, πβ© β£ ((π β π β§ π β π) β§ (π β πΆ β§ π β πΆ β§ (π β (πΆπΌπ) β¨ π β (πΆπΌπ))))} β (π Γ π) |
54 | 52, 53 | ssexi 5321 |
. . . . 5
β’
{β¨π, πβ© β£ ((π β π β§ π β π) β§ (π β πΆ β§ π β πΆ β§ (π β (πΆπΌπ) β¨ π β (πΆπΌπ))))} β V |
55 | 54 | a1i 11 |
. . . 4
β’ (π β {β¨π, πβ© β£ ((π β π β§ π β π) β§ (π β πΆ β§ π β πΆ β§ (π β (πΆπΌπ) β¨ π β (πΆπΌπ))))} β V) |
56 | 38, 49, 50, 55 | fvmptd 7001 |
. . 3
β’ (π β (πΎβπΆ) = {β¨π, πβ© β£ ((π β π β§ π β π) β§ (π β πΆ β§ π β πΆ β§ (π β (πΆπΌπ) β¨ π β (πΆπΌπ))))}) |
57 | 56 | breqd 5158 |
. 2
β’ (π β (π΄(πΎβπΆ)π΅ β π΄{β¨π, πβ© β£ ((π β π β§ π β π) β§ (π β πΆ β§ π β πΆ β§ (π β (πΆπΌπ) β¨ π β (πΆπΌπ))))}π΅)) |
58 | | ishlg.a |
. . . 4
β’ (π β π΄ β π) |
59 | | ishlg.b |
. . . 4
β’ (π β π΅ β π) |
60 | 58, 59 | jca 513 |
. . 3
β’ (π β (π΄ β π β§ π΅ β π)) |
61 | 60 | biantrurd 534 |
. 2
β’ (π β ((π΄ β πΆ β§ π΅ β πΆ β§ (π΄ β (πΆπΌπ΅) β¨ π΅ β (πΆπΌπ΄))) β ((π΄ β π β§ π΅ β π) β§ (π΄ β πΆ β§ π΅ β πΆ β§ (π΄ β (πΆπΌπ΅) β¨ π΅ β (πΆπΌπ΄)))))) |
62 | 13, 57, 61 | 3bitr4d 311 |
1
β’ (π β (π΄(πΎβπΆ)π΅ β (π΄ β πΆ β§ π΅ β πΆ β§ (π΄ β (πΆπΌπ΅) β¨ π΅ β (πΆπΌπ΄))))) |