Step | Hyp | Ref
| Expression |
1 | | wemapwe.u |
. . . . . . . . 9
β’ π = {π₯ β (π΅ βm π΄) β£ π₯ finSupp π} |
2 | | eqid 2737 |
. . . . . . . . 9
β’ {π₯ β (dom πΊ βm dom πΉ) β£ π₯ finSupp (β‘πΊβπ)} = {π₯ β (dom πΊ βm dom πΉ) β£ π₯ finSupp (β‘πΊβπ)} |
3 | | eqid 2737 |
. . . . . . . . 9
β’ (β‘πΊβπ) = (β‘πΊβπ) |
4 | | simprr 772 |
. . . . . . . . . . 11
β’ ((π β§ (π΅ β V β§ π΄ β V)) β π΄ β V) |
5 | | wemapwe.2 |
. . . . . . . . . . . 12
β’ (π β π
We π΄) |
6 | 5 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ (π΅ β V β§ π΄ β V)) β π
We π΄) |
7 | | wemapwe.5 |
. . . . . . . . . . . 12
β’ πΉ = OrdIso(π
, π΄) |
8 | 7 | oiiso 9480 |
. . . . . . . . . . 11
β’ ((π΄ β V β§ π
We π΄) β πΉ Isom E , π
(dom πΉ, π΄)) |
9 | 4, 6, 8 | syl2anc 585 |
. . . . . . . . . 10
β’ ((π β§ (π΅ β V β§ π΄ β V)) β πΉ Isom E , π
(dom πΉ, π΄)) |
10 | | isof1o 7273 |
. . . . . . . . . 10
β’ (πΉ Isom E , π
(dom πΉ, π΄) β πΉ:dom πΉβ1-1-ontoβπ΄) |
11 | 9, 10 | syl 17 |
. . . . . . . . 9
β’ ((π β§ (π΅ β V β§ π΄ β V)) β πΉ:dom πΉβ1-1-ontoβπ΄) |
12 | | simprl 770 |
. . . . . . . . . . 11
β’ ((π β§ (π΅ β V β§ π΄ β V)) β π΅ β V) |
13 | | wemapwe.3 |
. . . . . . . . . . . 12
β’ (π β π We π΅) |
14 | 13 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ (π΅ β V β§ π΄ β V)) β π We π΅) |
15 | | wemapwe.6 |
. . . . . . . . . . . 12
β’ πΊ = OrdIso(π, π΅) |
16 | 15 | oiiso 9480 |
. . . . . . . . . . 11
β’ ((π΅ β V β§ π We π΅) β πΊ Isom E , π (dom πΊ, π΅)) |
17 | 12, 14, 16 | syl2anc 585 |
. . . . . . . . . 10
β’ ((π β§ (π΅ β V β§ π΄ β V)) β πΊ Isom E , π (dom πΊ, π΅)) |
18 | | isof1o 7273 |
. . . . . . . . . 10
β’ (πΊ Isom E , π (dom πΊ, π΅) β πΊ:dom πΊβ1-1-ontoβπ΅) |
19 | | f1ocnv 6801 |
. . . . . . . . . 10
β’ (πΊ:dom πΊβ1-1-ontoβπ΅ β β‘πΊ:π΅β1-1-ontoβdom
πΊ) |
20 | 17, 18, 19 | 3syl 18 |
. . . . . . . . 9
β’ ((π β§ (π΅ β V β§ π΄ β V)) β β‘πΊ:π΅β1-1-ontoβdom
πΊ) |
21 | 7 | oiexg 9478 |
. . . . . . . . . . 11
β’ (π΄ β V β πΉ β V) |
22 | 21 | ad2antll 728 |
. . . . . . . . . 10
β’ ((π β§ (π΅ β V β§ π΄ β V)) β πΉ β V) |
23 | 22 | dmexd 7847 |
. . . . . . . . 9
β’ ((π β§ (π΅ β V β§ π΄ β V)) β dom πΉ β V) |
24 | 15 | oiexg 9478 |
. . . . . . . . . . 11
β’ (π΅ β V β πΊ β V) |
25 | 24 | ad2antrl 727 |
. . . . . . . . . 10
β’ ((π β§ (π΅ β V β§ π΄ β V)) β πΊ β V) |
26 | 25 | dmexd 7847 |
. . . . . . . . 9
β’ ((π β§ (π΅ β V β§ π΄ β V)) β dom πΊ β V) |
27 | | wemapwe.7 |
. . . . . . . . . 10
β’ π = (πΊββ
) |
28 | 17, 18 | syl 17 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π΅ β V β§ π΄ β V)) β πΊ:dom πΊβ1-1-ontoβπ΅) |
29 | | f1ofo 6796 |
. . . . . . . . . . . . . . 15
β’ (πΊ:dom πΊβ1-1-ontoβπ΅ β πΊ:dom πΊβontoβπ΅) |
30 | | forn 6764 |
. . . . . . . . . . . . . . 15
β’ (πΊ:dom πΊβontoβπ΅ β ran πΊ = π΅) |
31 | 28, 29, 30 | 3syl 18 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π΅ β V β§ π΄ β V)) β ran πΊ = π΅) |
32 | | wemapwe.4 |
. . . . . . . . . . . . . . 15
β’ (π β π΅ β β
) |
33 | 32 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π΅ β V β§ π΄ β V)) β π΅ β β
) |
34 | 31, 33 | eqnetrd 3012 |
. . . . . . . . . . . . 13
β’ ((π β§ (π΅ β V β§ π΄ β V)) β ran πΊ β β
) |
35 | | dm0rn0 5885 |
. . . . . . . . . . . . . 14
β’ (dom
πΊ = β
β ran
πΊ =
β
) |
36 | 35 | necon3bii 2997 |
. . . . . . . . . . . . 13
β’ (dom
πΊ β β
β ran
πΊ β
β
) |
37 | 34, 36 | sylibr 233 |
. . . . . . . . . . . 12
β’ ((π β§ (π΅ β V β§ π΄ β V)) β dom πΊ β β
) |
38 | 15 | oicl 9472 |
. . . . . . . . . . . . 13
β’ Ord dom
πΊ |
39 | | ord0eln0 6377 |
. . . . . . . . . . . . 13
β’ (Ord dom
πΊ β (β
β
dom πΊ β dom πΊ β β
)) |
40 | 38, 39 | ax-mp 5 |
. . . . . . . . . . . 12
β’ (β
β dom πΊ β dom
πΊ β
β
) |
41 | 37, 40 | sylibr 233 |
. . . . . . . . . . 11
β’ ((π β§ (π΅ β V β§ π΄ β V)) β β
β dom πΊ) |
42 | 15 | oif 9473 |
. . . . . . . . . . . 12
β’ πΊ:dom πΊβΆπ΅ |
43 | 42 | ffvelcdmi 7039 |
. . . . . . . . . . 11
β’ (β
β dom πΊ β (πΊββ
) β π΅) |
44 | 41, 43 | syl 17 |
. . . . . . . . . 10
β’ ((π β§ (π΅ β V β§ π΄ β V)) β (πΊββ
) β π΅) |
45 | 27, 44 | eqeltrid 2842 |
. . . . . . . . 9
β’ ((π β§ (π΅ β V β§ π΄ β V)) β π β π΅) |
46 | 1, 2, 3, 11, 20, 4, 12, 23, 26, 45 | mapfien 9351 |
. . . . . . . 8
β’ ((π β§ (π΅ β V β§ π΄ β V)) β (π β π β¦ (β‘πΊ β (π β πΉ))):πβ1-1-ontoβ{π₯ β (dom πΊ βm dom πΉ) β£ π₯ finSupp (β‘πΊβπ)}) |
47 | | eqid 2737 |
. . . . . . . . . . 11
β’ {π₯ β (dom πΊ βm dom πΉ) β£ π₯ finSupp β
} = {π₯ β (dom πΊ βm dom πΉ) β£ π₯ finSupp β
} |
48 | 15 | oion 9479 |
. . . . . . . . . . . 12
β’ (π΅ β V β dom πΊ β On) |
49 | 48 | ad2antrl 727 |
. . . . . . . . . . 11
β’ ((π β§ (π΅ β V β§ π΄ β V)) β dom πΊ β On) |
50 | 7 | oion 9479 |
. . . . . . . . . . . 12
β’ (π΄ β V β dom πΉ β On) |
51 | 50 | ad2antll 728 |
. . . . . . . . . . 11
β’ ((π β§ (π΅ β V β§ π΄ β V)) β dom πΉ β On) |
52 | 47, 49, 51 | cantnfdm 9607 |
. . . . . . . . . 10
β’ ((π β§ (π΅ β V β§ π΄ β V)) β dom (dom πΊ CNF dom πΉ) = {π₯ β (dom πΊ βm dom πΉ) β£ π₯ finSupp β
}) |
53 | 27 | fveq2i 6850 |
. . . . . . . . . . . . 13
β’ (β‘πΊβπ) = (β‘πΊβ(πΊββ
)) |
54 | | f1ocnvfv1 7227 |
. . . . . . . . . . . . . 14
β’ ((πΊ:dom πΊβ1-1-ontoβπ΅ β§ β
β dom πΊ) β (β‘πΊβ(πΊββ
)) = β
) |
55 | 28, 41, 54 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ ((π β§ (π΅ β V β§ π΄ β V)) β (β‘πΊβ(πΊββ
)) = β
) |
56 | 53, 55 | eqtrid 2789 |
. . . . . . . . . . . 12
β’ ((π β§ (π΅ β V β§ π΄ β V)) β (β‘πΊβπ) = β
) |
57 | 56 | breq2d 5122 |
. . . . . . . . . . 11
β’ ((π β§ (π΅ β V β§ π΄ β V)) β (π₯ finSupp (β‘πΊβπ) β π₯ finSupp β
)) |
58 | 57 | rabbidv 3418 |
. . . . . . . . . 10
β’ ((π β§ (π΅ β V β§ π΄ β V)) β {π₯ β (dom πΊ βm dom πΉ) β£ π₯ finSupp (β‘πΊβπ)} = {π₯ β (dom πΊ βm dom πΉ) β£ π₯ finSupp β
}) |
59 | 52, 58 | eqtr4d 2780 |
. . . . . . . . 9
β’ ((π β§ (π΅ β V β§ π΄ β V)) β dom (dom πΊ CNF dom πΉ) = {π₯ β (dom πΊ βm dom πΉ) β£ π₯ finSupp (β‘πΊβπ)}) |
60 | 59 | f1oeq3d 6786 |
. . . . . . . 8
β’ ((π β§ (π΅ β V β§ π΄ β V)) β ((π β π β¦ (β‘πΊ β (π β πΉ))):πβ1-1-ontoβdom
(dom πΊ CNF dom πΉ) β (π β π β¦ (β‘πΊ β (π β πΉ))):πβ1-1-ontoβ{π₯ β (dom πΊ βm dom πΉ) β£ π₯ finSupp (β‘πΊβπ)})) |
61 | 46, 60 | mpbird 257 |
. . . . . . 7
β’ ((π β§ (π΅ β V β§ π΄ β V)) β (π β π β¦ (β‘πΊ β (π β πΉ))):πβ1-1-ontoβdom
(dom πΊ CNF dom πΉ)) |
62 | | eqid 2737 |
. . . . . . . . 9
β’ dom (dom
πΊ CNF dom πΉ) = dom (dom πΊ CNF dom πΉ) |
63 | | eqid 2737 |
. . . . . . . . 9
β’
{β¨π, πβ© β£ βπ β dom πΉ((πβπ) β (πβπ) β§ βπ β dom πΉ(π β π β (πβπ) = (πβπ)))} = {β¨π, πβ© β£ βπ β dom πΉ((πβπ) β (πβπ) β§ βπ β dom πΉ(π β π β (πβπ) = (πβπ)))} |
64 | 62, 49, 51, 63 | oemapwe 9637 |
. . . . . . . 8
β’ ((π β§ (π΅ β V β§ π΄ β V)) β ({β¨π, πβ© β£ βπ β dom πΉ((πβπ) β (πβπ) β§ βπ β dom πΉ(π β π β (πβπ) = (πβπ)))} We dom (dom πΊ CNF dom πΉ) β§ dom OrdIso({β¨π, πβ© β£ βπ β dom πΉ((πβπ) β (πβπ) β§ βπ β dom πΉ(π β π β (πβπ) = (πβπ)))}, dom (dom πΊ CNF dom πΉ)) = (dom πΊ βo dom πΉ))) |
65 | 64 | simpld 496 |
. . . . . . 7
β’ ((π β§ (π΅ β V β§ π΄ β V)) β {β¨π, πβ© β£ βπ β dom πΉ((πβπ) β (πβπ) β§ βπ β dom πΉ(π β π β (πβπ) = (πβπ)))} We dom (dom πΊ CNF dom πΉ)) |
66 | | eqid 2737 |
. . . . . . . 8
β’
{β¨π₯, π¦β© β£ ((π β π β¦ (β‘πΊ β (π β πΉ)))βπ₯){β¨π, πβ© β£ βπ β dom πΉ((πβπ) β (πβπ) β§ βπ β dom πΉ(π β π β (πβπ) = (πβπ)))} ((π β π β¦ (β‘πΊ β (π β πΉ)))βπ¦)} = {β¨π₯, π¦β© β£ ((π β π β¦ (β‘πΊ β (π β πΉ)))βπ₯){β¨π, πβ© β£ βπ β dom πΉ((πβπ) β (πβπ) β§ βπ β dom πΉ(π β π β (πβπ) = (πβπ)))} ((π β π β¦ (β‘πΊ β (π β πΉ)))βπ¦)} |
67 | 66 | f1owe 7303 |
. . . . . . 7
β’ ((π β π β¦ (β‘πΊ β (π β πΉ))):πβ1-1-ontoβdom
(dom πΊ CNF dom πΉ) β ({β¨π, πβ© β£ βπ β dom πΉ((πβπ) β (πβπ) β§ βπ β dom πΉ(π β π β (πβπ) = (πβπ)))} We dom (dom πΊ CNF dom πΉ) β {β¨π₯, π¦β© β£ ((π β π β¦ (β‘πΊ β (π β πΉ)))βπ₯){β¨π, πβ© β£ βπ β dom πΉ((πβπ) β (πβπ) β§ βπ β dom πΉ(π β π β (πβπ) = (πβπ)))} ((π β π β¦ (β‘πΊ β (π β πΉ)))βπ¦)} We π)) |
68 | 61, 65, 67 | sylc 65 |
. . . . . 6
β’ ((π β§ (π΅ β V β§ π΄ β V)) β {β¨π₯, π¦β© β£ ((π β π β¦ (β‘πΊ β (π β πΉ)))βπ₯){β¨π, πβ© β£ βπ β dom πΉ((πβπ) β (πβπ) β§ βπ β dom πΉ(π β π β (πβπ) = (πβπ)))} ((π β π β¦ (β‘πΊ β (π β πΉ)))βπ¦)} We π) |
69 | | weinxp 5721 |
. . . . . 6
β’
({β¨π₯, π¦β© β£ ((π β π β¦ (β‘πΊ β (π β πΉ)))βπ₯){β¨π, πβ© β£ βπ β dom πΉ((πβπ) β (πβπ) β§ βπ β dom πΉ(π β π β (πβπ) = (πβπ)))} ((π β π β¦ (β‘πΊ β (π β πΉ)))βπ¦)} We π β ({β¨π₯, π¦β© β£ ((π β π β¦ (β‘πΊ β (π β πΉ)))βπ₯){β¨π, πβ© β£ βπ β dom πΉ((πβπ) β (πβπ) β§ βπ β dom πΉ(π β π β (πβπ) = (πβπ)))} ((π β π β¦ (β‘πΊ β (π β πΉ)))βπ¦)} β© (π Γ π)) We π) |
70 | 68, 69 | sylib 217 |
. . . . 5
β’ ((π β§ (π΅ β V β§ π΄ β V)) β ({β¨π₯, π¦β© β£ ((π β π β¦ (β‘πΊ β (π β πΉ)))βπ₯){β¨π, πβ© β£ βπ β dom πΉ((πβπ) β (πβπ) β§ βπ β dom πΉ(π β π β (πβπ) = (πβπ)))} ((π β π β¦ (β‘πΊ β (π β πΉ)))βπ¦)} β© (π Γ π)) We π) |
71 | 11 | adantr 482 |
. . . . . . . . . . . 12
β’ (((π β§ (π΅ β V β§ π΄ β V)) β§ (π₯ β π β§ π¦ β π)) β πΉ:dom πΉβ1-1-ontoβπ΄) |
72 | | f1ofn 6790 |
. . . . . . . . . . . 12
β’ (πΉ:dom πΉβ1-1-ontoβπ΄ β πΉ Fn dom πΉ) |
73 | | fveq2 6847 |
. . . . . . . . . . . . . . 15
β’ (π§ = (πΉβπ) β (π₯βπ§) = (π₯β(πΉβπ))) |
74 | | fveq2 6847 |
. . . . . . . . . . . . . . 15
β’ (π§ = (πΉβπ) β (π¦βπ§) = (π¦β(πΉβπ))) |
75 | 73, 74 | breq12d 5123 |
. . . . . . . . . . . . . 14
β’ (π§ = (πΉβπ) β ((π₯βπ§)π(π¦βπ§) β (π₯β(πΉβπ))π(π¦β(πΉβπ)))) |
76 | | breq1 5113 |
. . . . . . . . . . . . . . . 16
β’ (π§ = (πΉβπ) β (π§π
π€ β (πΉβπ)π
π€)) |
77 | 76 | imbi1d 342 |
. . . . . . . . . . . . . . 15
β’ (π§ = (πΉβπ) β ((π§π
π€ β (π₯βπ€) = (π¦βπ€)) β ((πΉβπ)π
π€ β (π₯βπ€) = (π¦βπ€)))) |
78 | 77 | ralbidv 3175 |
. . . . . . . . . . . . . 14
β’ (π§ = (πΉβπ) β (βπ€ β π΄ (π§π
π€ β (π₯βπ€) = (π¦βπ€)) β βπ€ β π΄ ((πΉβπ)π
π€ β (π₯βπ€) = (π¦βπ€)))) |
79 | 75, 78 | anbi12d 632 |
. . . . . . . . . . . . 13
β’ (π§ = (πΉβπ) β (((π₯βπ§)π(π¦βπ§) β§ βπ€ β π΄ (π§π
π€ β (π₯βπ€) = (π¦βπ€))) β ((π₯β(πΉβπ))π(π¦β(πΉβπ)) β§ βπ€ β π΄ ((πΉβπ)π
π€ β (π₯βπ€) = (π¦βπ€))))) |
80 | 79 | rexrn 7042 |
. . . . . . . . . . . 12
β’ (πΉ Fn dom πΉ β (βπ§ β ran πΉ((π₯βπ§)π(π¦βπ§) β§ βπ€ β π΄ (π§π
π€ β (π₯βπ€) = (π¦βπ€))) β βπ β dom πΉ((π₯β(πΉβπ))π(π¦β(πΉβπ)) β§ βπ€ β π΄ ((πΉβπ)π
π€ β (π₯βπ€) = (π¦βπ€))))) |
81 | 71, 72, 80 | 3syl 18 |
. . . . . . . . . . 11
β’ (((π β§ (π΅ β V β§ π΄ β V)) β§ (π₯ β π β§ π¦ β π)) β (βπ§ β ran πΉ((π₯βπ§)π(π¦βπ§) β§ βπ€ β π΄ (π§π
π€ β (π₯βπ€) = (π¦βπ€))) β βπ β dom πΉ((π₯β(πΉβπ))π(π¦β(πΉβπ)) β§ βπ€ β π΄ ((πΉβπ)π
π€ β (π₯βπ€) = (π¦βπ€))))) |
82 | | f1ofo 6796 |
. . . . . . . . . . . . 13
β’ (πΉ:dom πΉβ1-1-ontoβπ΄ β πΉ:dom πΉβontoβπ΄) |
83 | | forn 6764 |
. . . . . . . . . . . . 13
β’ (πΉ:dom πΉβontoβπ΄ β ran πΉ = π΄) |
84 | 71, 82, 83 | 3syl 18 |
. . . . . . . . . . . 12
β’ (((π β§ (π΅ β V β§ π΄ β V)) β§ (π₯ β π β§ π¦ β π)) β ran πΉ = π΄) |
85 | 84 | rexeqdv 3317 |
. . . . . . . . . . 11
β’ (((π β§ (π΅ β V β§ π΄ β V)) β§ (π₯ β π β§ π¦ β π)) β (βπ§ β ran πΉ((π₯βπ§)π(π¦βπ§) β§ βπ€ β π΄ (π§π
π€ β (π₯βπ€) = (π¦βπ€))) β βπ§ β π΄ ((π₯βπ§)π(π¦βπ§) β§ βπ€ β π΄ (π§π
π€ β (π₯βπ€) = (π¦βπ€))))) |
86 | 25 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π΅ β V β§ π΄ β V)) β§ (π₯ β π β§ π¦ β π)) β πΊ β V) |
87 | | cnvexg 7866 |
. . . . . . . . . . . . . . 15
β’ (πΊ β V β β‘πΊ β V) |
88 | 86, 87 | syl 17 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π΅ β V β§ π΄ β V)) β§ (π₯ β π β§ π¦ β π)) β β‘πΊ β V) |
89 | | vex 3452 |
. . . . . . . . . . . . . . 15
β’ π₯ β V |
90 | 22 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π΅ β V β§ π΄ β V)) β§ (π₯ β π β§ π¦ β π)) β πΉ β V) |
91 | | coexg 7871 |
. . . . . . . . . . . . . . 15
β’ ((π₯ β V β§ πΉ β V) β (π₯ β πΉ) β V) |
92 | 89, 90, 91 | sylancr 588 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π΅ β V β§ π΄ β V)) β§ (π₯ β π β§ π¦ β π)) β (π₯ β πΉ) β V) |
93 | | coexg 7871 |
. . . . . . . . . . . . . 14
β’ ((β‘πΊ β V β§ (π₯ β πΉ) β V) β (β‘πΊ β (π₯ β πΉ)) β V) |
94 | 88, 92, 93 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ (((π β§ (π΅ β V β§ π΄ β V)) β§ (π₯ β π β§ π¦ β π)) β (β‘πΊ β (π₯ β πΉ)) β V) |
95 | | vex 3452 |
. . . . . . . . . . . . . . 15
β’ π¦ β V |
96 | | coexg 7871 |
. . . . . . . . . . . . . . 15
β’ ((π¦ β V β§ πΉ β V) β (π¦ β πΉ) β V) |
97 | 95, 90, 96 | sylancr 588 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π΅ β V β§ π΄ β V)) β§ (π₯ β π β§ π¦ β π)) β (π¦ β πΉ) β V) |
98 | | coexg 7871 |
. . . . . . . . . . . . . 14
β’ ((β‘πΊ β V β§ (π¦ β πΉ) β V) β (β‘πΊ β (π¦ β πΉ)) β V) |
99 | 88, 97, 98 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ (((π β§ (π΅ β V β§ π΄ β V)) β§ (π₯ β π β§ π¦ β π)) β (β‘πΊ β (π¦ β πΉ)) β V) |
100 | | fveq1 6846 |
. . . . . . . . . . . . . . . . 17
β’ (π = (β‘πΊ β (π₯ β πΉ)) β (πβπ) = ((β‘πΊ β (π₯ β πΉ))βπ)) |
101 | | fveq1 6846 |
. . . . . . . . . . . . . . . . 17
β’ (π = (β‘πΊ β (π¦ β πΉ)) β (πβπ) = ((β‘πΊ β (π¦ β πΉ))βπ)) |
102 | | eleq12 2828 |
. . . . . . . . . . . . . . . . 17
β’ (((πβπ) = ((β‘πΊ β (π₯ β πΉ))βπ) β§ (πβπ) = ((β‘πΊ β (π¦ β πΉ))βπ)) β ((πβπ) β (πβπ) β ((β‘πΊ β (π₯ β πΉ))βπ) β ((β‘πΊ β (π¦ β πΉ))βπ))) |
103 | 100, 101,
102 | syl2an 597 |
. . . . . . . . . . . . . . . 16
β’ ((π = (β‘πΊ β (π₯ β πΉ)) β§ π = (β‘πΊ β (π¦ β πΉ))) β ((πβπ) β (πβπ) β ((β‘πΊ β (π₯ β πΉ))βπ) β ((β‘πΊ β (π¦ β πΉ))βπ))) |
104 | | fveq1 6846 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = (β‘πΊ β (π₯ β πΉ)) β (πβπ) = ((β‘πΊ β (π₯ β πΉ))βπ)) |
105 | | fveq1 6846 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = (β‘πΊ β (π¦ β πΉ)) β (πβπ) = ((β‘πΊ β (π¦ β πΉ))βπ)) |
106 | 104, 105 | eqeqan12d 2751 |
. . . . . . . . . . . . . . . . . 18
β’ ((π = (β‘πΊ β (π₯ β πΉ)) β§ π = (β‘πΊ β (π¦ β πΉ))) β ((πβπ) = (πβπ) β ((β‘πΊ β (π₯ β πΉ))βπ) = ((β‘πΊ β (π¦ β πΉ))βπ))) |
107 | 106 | imbi2d 341 |
. . . . . . . . . . . . . . . . 17
β’ ((π = (β‘πΊ β (π₯ β πΉ)) β§ π = (β‘πΊ β (π¦ β πΉ))) β ((π β π β (πβπ) = (πβπ)) β (π β π β ((β‘πΊ β (π₯ β πΉ))βπ) = ((β‘πΊ β (π¦ β πΉ))βπ)))) |
108 | 107 | ralbidv 3175 |
. . . . . . . . . . . . . . . 16
β’ ((π = (β‘πΊ β (π₯ β πΉ)) β§ π = (β‘πΊ β (π¦ β πΉ))) β (βπ β dom πΉ(π β π β (πβπ) = (πβπ)) β βπ β dom πΉ(π β π β ((β‘πΊ β (π₯ β πΉ))βπ) = ((β‘πΊ β (π¦ β πΉ))βπ)))) |
109 | 103, 108 | anbi12d 632 |
. . . . . . . . . . . . . . 15
β’ ((π = (β‘πΊ β (π₯ β πΉ)) β§ π = (β‘πΊ β (π¦ β πΉ))) β (((πβπ) β (πβπ) β§ βπ β dom πΉ(π β π β (πβπ) = (πβπ))) β (((β‘πΊ β (π₯ β πΉ))βπ) β ((β‘πΊ β (π¦ β πΉ))βπ) β§ βπ β dom πΉ(π β π β ((β‘πΊ β (π₯ β πΉ))βπ) = ((β‘πΊ β (π¦ β πΉ))βπ))))) |
110 | 109 | rexbidv 3176 |
. . . . . . . . . . . . . 14
β’ ((π = (β‘πΊ β (π₯ β πΉ)) β§ π = (β‘πΊ β (π¦ β πΉ))) β (βπ β dom πΉ((πβπ) β (πβπ) β§ βπ β dom πΉ(π β π β (πβπ) = (πβπ))) β βπ β dom πΉ(((β‘πΊ β (π₯ β πΉ))βπ) β ((β‘πΊ β (π¦ β πΉ))βπ) β§ βπ β dom πΉ(π β π β ((β‘πΊ β (π₯ β πΉ))βπ) = ((β‘πΊ β (π¦ β πΉ))βπ))))) |
111 | 110, 63 | brabga 5496 |
. . . . . . . . . . . . 13
β’ (((β‘πΊ β (π₯ β πΉ)) β V β§ (β‘πΊ β (π¦ β πΉ)) β V) β ((β‘πΊ β (π₯ β πΉ)){β¨π, πβ© β£ βπ β dom πΉ((πβπ) β (πβπ) β§ βπ β dom πΉ(π β π β (πβπ) = (πβπ)))} (β‘πΊ β (π¦ β πΉ)) β βπ β dom πΉ(((β‘πΊ β (π₯ β πΉ))βπ) β ((β‘πΊ β (π¦ β πΉ))βπ) β§ βπ β dom πΉ(π β π β ((β‘πΊ β (π₯ β πΉ))βπ) = ((β‘πΊ β (π¦ β πΉ))βπ))))) |
112 | 94, 99, 111 | syl2anc 585 |
. . . . . . . . . . . 12
β’ (((π β§ (π΅ β V β§ π΄ β V)) β§ (π₯ β π β§ π¦ β π)) β ((β‘πΊ β (π₯ β πΉ)){β¨π, πβ© β£ βπ β dom πΉ((πβπ) β (πβπ) β§ βπ β dom πΉ(π β π β (πβπ) = (πβπ)))} (β‘πΊ β (π¦ β πΉ)) β βπ β dom πΉ(((β‘πΊ β (π₯ β πΉ))βπ) β ((β‘πΊ β (π¦ β πΉ))βπ) β§ βπ β dom πΉ(π β π β ((β‘πΊ β (π₯ β πΉ))βπ) = ((β‘πΊ β (π¦ β πΉ))βπ))))) |
113 | | eqid 2737 |
. . . . . . . . . . . . . 14
β’ (π β π β¦ (β‘πΊ β (π β πΉ))) = (π β π β¦ (β‘πΊ β (π β πΉ))) |
114 | | coeq1 5818 |
. . . . . . . . . . . . . . 15
β’ (π = π₯ β (π β πΉ) = (π₯ β πΉ)) |
115 | 114 | coeq2d 5823 |
. . . . . . . . . . . . . 14
β’ (π = π₯ β (β‘πΊ β (π β πΉ)) = (β‘πΊ β (π₯ β πΉ))) |
116 | | simprl 770 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π΅ β V β§ π΄ β V)) β§ (π₯ β π β§ π¦ β π)) β π₯ β π) |
117 | 113, 115,
116, 94 | fvmptd3 6976 |
. . . . . . . . . . . . 13
β’ (((π β§ (π΅ β V β§ π΄ β V)) β§ (π₯ β π β§ π¦ β π)) β ((π β π β¦ (β‘πΊ β (π β πΉ)))βπ₯) = (β‘πΊ β (π₯ β πΉ))) |
118 | | coeq1 5818 |
. . . . . . . . . . . . . . 15
β’ (π = π¦ β (π β πΉ) = (π¦ β πΉ)) |
119 | 118 | coeq2d 5823 |
. . . . . . . . . . . . . 14
β’ (π = π¦ β (β‘πΊ β (π β πΉ)) = (β‘πΊ β (π¦ β πΉ))) |
120 | | simprr 772 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π΅ β V β§ π΄ β V)) β§ (π₯ β π β§ π¦ β π)) β π¦ β π) |
121 | 113, 119,
120, 99 | fvmptd3 6976 |
. . . . . . . . . . . . 13
β’ (((π β§ (π΅ β V β§ π΄ β V)) β§ (π₯ β π β§ π¦ β π)) β ((π β π β¦ (β‘πΊ β (π β πΉ)))βπ¦) = (β‘πΊ β (π¦ β πΉ))) |
122 | 117, 121 | breq12d 5123 |
. . . . . . . . . . . 12
β’ (((π β§ (π΅ β V β§ π΄ β V)) β§ (π₯ β π β§ π¦ β π)) β (((π β π β¦ (β‘πΊ β (π β πΉ)))βπ₯){β¨π, πβ© β£ βπ β dom πΉ((πβπ) β (πβπ) β§ βπ β dom πΉ(π β π β (πβπ) = (πβπ)))} ((π β π β¦ (β‘πΊ β (π β πΉ)))βπ¦) β (β‘πΊ β (π₯ β πΉ)){β¨π, πβ© β£ βπ β dom πΉ((πβπ) β (πβπ) β§ βπ β dom πΉ(π β π β (πβπ) = (πβπ)))} (β‘πΊ β (π¦ β πΉ)))) |
123 | 17 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ (π΅ β V β§ π΄ β V)) β§ (π₯ β π β§ π¦ β π)) β§ π β dom πΉ) β πΊ Isom E , π (dom πΊ, π΅)) |
124 | | isocnv 7280 |
. . . . . . . . . . . . . . . . . 18
β’ (πΊ Isom E , π (dom πΊ, π΅) β β‘πΊ Isom π, E (π΅, dom πΊ)) |
125 | 123, 124 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ (π΅ β V β§ π΄ β V)) β§ (π₯ β π β§ π¦ β π)) β§ π β dom πΉ) β β‘πΊ Isom π, E (π΅, dom πΊ)) |
126 | 1 | ssrab3 4045 |
. . . . . . . . . . . . . . . . . . . 20
β’ π β (π΅ βm π΄) |
127 | 126, 116 | sselid 3947 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ (π΅ β V β§ π΄ β V)) β§ (π₯ β π β§ π¦ β π)) β π₯ β (π΅ βm π΄)) |
128 | | elmapi 8794 |
. . . . . . . . . . . . . . . . . . 19
β’ (π₯ β (π΅ βm π΄) β π₯:π΄βΆπ΅) |
129 | 127, 128 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ (π΅ β V β§ π΄ β V)) β§ (π₯ β π β§ π¦ β π)) β π₯:π΄βΆπ΅) |
130 | 7 | oif 9473 |
. . . . . . . . . . . . . . . . . . 19
β’ πΉ:dom πΉβΆπ΄ |
131 | 130 | ffvelcdmi 7039 |
. . . . . . . . . . . . . . . . . 18
β’ (π β dom πΉ β (πΉβπ) β π΄) |
132 | | ffvelcdm 7037 |
. . . . . . . . . . . . . . . . . 18
β’ ((π₯:π΄βΆπ΅ β§ (πΉβπ) β π΄) β (π₯β(πΉβπ)) β π΅) |
133 | 129, 131,
132 | syl2an 597 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ (π΅ β V β§ π΄ β V)) β§ (π₯ β π β§ π¦ β π)) β§ π β dom πΉ) β (π₯β(πΉβπ)) β π΅) |
134 | 126, 120 | sselid 3947 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ (π΅ β V β§ π΄ β V)) β§ (π₯ β π β§ π¦ β π)) β π¦ β (π΅ βm π΄)) |
135 | | elmapi 8794 |
. . . . . . . . . . . . . . . . . . 19
β’ (π¦ β (π΅ βm π΄) β π¦:π΄βΆπ΅) |
136 | 134, 135 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ (π΅ β V β§ π΄ β V)) β§ (π₯ β π β§ π¦ β π)) β π¦:π΄βΆπ΅) |
137 | | ffvelcdm 7037 |
. . . . . . . . . . . . . . . . . 18
β’ ((π¦:π΄βΆπ΅ β§ (πΉβπ) β π΄) β (π¦β(πΉβπ)) β π΅) |
138 | 136, 131,
137 | syl2an 597 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ (π΅ β V β§ π΄ β V)) β§ (π₯ β π β§ π¦ β π)) β§ π β dom πΉ) β (π¦β(πΉβπ)) β π΅) |
139 | | isorel 7276 |
. . . . . . . . . . . . . . . . 17
β’ ((β‘πΊ Isom π, E (π΅, dom πΊ) β§ ((π₯β(πΉβπ)) β π΅ β§ (π¦β(πΉβπ)) β π΅)) β ((π₯β(πΉβπ))π(π¦β(πΉβπ)) β (β‘πΊβ(π₯β(πΉβπ))) E (β‘πΊβ(π¦β(πΉβπ))))) |
140 | 125, 133,
138, 139 | syl12anc 836 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ (π΅ β V β§ π΄ β V)) β§ (π₯ β π β§ π¦ β π)) β§ π β dom πΉ) β ((π₯β(πΉβπ))π(π¦β(πΉβπ)) β (β‘πΊβ(π₯β(πΉβπ))) E (β‘πΊβ(π¦β(πΉβπ))))) |
141 | | fvex 6860 |
. . . . . . . . . . . . . . . . 17
β’ (β‘πΊβ(π¦β(πΉβπ))) β V |
142 | 141 | epeli 5544 |
. . . . . . . . . . . . . . . 16
β’ ((β‘πΊβ(π₯β(πΉβπ))) E (β‘πΊβ(π¦β(πΉβπ))) β (β‘πΊβ(π₯β(πΉβπ))) β (β‘πΊβ(π¦β(πΉβπ)))) |
143 | 140, 142 | bitrdi 287 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ (π΅ β V β§ π΄ β V)) β§ (π₯ β π β§ π¦ β π)) β§ π β dom πΉ) β ((π₯β(πΉβπ))π(π¦β(πΉβπ)) β (β‘πΊβ(π₯β(πΉβπ))) β (β‘πΊβ(π¦β(πΉβπ))))) |
144 | 129 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ (π΅ β V β§ π΄ β V)) β§ (π₯ β π β§ π¦ β π)) β§ π β dom πΉ) β π₯:π΄βΆπ΅) |
145 | | fco 6697 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π₯:π΄βΆπ΅ β§ πΉ:dom πΉβΆπ΄) β (π₯ β πΉ):dom πΉβΆπ΅) |
146 | 144, 130,
145 | sylancl 587 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ (π΅ β V β§ π΄ β V)) β§ (π₯ β π β§ π¦ β π)) β§ π β dom πΉ) β (π₯ β πΉ):dom πΉβΆπ΅) |
147 | | fvco3 6945 |
. . . . . . . . . . . . . . . . . 18
β’ (((π₯ β πΉ):dom πΉβΆπ΅ β§ π β dom πΉ) β ((β‘πΊ β (π₯ β πΉ))βπ) = (β‘πΊβ((π₯ β πΉ)βπ))) |
148 | 146, 147 | sylancom 589 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ (π΅ β V β§ π΄ β V)) β§ (π₯ β π β§ π¦ β π)) β§ π β dom πΉ) β ((β‘πΊ β (π₯ β πΉ))βπ) = (β‘πΊβ((π₯ β πΉ)βπ))) |
149 | | simpr 486 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ (π΅ β V β§ π΄ β V)) β§ (π₯ β π β§ π¦ β π)) β§ π β dom πΉ) β π β dom πΉ) |
150 | | fvco3 6945 |
. . . . . . . . . . . . . . . . . . 19
β’ ((πΉ:dom πΉβΆπ΄ β§ π β dom πΉ) β ((π₯ β πΉ)βπ) = (π₯β(πΉβπ))) |
151 | 130, 149,
150 | sylancr 588 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ (π΅ β V β§ π΄ β V)) β§ (π₯ β π β§ π¦ β π)) β§ π β dom πΉ) β ((π₯ β πΉ)βπ) = (π₯β(πΉβπ))) |
152 | 151 | fveq2d 6851 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ (π΅ β V β§ π΄ β V)) β§ (π₯ β π β§ π¦ β π)) β§ π β dom πΉ) β (β‘πΊβ((π₯ β πΉ)βπ)) = (β‘πΊβ(π₯β(πΉβπ)))) |
153 | 148, 152 | eqtrd 2777 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ (π΅ β V β§ π΄ β V)) β§ (π₯ β π β§ π¦ β π)) β§ π β dom πΉ) β ((β‘πΊ β (π₯ β πΉ))βπ) = (β‘πΊβ(π₯β(πΉβπ)))) |
154 | 136 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ (π΅ β V β§ π΄ β V)) β§ (π₯ β π β§ π¦ β π)) β§ π β dom πΉ) β π¦:π΄βΆπ΅) |
155 | | fco 6697 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π¦:π΄βΆπ΅ β§ πΉ:dom πΉβΆπ΄) β (π¦ β πΉ):dom πΉβΆπ΅) |
156 | 154, 130,
155 | sylancl 587 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ (π΅ β V β§ π΄ β V)) β§ (π₯ β π β§ π¦ β π)) β§ π β dom πΉ) β (π¦ β πΉ):dom πΉβΆπ΅) |
157 | | fvco3 6945 |
. . . . . . . . . . . . . . . . . 18
β’ (((π¦ β πΉ):dom πΉβΆπ΅ β§ π β dom πΉ) β ((β‘πΊ β (π¦ β πΉ))βπ) = (β‘πΊβ((π¦ β πΉ)βπ))) |
158 | 156, 157 | sylancom 589 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ (π΅ β V β§ π΄ β V)) β§ (π₯ β π β§ π¦ β π)) β§ π β dom πΉ) β ((β‘πΊ β (π¦ β πΉ))βπ) = (β‘πΊβ((π¦ β πΉ)βπ))) |
159 | | fvco3 6945 |
. . . . . . . . . . . . . . . . . . 19
β’ ((πΉ:dom πΉβΆπ΄ β§ π β dom πΉ) β ((π¦ β πΉ)βπ) = (π¦β(πΉβπ))) |
160 | 130, 149,
159 | sylancr 588 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ (π΅ β V β§ π΄ β V)) β§ (π₯ β π β§ π¦ β π)) β§ π β dom πΉ) β ((π¦ β πΉ)βπ) = (π¦β(πΉβπ))) |
161 | 160 | fveq2d 6851 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ (π΅ β V β§ π΄ β V)) β§ (π₯ β π β§ π¦ β π)) β§ π β dom πΉ) β (β‘πΊβ((π¦ β πΉ)βπ)) = (β‘πΊβ(π¦β(πΉβπ)))) |
162 | 158, 161 | eqtrd 2777 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ (π΅ β V β§ π΄ β V)) β§ (π₯ β π β§ π¦ β π)) β§ π β dom πΉ) β ((β‘πΊ β (π¦ β πΉ))βπ) = (β‘πΊβ(π¦β(πΉβπ)))) |
163 | 153, 162 | eleq12d 2832 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ (π΅ β V β§ π΄ β V)) β§ (π₯ β π β§ π¦ β π)) β§ π β dom πΉ) β (((β‘πΊ β (π₯ β πΉ))βπ) β ((β‘πΊ β (π¦ β πΉ))βπ) β (β‘πΊβ(π₯β(πΉβπ))) β (β‘πΊβ(π¦β(πΉβπ))))) |
164 | 143, 163 | bitr4d 282 |
. . . . . . . . . . . . . 14
β’ ((((π β§ (π΅ β V β§ π΄ β V)) β§ (π₯ β π β§ π¦ β π)) β§ π β dom πΉ) β ((π₯β(πΉβπ))π(π¦β(πΉβπ)) β ((β‘πΊ β (π₯ β πΉ))βπ) β ((β‘πΊ β (π¦ β πΉ))βπ))) |
165 | 84 | raleqdv 3316 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (π΅ β V β§ π΄ β V)) β§ (π₯ β π β§ π¦ β π)) β (βπ€ β ran πΉ((πΉβπ)π
π€ β (π₯βπ€) = (π¦βπ€)) β βπ€ β π΄ ((πΉβπ)π
π€ β (π₯βπ€) = (π¦βπ€)))) |
166 | | breq2 5114 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π€ = (πΉβπ) β ((πΉβπ)π
π€ β (πΉβπ)π
(πΉβπ))) |
167 | | fveq2 6847 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π€ = (πΉβπ) β (π₯βπ€) = (π₯β(πΉβπ))) |
168 | | fveq2 6847 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π€ = (πΉβπ) β (π¦βπ€) = (π¦β(πΉβπ))) |
169 | 167, 168 | eqeq12d 2753 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π€ = (πΉβπ) β ((π₯βπ€) = (π¦βπ€) β (π₯β(πΉβπ)) = (π¦β(πΉβπ)))) |
170 | 166, 169 | imbi12d 345 |
. . . . . . . . . . . . . . . . . . 19
β’ (π€ = (πΉβπ) β (((πΉβπ)π
π€ β (π₯βπ€) = (π¦βπ€)) β ((πΉβπ)π
(πΉβπ) β (π₯β(πΉβπ)) = (π¦β(πΉβπ))))) |
171 | 170 | ralrn 7043 |
. . . . . . . . . . . . . . . . . 18
β’ (πΉ Fn dom πΉ β (βπ€ β ran πΉ((πΉβπ)π
π€ β (π₯βπ€) = (π¦βπ€)) β βπ β dom πΉ((πΉβπ)π
(πΉβπ) β (π₯β(πΉβπ)) = (π¦β(πΉβπ))))) |
172 | 71, 72, 171 | 3syl 18 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (π΅ β V β§ π΄ β V)) β§ (π₯ β π β§ π¦ β π)) β (βπ€ β ran πΉ((πΉβπ)π
π€ β (π₯βπ€) = (π¦βπ€)) β βπ β dom πΉ((πΉβπ)π
(πΉβπ) β (π₯β(πΉβπ)) = (π¦β(πΉβπ))))) |
173 | 165, 172 | bitr3d 281 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π΅ β V β§ π΄ β V)) β§ (π₯ β π β§ π¦ β π)) β (βπ€ β π΄ ((πΉβπ)π
π€ β (π₯βπ€) = (π¦βπ€)) β βπ β dom πΉ((πΉβπ)π
(πΉβπ) β (π₯β(πΉβπ)) = (π¦β(πΉβπ))))) |
174 | 173 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ (π΅ β V β§ π΄ β V)) β§ (π₯ β π β§ π¦ β π)) β§ π β dom πΉ) β (βπ€ β π΄ ((πΉβπ)π
π€ β (π₯βπ€) = (π¦βπ€)) β βπ β dom πΉ((πΉβπ)π
(πΉβπ) β (π₯β(πΉβπ)) = (π¦β(πΉβπ))))) |
175 | | epel 5545 |
. . . . . . . . . . . . . . . . . . 19
β’ (π E π β π β π) |
176 | 9 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ (π΅ β V β§ π΄ β V)) β§ (π₯ β π β§ π¦ β π)) β§ (π β dom πΉ β§ π β dom πΉ)) β πΉ Isom E , π
(dom πΉ, π΄)) |
177 | | isorel 7276 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((πΉ Isom E , π
(dom πΉ, π΄) β§ (π β dom πΉ β§ π β dom πΉ)) β (π E π β (πΉβπ)π
(πΉβπ))) |
178 | 176, 177 | sylancom 589 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ (π΅ β V β§ π΄ β V)) β§ (π₯ β π β§ π¦ β π)) β§ (π β dom πΉ β§ π β dom πΉ)) β (π E π β (πΉβπ)π
(πΉβπ))) |
179 | 175, 178 | bitr3id 285 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ (π΅ β V β§ π΄ β V)) β§ (π₯ β π β§ π¦ β π)) β§ (π β dom πΉ β§ π β dom πΉ)) β (π β π β (πΉβπ)π
(πΉβπ))) |
180 | 146 | adantrr 716 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ (π΅ β V β§ π΄ β V)) β§ (π₯ β π β§ π¦ β π)) β§ (π β dom πΉ β§ π β dom πΉ)) β (π₯ β πΉ):dom πΉβΆπ΅) |
181 | | simprr 772 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ (π΅ β V β§ π΄ β V)) β§ (π₯ β π β§ π¦ β π)) β§ (π β dom πΉ β§ π β dom πΉ)) β π β dom πΉ) |
182 | 180, 181 | fvco3d 6946 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ (π΅ β V β§ π΄ β V)) β§ (π₯ β π β§ π¦ β π)) β§ (π β dom πΉ β§ π β dom πΉ)) β ((β‘πΊ β (π₯ β πΉ))βπ) = (β‘πΊβ((π₯ β πΉ)βπ))) |
183 | 156 | adantrr 716 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ (π΅ β V β§ π΄ β V)) β§ (π₯ β π β§ π¦ β π)) β§ (π β dom πΉ β§ π β dom πΉ)) β (π¦ β πΉ):dom πΉβΆπ΅) |
184 | 183, 181 | fvco3d 6946 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ (π΅ β V β§ π΄ β V)) β§ (π₯ β π β§ π¦ β π)) β§ (π β dom πΉ β§ π β dom πΉ)) β ((β‘πΊ β (π¦ β πΉ))βπ) = (β‘πΊβ((π¦ β πΉ)βπ))) |
185 | 182, 184 | eqeq12d 2753 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ (π΅ β V β§ π΄ β V)) β§ (π₯ β π β§ π¦ β π)) β§ (π β dom πΉ β§ π β dom πΉ)) β (((β‘πΊ β (π₯ β πΉ))βπ) = ((β‘πΊ β (π¦ β πΉ))βπ) β (β‘πΊβ((π₯ β πΉ)βπ)) = (β‘πΊβ((π¦ β πΉ)βπ)))) |
186 | 28 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ (π΅ β V β§ π΄ β V)) β§ (π₯ β π β§ π¦ β π)) β§ (π β dom πΉ β§ π β dom πΉ)) β πΊ:dom πΊβ1-1-ontoβπ΅) |
187 | | f1of1 6788 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (β‘πΊ:π΅β1-1-ontoβdom
πΊ β β‘πΊ:π΅β1-1βdom πΊ) |
188 | 186, 19, 187 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ (π΅ β V β§ π΄ β V)) β§ (π₯ β π β§ π¦ β π)) β§ (π β dom πΉ β§ π β dom πΉ)) β β‘πΊ:π΅β1-1βdom πΊ) |
189 | 180, 181 | ffvelcdmd 7041 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ (π΅ β V β§ π΄ β V)) β§ (π₯ β π β§ π¦ β π)) β§ (π β dom πΉ β§ π β dom πΉ)) β ((π₯ β πΉ)βπ) β π΅) |
190 | 183, 181 | ffvelcdmd 7041 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ (π΅ β V β§ π΄ β V)) β§ (π₯ β π β§ π¦ β π)) β§ (π β dom πΉ β§ π β dom πΉ)) β ((π¦ β πΉ)βπ) β π΅) |
191 | | f1fveq 7214 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((β‘πΊ:π΅β1-1βdom πΊ β§ (((π₯ β πΉ)βπ) β π΅ β§ ((π¦ β πΉ)βπ) β π΅)) β ((β‘πΊβ((π₯ β πΉ)βπ)) = (β‘πΊβ((π¦ β πΉ)βπ)) β ((π₯ β πΉ)βπ) = ((π¦ β πΉ)βπ))) |
192 | 188, 189,
190, 191 | syl12anc 836 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ (π΅ β V β§ π΄ β V)) β§ (π₯ β π β§ π¦ β π)) β§ (π β dom πΉ β§ π β dom πΉ)) β ((β‘πΊβ((π₯ β πΉ)βπ)) = (β‘πΊβ((π¦ β πΉ)βπ)) β ((π₯ β πΉ)βπ) = ((π¦ β πΉ)βπ))) |
193 | | fvco3 6945 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((πΉ:dom πΉβΆπ΄ β§ π β dom πΉ) β ((π₯ β πΉ)βπ) = (π₯β(πΉβπ))) |
194 | 130, 181,
193 | sylancr 588 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ (π΅ β V β§ π΄ β V)) β§ (π₯ β π β§ π¦ β π)) β§ (π β dom πΉ β§ π β dom πΉ)) β ((π₯ β πΉ)βπ) = (π₯β(πΉβπ))) |
195 | | fvco3 6945 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((πΉ:dom πΉβΆπ΄ β§ π β dom πΉ) β ((π¦ β πΉ)βπ) = (π¦β(πΉβπ))) |
196 | 130, 181,
195 | sylancr 588 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ (π΅ β V β§ π΄ β V)) β§ (π₯ β π β§ π¦ β π)) β§ (π β dom πΉ β§ π β dom πΉ)) β ((π¦ β πΉ)βπ) = (π¦β(πΉβπ))) |
197 | 194, 196 | eqeq12d 2753 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ (π΅ β V β§ π΄ β V)) β§ (π₯ β π β§ π¦ β π)) β§ (π β dom πΉ β§ π β dom πΉ)) β (((π₯ β πΉ)βπ) = ((π¦ β πΉ)βπ) β (π₯β(πΉβπ)) = (π¦β(πΉβπ)))) |
198 | 185, 192,
197 | 3bitrd 305 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ (π΅ β V β§ π΄ β V)) β§ (π₯ β π β§ π¦ β π)) β§ (π β dom πΉ β§ π β dom πΉ)) β (((β‘πΊ β (π₯ β πΉ))βπ) = ((β‘πΊ β (π¦ β πΉ))βπ) β (π₯β(πΉβπ)) = (π¦β(πΉβπ)))) |
199 | 179, 198 | imbi12d 345 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ (π΅ β V β§ π΄ β V)) β§ (π₯ β π β§ π¦ β π)) β§ (π β dom πΉ β§ π β dom πΉ)) β ((π β π β ((β‘πΊ β (π₯ β πΉ))βπ) = ((β‘πΊ β (π¦ β πΉ))βπ)) β ((πΉβπ)π
(πΉβπ) β (π₯β(πΉβπ)) = (π¦β(πΉβπ))))) |
200 | 199 | anassrs 469 |
. . . . . . . . . . . . . . . 16
β’
(((((π β§ (π΅ β V β§ π΄ β V)) β§ (π₯ β π β§ π¦ β π)) β§ π β dom πΉ) β§ π β dom πΉ) β ((π β π β ((β‘πΊ β (π₯ β πΉ))βπ) = ((β‘πΊ β (π¦ β πΉ))βπ)) β ((πΉβπ)π
(πΉβπ) β (π₯β(πΉβπ)) = (π¦β(πΉβπ))))) |
201 | 200 | ralbidva 3173 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ (π΅ β V β§ π΄ β V)) β§ (π₯ β π β§ π¦ β π)) β§ π β dom πΉ) β (βπ β dom πΉ(π β π β ((β‘πΊ β (π₯ β πΉ))βπ) = ((β‘πΊ β (π¦ β πΉ))βπ)) β βπ β dom πΉ((πΉβπ)π
(πΉβπ) β (π₯β(πΉβπ)) = (π¦β(πΉβπ))))) |
202 | 174, 201 | bitr4d 282 |
. . . . . . . . . . . . . 14
β’ ((((π β§ (π΅ β V β§ π΄ β V)) β§ (π₯ β π β§ π¦ β π)) β§ π β dom πΉ) β (βπ€ β π΄ ((πΉβπ)π
π€ β (π₯βπ€) = (π¦βπ€)) β βπ β dom πΉ(π β π β ((β‘πΊ β (π₯ β πΉ))βπ) = ((β‘πΊ β (π¦ β πΉ))βπ)))) |
203 | 164, 202 | anbi12d 632 |
. . . . . . . . . . . . 13
β’ ((((π β§ (π΅ β V β§ π΄ β V)) β§ (π₯ β π β§ π¦ β π)) β§ π β dom πΉ) β (((π₯β(πΉβπ))π(π¦β(πΉβπ)) β§ βπ€ β π΄ ((πΉβπ)π
π€ β (π₯βπ€) = (π¦βπ€))) β (((β‘πΊ β (π₯ β πΉ))βπ) β ((β‘πΊ β (π¦ β πΉ))βπ) β§ βπ β dom πΉ(π β π β ((β‘πΊ β (π₯ β πΉ))βπ) = ((β‘πΊ β (π¦ β πΉ))βπ))))) |
204 | 203 | rexbidva 3174 |
. . . . . . . . . . . 12
β’ (((π β§ (π΅ β V β§ π΄ β V)) β§ (π₯ β π β§ π¦ β π)) β (βπ β dom πΉ((π₯β(πΉβπ))π(π¦β(πΉβπ)) β§ βπ€ β π΄ ((πΉβπ)π
π€ β (π₯βπ€) = (π¦βπ€))) β βπ β dom πΉ(((β‘πΊ β (π₯ β πΉ))βπ) β ((β‘πΊ β (π¦ β πΉ))βπ) β§ βπ β dom πΉ(π β π β ((β‘πΊ β (π₯ β πΉ))βπ) = ((β‘πΊ β (π¦ β πΉ))βπ))))) |
205 | 112, 122,
204 | 3bitr4rd 312 |
. . . . . . . . . . 11
β’ (((π β§ (π΅ β V β§ π΄ β V)) β§ (π₯ β π β§ π¦ β π)) β (βπ β dom πΉ((π₯β(πΉβπ))π(π¦β(πΉβπ)) β§ βπ€ β π΄ ((πΉβπ)π
π€ β (π₯βπ€) = (π¦βπ€))) β ((π β π β¦ (β‘πΊ β (π β πΉ)))βπ₯){β¨π, πβ© β£ βπ β dom πΉ((πβπ) β (πβπ) β§ βπ β dom πΉ(π β π β (πβπ) = (πβπ)))} ((π β π β¦ (β‘πΊ β (π β πΉ)))βπ¦))) |
206 | 81, 85, 205 | 3bitr3d 309 |
. . . . . . . . . 10
β’ (((π β§ (π΅ β V β§ π΄ β V)) β§ (π₯ β π β§ π¦ β π)) β (βπ§ β π΄ ((π₯βπ§)π(π¦βπ§) β§ βπ€ β π΄ (π§π
π€ β (π₯βπ€) = (π¦βπ€))) β ((π β π β¦ (β‘πΊ β (π β πΉ)))βπ₯){β¨π, πβ© β£ βπ β dom πΉ((πβπ) β (πβπ) β§ βπ β dom πΉ(π β π β (πβπ) = (πβπ)))} ((π β π β¦ (β‘πΊ β (π β πΉ)))βπ¦))) |
207 | 206 | ex 414 |
. . . . . . . . 9
β’ ((π β§ (π΅ β V β§ π΄ β V)) β ((π₯ β π β§ π¦ β π) β (βπ§ β π΄ ((π₯βπ§)π(π¦βπ§) β§ βπ€ β π΄ (π§π
π€ β (π₯βπ€) = (π¦βπ€))) β ((π β π β¦ (β‘πΊ β (π β πΉ)))βπ₯){β¨π, πβ© β£ βπ β dom πΉ((πβπ) β (πβπ) β§ βπ β dom πΉ(π β π β (πβπ) = (πβπ)))} ((π β π β¦ (β‘πΊ β (π β πΉ)))βπ¦)))) |
208 | 207 | pm5.32rd 579 |
. . . . . . . 8
β’ ((π β§ (π΅ β V β§ π΄ β V)) β ((βπ§ β π΄ ((π₯βπ§)π(π¦βπ§) β§ βπ€ β π΄ (π§π
π€ β (π₯βπ€) = (π¦βπ€))) β§ (π₯ β π β§ π¦ β π)) β (((π β π β¦ (β‘πΊ β (π β πΉ)))βπ₯){β¨π, πβ© β£ βπ β dom πΉ((πβπ) β (πβπ) β§ βπ β dom πΉ(π β π β (πβπ) = (πβπ)))} ((π β π β¦ (β‘πΊ β (π β πΉ)))βπ¦) β§ (π₯ β π β§ π¦ β π)))) |
209 | 208 | opabbidv 5176 |
. . . . . . 7
β’ ((π β§ (π΅ β V β§ π΄ β V)) β {β¨π₯, π¦β© β£ (βπ§ β π΄ ((π₯βπ§)π(π¦βπ§) β§ βπ€ β π΄ (π§π
π€ β (π₯βπ€) = (π¦βπ€))) β§ (π₯ β π β§ π¦ β π))} = {β¨π₯, π¦β© β£ (((π β π β¦ (β‘πΊ β (π β πΉ)))βπ₯){β¨π, πβ© β£ βπ β dom πΉ((πβπ) β (πβπ) β§ βπ β dom πΉ(π β π β (πβπ) = (πβπ)))} ((π β π β¦ (β‘πΊ β (π β πΉ)))βπ¦) β§ (π₯ β π β§ π¦ β π))}) |
210 | | wemapwe.t |
. . . . . . . . 9
β’ π = {β¨π₯, π¦β© β£ βπ§ β π΄ ((π₯βπ§)π(π¦βπ§) β§ βπ€ β π΄ (π§π
π€ β (π₯βπ€) = (π¦βπ€)))} |
211 | | df-xp 5644 |
. . . . . . . . 9
β’ (π Γ π) = {β¨π₯, π¦β© β£ (π₯ β π β§ π¦ β π)} |
212 | 210, 211 | ineq12i 4175 |
. . . . . . . 8
β’ (π β© (π Γ π)) = ({β¨π₯, π¦β© β£ βπ§ β π΄ ((π₯βπ§)π(π¦βπ§) β§ βπ€ β π΄ (π§π
π€ β (π₯βπ€) = (π¦βπ€)))} β© {β¨π₯, π¦β© β£ (π₯ β π β§ π¦ β π)}) |
213 | | inopab 5790 |
. . . . . . . 8
β’
({β¨π₯, π¦β© β£ βπ§ β π΄ ((π₯βπ§)π(π¦βπ§) β§ βπ€ β π΄ (π§π
π€ β (π₯βπ€) = (π¦βπ€)))} β© {β¨π₯, π¦β© β£ (π₯ β π β§ π¦ β π)}) = {β¨π₯, π¦β© β£ (βπ§ β π΄ ((π₯βπ§)π(π¦βπ§) β§ βπ€ β π΄ (π§π
π€ β (π₯βπ€) = (π¦βπ€))) β§ (π₯ β π β§ π¦ β π))} |
214 | 212, 213 | eqtri 2765 |
. . . . . . 7
β’ (π β© (π Γ π)) = {β¨π₯, π¦β© β£ (βπ§ β π΄ ((π₯βπ§)π(π¦βπ§) β§ βπ€ β π΄ (π§π
π€ β (π₯βπ€) = (π¦βπ€))) β§ (π₯ β π β§ π¦ β π))} |
215 | 211 | ineq2i 4174 |
. . . . . . . 8
β’
({β¨π₯, π¦β© β£ ((π β π β¦ (β‘πΊ β (π β πΉ)))βπ₯){β¨π, πβ© β£ βπ β dom πΉ((πβπ) β (πβπ) β§ βπ β dom πΉ(π β π β (πβπ) = (πβπ)))} ((π β π β¦ (β‘πΊ β (π β πΉ)))βπ¦)} β© (π Γ π)) = ({β¨π₯, π¦β© β£ ((π β π β¦ (β‘πΊ β (π β πΉ)))βπ₯){β¨π, πβ© β£ βπ β dom πΉ((πβπ) β (πβπ) β§ βπ β dom πΉ(π β π β (πβπ) = (πβπ)))} ((π β π β¦ (β‘πΊ β (π β πΉ)))βπ¦)} β© {β¨π₯, π¦β© β£ (π₯ β π β§ π¦ β π)}) |
216 | | inopab 5790 |
. . . . . . . 8
β’
({β¨π₯, π¦β© β£ ((π β π β¦ (β‘πΊ β (π β πΉ)))βπ₯){β¨π, πβ© β£ βπ β dom πΉ((πβπ) β (πβπ) β§ βπ β dom πΉ(π β π β (πβπ) = (πβπ)))} ((π β π β¦ (β‘πΊ β (π β πΉ)))βπ¦)} β© {β¨π₯, π¦β© β£ (π₯ β π β§ π¦ β π)}) = {β¨π₯, π¦β© β£ (((π β π β¦ (β‘πΊ β (π β πΉ)))βπ₯){β¨π, πβ© β£ βπ β dom πΉ((πβπ) β (πβπ) β§ βπ β dom πΉ(π β π β (πβπ) = (πβπ)))} ((π β π β¦ (β‘πΊ β (π β πΉ)))βπ¦) β§ (π₯ β π β§ π¦ β π))} |
217 | 215, 216 | eqtri 2765 |
. . . . . . 7
β’
({β¨π₯, π¦β© β£ ((π β π β¦ (β‘πΊ β (π β πΉ)))βπ₯){β¨π, πβ© β£ βπ β dom πΉ((πβπ) β (πβπ) β§ βπ β dom πΉ(π β π β (πβπ) = (πβπ)))} ((π β π β¦ (β‘πΊ β (π β πΉ)))βπ¦)} β© (π Γ π)) = {β¨π₯, π¦β© β£ (((π β π β¦ (β‘πΊ β (π β πΉ)))βπ₯){β¨π, πβ© β£ βπ β dom πΉ((πβπ) β (πβπ) β§ βπ β dom πΉ(π β π β (πβπ) = (πβπ)))} ((π β π β¦ (β‘πΊ β (π β πΉ)))βπ¦) β§ (π₯ β π β§ π¦ β π))} |
218 | 209, 214,
217 | 3eqtr4g 2802 |
. . . . . 6
β’ ((π β§ (π΅ β V β§ π΄ β V)) β (π β© (π Γ π)) = ({β¨π₯, π¦β© β£ ((π β π β¦ (β‘πΊ β (π β πΉ)))βπ₯){β¨π, πβ© β£ βπ β dom πΉ((πβπ) β (πβπ) β§ βπ β dom πΉ(π β π β (πβπ) = (πβπ)))} ((π β π β¦ (β‘πΊ β (π β πΉ)))βπ¦)} β© (π Γ π))) |
219 | | weeq1 5626 |
. . . . . 6
β’ ((π β© (π Γ π)) = ({β¨π₯, π¦β© β£ ((π β π β¦ (β‘πΊ β (π β πΉ)))βπ₯){β¨π, πβ© β£ βπ β dom πΉ((πβπ) β (πβπ) β§ βπ β dom πΉ(π β π β (πβπ) = (πβπ)))} ((π β π β¦ (β‘πΊ β (π β πΉ)))βπ¦)} β© (π Γ π)) β ((π β© (π Γ π)) We π β ({β¨π₯, π¦β© β£ ((π β π β¦ (β‘πΊ β (π β πΉ)))βπ₯){β¨π, πβ© β£ βπ β dom πΉ((πβπ) β (πβπ) β§ βπ β dom πΉ(π β π β (πβπ) = (πβπ)))} ((π β π β¦ (β‘πΊ β (π β πΉ)))βπ¦)} β© (π Γ π)) We π)) |
220 | 218, 219 | syl 17 |
. . . . 5
β’ ((π β§ (π΅ β V β§ π΄ β V)) β ((π β© (π Γ π)) We π β ({β¨π₯, π¦β© β£ ((π β π β¦ (β‘πΊ β (π β πΉ)))βπ₯){β¨π, πβ© β£ βπ β dom πΉ((πβπ) β (πβπ) β§ βπ β dom πΉ(π β π β (πβπ) = (πβπ)))} ((π β π β¦ (β‘πΊ β (π β πΉ)))βπ¦)} β© (π Γ π)) We π)) |
221 | 70, 220 | mpbird 257 |
. . . 4
β’ ((π β§ (π΅ β V β§ π΄ β V)) β (π β© (π Γ π)) We π) |
222 | | weinxp 5721 |
. . . 4
β’ (π We π β (π β© (π Γ π)) We π) |
223 | 221, 222 | sylibr 233 |
. . 3
β’ ((π β§ (π΅ β V β§ π΄ β V)) β π We π) |
224 | 223 | ex 414 |
. 2
β’ (π β ((π΅ β V β§ π΄ β V) β π We π)) |
225 | | we0 5633 |
. . 3
β’ π We β
|
226 | | elmapex 8793 |
. . . . . . . . 9
β’ (π₯ β (π΅ βm π΄) β (π΅ β V β§ π΄ β V)) |
227 | 226 | con3i 154 |
. . . . . . . 8
β’ (Β¬
(π΅ β V β§ π΄ β V) β Β¬ π₯ β (π΅ βm π΄)) |
228 | 227 | pm2.21d 121 |
. . . . . . 7
β’ (Β¬
(π΅ β V β§ π΄ β V) β (π₯ β (π΅ βm π΄) β Β¬ π₯ finSupp π)) |
229 | 228 | ralrimiv 3143 |
. . . . . 6
β’ (Β¬
(π΅ β V β§ π΄ β V) β βπ₯ β (π΅ βm π΄) Β¬ π₯ finSupp π) |
230 | | rabeq0 4349 |
. . . . . 6
β’ ({π₯ β (π΅ βm π΄) β£ π₯ finSupp π} = β
β βπ₯ β (π΅ βm π΄) Β¬ π₯ finSupp π) |
231 | 229, 230 | sylibr 233 |
. . . . 5
β’ (Β¬
(π΅ β V β§ π΄ β V) β {π₯ β (π΅ βm π΄) β£ π₯ finSupp π} = β
) |
232 | 1, 231 | eqtrid 2789 |
. . . 4
β’ (Β¬
(π΅ β V β§ π΄ β V) β π = β
) |
233 | | weeq2 5627 |
. . . 4
β’ (π = β
β (π We π β π We β
)) |
234 | 232, 233 | syl 17 |
. . 3
β’ (Β¬
(π΅ β V β§ π΄ β V) β (π We π β π We β
)) |
235 | 225, 234 | mpbiri 258 |
. 2
β’ (Β¬
(π΅ β V β§ π΄ β V) β π We π) |
236 | 224, 235 | pm2.61d1 180 |
1
β’ (π β π We π) |