Step | Hyp | Ref
| Expression |
1 | | iscgrg.e |
. . . 4
β’ βΌ =
(cgrGβπΊ) |
2 | | elex 3493 |
. . . . 5
β’ (πΊ β π β πΊ β V) |
3 | | fveq2 6892 |
. . . . . . . . . . . 12
β’ (π = πΊ β (Baseβπ) = (BaseβπΊ)) |
4 | | iscgrg.p |
. . . . . . . . . . . 12
β’ π = (BaseβπΊ) |
5 | 3, 4 | eqtr4di 2791 |
. . . . . . . . . . 11
β’ (π = πΊ β (Baseβπ) = π) |
6 | 5 | oveq1d 7424 |
. . . . . . . . . 10
β’ (π = πΊ β ((Baseβπ) βpm β) = (π βpm
β)) |
7 | 6 | eleq2d 2820 |
. . . . . . . . 9
β’ (π = πΊ β (π β ((Baseβπ) βpm β) β π β (π βpm
β))) |
8 | 6 | eleq2d 2820 |
. . . . . . . . 9
β’ (π = πΊ β (π β ((Baseβπ) βpm β) β π β (π βpm
β))) |
9 | 7, 8 | anbi12d 632 |
. . . . . . . 8
β’ (π = πΊ β ((π β ((Baseβπ) βpm β) β§ π β ((Baseβπ) βpm β))
β (π β (π βpm β)
β§ π β (π βpm
β)))) |
10 | | fveq2 6892 |
. . . . . . . . . . . . 13
β’ (π = πΊ β (distβπ) = (distβπΊ)) |
11 | | iscgrg.m |
. . . . . . . . . . . . 13
β’ β =
(distβπΊ) |
12 | 10, 11 | eqtr4di 2791 |
. . . . . . . . . . . 12
β’ (π = πΊ β (distβπ) = β ) |
13 | 12 | oveqd 7426 |
. . . . . . . . . . 11
β’ (π = πΊ β ((πβπ)(distβπ)(πβπ)) = ((πβπ) β (πβπ))) |
14 | 12 | oveqd 7426 |
. . . . . . . . . . 11
β’ (π = πΊ β ((πβπ)(distβπ)(πβπ)) = ((πβπ) β (πβπ))) |
15 | 13, 14 | eqeq12d 2749 |
. . . . . . . . . 10
β’ (π = πΊ β (((πβπ)(distβπ)(πβπ)) = ((πβπ)(distβπ)(πβπ)) β ((πβπ) β (πβπ)) = ((πβπ) β (πβπ)))) |
16 | 15 | 2ralbidv 3219 |
. . . . . . . . 9
β’ (π = πΊ β (βπ β dom πβπ β dom π((πβπ)(distβπ)(πβπ)) = ((πβπ)(distβπ)(πβπ)) β βπ β dom πβπ β dom π((πβπ) β (πβπ)) = ((πβπ) β (πβπ)))) |
17 | 16 | anbi2d 630 |
. . . . . . . 8
β’ (π = πΊ β ((dom π = dom π β§ βπ β dom πβπ β dom π((πβπ)(distβπ)(πβπ)) = ((πβπ)(distβπ)(πβπ))) β (dom π = dom π β§ βπ β dom πβπ β dom π((πβπ) β (πβπ)) = ((πβπ) β (πβπ))))) |
18 | 9, 17 | anbi12d 632 |
. . . . . . 7
β’ (π = πΊ β (((π β ((Baseβπ) βpm β) β§ π β ((Baseβπ) βpm β))
β§ (dom π = dom π β§ βπ β dom πβπ β dom π((πβπ)(distβπ)(πβπ)) = ((πβπ)(distβπ)(πβπ)))) β ((π β (π βpm β) β§ π β (π βpm β)) β§ (dom
π = dom π β§ βπ β dom πβπ β dom π((πβπ) β (πβπ)) = ((πβπ) β (πβπ)))))) |
19 | 18 | opabbidv 5215 |
. . . . . 6
β’ (π = πΊ β {β¨π, πβ© β£ ((π β ((Baseβπ) βpm β) β§ π β ((Baseβπ) βpm β))
β§ (dom π = dom π β§ βπ β dom πβπ β dom π((πβπ)(distβπ)(πβπ)) = ((πβπ)(distβπ)(πβπ))))} = {β¨π, πβ© β£ ((π β (π βpm β) β§ π β (π βpm β)) β§ (dom
π = dom π β§ βπ β dom πβπ β dom π((πβπ) β (πβπ)) = ((πβπ) β (πβπ))))}) |
20 | | df-cgrg 27762 |
. . . . . 6
β’ cgrG =
(π β V β¦
{β¨π, πβ© β£ ((π β ((Baseβπ) βpm β)
β§ π β
((Baseβπ)
βpm β)) β§ (dom π = dom π β§ βπ β dom πβπ β dom π((πβπ)(distβπ)(πβπ)) = ((πβπ)(distβπ)(πβπ))))}) |
21 | | df-xp 5683 |
. . . . . . . 8
β’ ((π βpm β)
Γ (π
βpm β)) = {β¨π, πβ© β£ (π β (π βpm β) β§ π β (π βpm
β))} |
22 | | ovex 7442 |
. . . . . . . . 9
β’ (π βpm β)
β V |
23 | 22, 22 | xpex 7740 |
. . . . . . . 8
β’ ((π βpm β)
Γ (π
βpm β)) β V |
24 | 21, 23 | eqeltrri 2831 |
. . . . . . 7
β’
{β¨π, πβ© β£ (π β (π βpm β) β§ π β (π βpm β))} β
V |
25 | | simpl 484 |
. . . . . . . 8
β’ (((π β (π βpm β) β§ π β (π βpm β)) β§ (dom
π = dom π β§ βπ β dom πβπ β dom π((πβπ) β (πβπ)) = ((πβπ) β (πβπ)))) β (π β (π βpm β) β§ π β (π βpm
β))) |
26 | 25 | ssopab2i 5551 |
. . . . . . 7
β’
{β¨π, πβ© β£ ((π β (π βpm β) β§ π β (π βpm β)) β§ (dom
π = dom π β§ βπ β dom πβπ β dom π((πβπ) β (πβπ)) = ((πβπ) β (πβπ))))} β {β¨π, πβ© β£ (π β (π βpm β) β§ π β (π βpm
β))} |
27 | 24, 26 | ssexi 5323 |
. . . . . 6
β’
{β¨π, πβ© β£ ((π β (π βpm β) β§ π β (π βpm β)) β§ (dom
π = dom π β§ βπ β dom πβπ β dom π((πβπ) β (πβπ)) = ((πβπ) β (πβπ))))} β V |
28 | 19, 20, 27 | fvmpt 6999 |
. . . . 5
β’ (πΊ β V β
(cgrGβπΊ) =
{β¨π, πβ© β£ ((π β (π βpm β) β§ π β (π βpm β)) β§ (dom
π = dom π β§ βπ β dom πβπ β dom π((πβπ) β (πβπ)) = ((πβπ) β (πβπ))))}) |
29 | 2, 28 | syl 17 |
. . . 4
β’ (πΊ β π β (cgrGβπΊ) = {β¨π, πβ© β£ ((π β (π βpm β) β§ π β (π βpm β)) β§ (dom
π = dom π β§ βπ β dom πβπ β dom π((πβπ) β (πβπ)) = ((πβπ) β (πβπ))))}) |
30 | 1, 29 | eqtrid 2785 |
. . 3
β’ (πΊ β π β βΌ = {β¨π, πβ© β£ ((π β (π βpm β) β§ π β (π βpm β)) β§ (dom
π = dom π β§ βπ β dom πβπ β dom π((πβπ) β (πβπ)) = ((πβπ) β (πβπ))))}) |
31 | 30 | breqd 5160 |
. 2
β’ (πΊ β π β (π΄ βΌ π΅ β π΄{β¨π, πβ© β£ ((π β (π βpm β) β§ π β (π βpm β)) β§ (dom
π = dom π β§ βπ β dom πβπ β dom π((πβπ) β (πβπ)) = ((πβπ) β (πβπ))))}π΅)) |
32 | | dmeq 5904 |
. . . . . 6
β’ (π = π΄ β dom π = dom π΄) |
33 | 32 | eqeq1d 2735 |
. . . . 5
β’ (π = π΄ β (dom π = dom π β dom π΄ = dom π)) |
34 | 32 | adantr 482 |
. . . . . . 7
β’ ((π = π΄ β§ π β dom π) β dom π = dom π΄) |
35 | | simpll 766 |
. . . . . . . . . 10
β’ (((π = π΄ β§ π β dom π) β§ π β dom π) β π = π΄) |
36 | 35 | fveq1d 6894 |
. . . . . . . . 9
β’ (((π = π΄ β§ π β dom π) β§ π β dom π) β (πβπ) = (π΄βπ)) |
37 | 35 | fveq1d 6894 |
. . . . . . . . 9
β’ (((π = π΄ β§ π β dom π) β§ π β dom π) β (πβπ) = (π΄βπ)) |
38 | 36, 37 | oveq12d 7427 |
. . . . . . . 8
β’ (((π = π΄ β§ π β dom π) β§ π β dom π) β ((πβπ) β (πβπ)) = ((π΄βπ) β (π΄βπ))) |
39 | 38 | eqeq1d 2735 |
. . . . . . 7
β’ (((π = π΄ β§ π β dom π) β§ π β dom π) β (((πβπ) β (πβπ)) = ((πβπ) β (πβπ)) β ((π΄βπ) β (π΄βπ)) = ((πβπ) β (πβπ)))) |
40 | 34, 39 | raleqbidva 3328 |
. . . . . 6
β’ ((π = π΄ β§ π β dom π) β (βπ β dom π((πβπ) β (πβπ)) = ((πβπ) β (πβπ)) β βπ β dom π΄((π΄βπ) β (π΄βπ)) = ((πβπ) β (πβπ)))) |
41 | 32, 40 | raleqbidva 3328 |
. . . . 5
β’ (π = π΄ β (βπ β dom πβπ β dom π((πβπ) β (πβπ)) = ((πβπ) β (πβπ)) β βπ β dom π΄βπ β dom π΄((π΄βπ) β (π΄βπ)) = ((πβπ) β (πβπ)))) |
42 | 33, 41 | anbi12d 632 |
. . . 4
β’ (π = π΄ β ((dom π = dom π β§ βπ β dom πβπ β dom π((πβπ) β (πβπ)) = ((πβπ) β (πβπ))) β (dom π΄ = dom π β§ βπ β dom π΄βπ β dom π΄((π΄βπ) β (π΄βπ)) = ((πβπ) β (πβπ))))) |
43 | | dmeq 5904 |
. . . . . 6
β’ (π = π΅ β dom π = dom π΅) |
44 | 43 | eqeq2d 2744 |
. . . . 5
β’ (π = π΅ β (dom π΄ = dom π β dom π΄ = dom π΅)) |
45 | | fveq1 6891 |
. . . . . . . 8
β’ (π = π΅ β (πβπ) = (π΅βπ)) |
46 | | fveq1 6891 |
. . . . . . . 8
β’ (π = π΅ β (πβπ) = (π΅βπ)) |
47 | 45, 46 | oveq12d 7427 |
. . . . . . 7
β’ (π = π΅ β ((πβπ) β (πβπ)) = ((π΅βπ) β (π΅βπ))) |
48 | 47 | eqeq2d 2744 |
. . . . . 6
β’ (π = π΅ β (((π΄βπ) β (π΄βπ)) = ((πβπ) β (πβπ)) β ((π΄βπ) β (π΄βπ)) = ((π΅βπ) β (π΅βπ)))) |
49 | 48 | 2ralbidv 3219 |
. . . . 5
β’ (π = π΅ β (βπ β dom π΄βπ β dom π΄((π΄βπ) β (π΄βπ)) = ((πβπ) β (πβπ)) β βπ β dom π΄βπ β dom π΄((π΄βπ) β (π΄βπ)) = ((π΅βπ) β (π΅βπ)))) |
50 | 44, 49 | anbi12d 632 |
. . . 4
β’ (π = π΅ β ((dom π΄ = dom π β§ βπ β dom π΄βπ β dom π΄((π΄βπ) β (π΄βπ)) = ((πβπ) β (πβπ))) β (dom π΄ = dom π΅ β§ βπ β dom π΄βπ β dom π΄((π΄βπ) β (π΄βπ)) = ((π΅βπ) β (π΅βπ))))) |
51 | 42, 50 | sylan9bb 511 |
. . 3
β’ ((π = π΄ β§ π = π΅) β ((dom π = dom π β§ βπ β dom πβπ β dom π((πβπ) β (πβπ)) = ((πβπ) β (πβπ))) β (dom π΄ = dom π΅ β§ βπ β dom π΄βπ β dom π΄((π΄βπ) β (π΄βπ)) = ((π΅βπ) β (π΅βπ))))) |
52 | | eqid 2733 |
. . 3
β’
{β¨π, πβ© β£ ((π β (π βpm β) β§ π β (π βpm β)) β§ (dom
π = dom π β§ βπ β dom πβπ β dom π((πβπ) β (πβπ)) = ((πβπ) β (πβπ))))} = {β¨π, πβ© β£ ((π β (π βpm β) β§ π β (π βpm β)) β§ (dom
π = dom π β§ βπ β dom πβπ β dom π((πβπ) β (πβπ)) = ((πβπ) β (πβπ))))} |
53 | 51, 52 | brab2a 5770 |
. 2
β’ (π΄{β¨π, πβ© β£ ((π β (π βpm β) β§ π β (π βpm β)) β§ (dom
π = dom π β§ βπ β dom πβπ β dom π((πβπ) β (πβπ)) = ((πβπ) β (πβπ))))}π΅ β ((π΄ β (π βpm β) β§ π΅ β (π βpm β)) β§ (dom
π΄ = dom π΅ β§ βπ β dom π΄βπ β dom π΄((π΄βπ) β (π΄βπ)) = ((π΅βπ) β (π΅βπ))))) |
54 | 31, 53 | bitrdi 287 |
1
β’ (πΊ β π β (π΄ βΌ π΅ β ((π΄ β (π βpm β) β§ π΅ β (π βpm β)) β§ (dom
π΄ = dom π΅ β§ βπ β dom π΄βπ β dom π΄((π΄βπ) β (π΄βπ)) = ((π΅βπ) β (π΅βπ)))))) |