Step | Hyp | Ref
| Expression |
1 | | is2ndc 22813 |
. . 3
β’ (π½ β 2ndΟ
β βπ β
TopBases (π βΌ Ο
β§ (topGenβπ) =
π½)) |
2 | | omex 9584 |
. . . . . . 7
β’ Ο
β V |
3 | 2 | brdom 8903 |
. . . . . 6
β’ (π βΌ Ο β
βπ π:πβ1-1βΟ) |
4 | | ssrab2 4038 |
. . . . . . . . . . . . . . . . . . . 20
β’ {π β ran π β£ (β‘πβπ) β (π« π΅ β {β
})} β ran π |
5 | | f1f 6739 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π:πβ1-1βΟ β π:πβΆΟ) |
6 | 5 | frnd 6677 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π:πβ1-1βΟ β ran π β Ο) |
7 | 6 | adantl 483 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β TopBases β§ π:πβ1-1βΟ) β ran π β Ο) |
8 | 4, 7 | sstrid 3956 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β TopBases β§ π:πβ1-1βΟ) β {π β ran π β£ (β‘πβπ) β (π« π΅ β {β
})} β
Ο) |
9 | 8 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β TopBases β§ π:πβ1-1βΟ) β§ (π₯ β π΄ β§ π΅ β ((topGenβπ) β {β
}))) β {π β ran π β£ (β‘πβπ) β (π« π΅ β {β
})} β
Ο) |
10 | | eldifsn 4748 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π΅ β ((topGenβπ) β {β
}) β
(π΅ β
(topGenβπ) β§
π΅ β
β
)) |
11 | | n0 4307 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π΅ β β
β
βπ¦ π¦ β π΅) |
12 | | tg2 22331 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π΅ β (topGenβπ) β§ π¦ β π΅) β βπ§ β π (π¦ β π§ β§ π§ β π΅)) |
13 | | omsson 7807 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ Ο
β On |
14 | 8, 13 | sstrdi 3957 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π β TopBases β§ π:πβ1-1βΟ) β {π β ran π β£ (β‘πβπ) β (π« π΅ β {β
})} β
On) |
15 | 14 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((((π β TopBases β§ π:πβ1-1βΟ) β§ π₯ β π΄) β§ (π§ β π β§ (π¦ β π§ β§ π§ β π΅))) β {π β ran π β£ (β‘πβπ) β (π« π΅ β {β
})} β
On) |
16 | | f1fn 6740 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (π:πβ1-1βΟ β π Fn π) |
17 | 16 | ad3antlr 730 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((((π β TopBases β§ π:πβ1-1βΟ) β§ π₯ β π΄) β§ (π§ β π β§ (π¦ β π§ β§ π§ β π΅))) β π Fn π) |
18 | | simprl 770 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((((π β TopBases β§ π:πβ1-1βΟ) β§ π₯ β π΄) β§ (π§ β π β§ (π¦ β π§ β§ π§ β π΅))) β π§ β π) |
19 | | fnfvelrn 7032 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((π Fn π β§ π§ β π) β (πβπ§) β ran π) |
20 | 17, 18, 19 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((((π β TopBases β§ π:πβ1-1βΟ) β§ π₯ β π΄) β§ (π§ β π β§ (π¦ β π§ β§ π§ β π΅))) β (πβπ§) β ran π) |
21 | | f1f1orn 6796 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (π:πβ1-1βΟ β π:πβ1-1-ontoβran
π) |
22 | 21 | ad3antlr 730 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((((π β TopBases β§ π:πβ1-1βΟ) β§ π₯ β π΄) β§ (π§ β π β§ (π¦ β π§ β§ π§ β π΅))) β π:πβ1-1-ontoβran
π) |
23 | | f1ocnvfv1 7223 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((π:πβ1-1-ontoβran
π β§ π§ β π) β (β‘πβ(πβπ§)) = π§) |
24 | 22, 18, 23 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((((π β TopBases β§ π:πβ1-1βΟ) β§ π₯ β π΄) β§ (π§ β π β§ (π¦ β π§ β§ π§ β π΅))) β (β‘πβ(πβπ§)) = π§) |
25 | | simprrr 781 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ ((((π β TopBases β§ π:πβ1-1βΟ) β§ π₯ β π΄) β§ (π§ β π β§ (π¦ β π§ β§ π§ β π΅))) β π§ β π΅) |
26 | | velpw 4566 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (π§ β π« π΅ β π§ β π΅) |
27 | 25, 26 | sylibr 233 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((((π β TopBases β§ π:πβ1-1βΟ) β§ π₯ β π΄) β§ (π§ β π β§ (π¦ β π§ β§ π§ β π΅))) β π§ β π« π΅) |
28 | | simprrl 780 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ ((((π β TopBases β§ π:πβ1-1βΟ) β§ π₯ β π΄) β§ (π§ β π β§ (π¦ β π§ β§ π§ β π΅))) β π¦ β π§) |
29 | 28 | ne0d 4296 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((((π β TopBases β§ π:πβ1-1βΟ) β§ π₯ β π΄) β§ (π§ β π β§ (π¦ β π§ β§ π§ β π΅))) β π§ β β
) |
30 | | eldifsn 4748 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (π§ β (π« π΅ β {β
}) β
(π§ β π« π΅ β§ π§ β β
)) |
31 | 27, 29, 30 | sylanbrc 584 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((((π β TopBases β§ π:πβ1-1βΟ) β§ π₯ β π΄) β§ (π§ β π β§ (π¦ β π§ β§ π§ β π΅))) β π§ β (π« π΅ β {β
})) |
32 | 24, 31 | eqeltrd 2834 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((((π β TopBases β§ π:πβ1-1βΟ) β§ π₯ β π΄) β§ (π§ β π β§ (π¦ β π§ β§ π§ β π΅))) β (β‘πβ(πβπ§)) β (π« π΅ β {β
})) |
33 | | fveq2 6843 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (π = (πβπ§) β (β‘πβπ) = (β‘πβ(πβπ§))) |
34 | 33 | eleq1d 2819 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (π = (πβπ§) β ((β‘πβπ) β (π« π΅ β {β
}) β (β‘πβ(πβπ§)) β (π« π΅ β {β
}))) |
35 | 34 | rspcev 3580 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (((πβπ§) β ran π β§ (β‘πβ(πβπ§)) β (π« π΅ β {β
})) β βπ β ran π(β‘πβπ) β (π« π΅ β {β
})) |
36 | 20, 32, 35 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((((π β TopBases β§ π:πβ1-1βΟ) β§ π₯ β π΄) β§ (π§ β π β§ (π¦ β π§ β§ π§ β π΅))) β βπ β ran π(β‘πβπ) β (π« π΅ β {β
})) |
37 | | rabn0 4346 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ({π β ran π β£ (β‘πβπ) β (π« π΅ β {β
})} β β
β
βπ β ran π(β‘πβπ) β (π« π΅ β {β
})) |
38 | 36, 37 | sylibr 233 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((((π β TopBases β§ π:πβ1-1βΟ) β§ π₯ β π΄) β§ (π§ β π β§ (π¦ β π§ β§ π§ β π΅))) β {π β ran π β£ (β‘πβπ) β (π« π΅ β {β
})} β
β
) |
39 | | onint 7726 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (({π β ran π β£ (β‘πβπ) β (π« π΅ β {β
})} β On β§ {π β ran π β£ (β‘πβπ) β (π« π΅ β {β
})} β β
) β
β© {π β ran π β£ (β‘πβπ) β (π« π΅ β {β
})} β {π β ran π β£ (β‘πβπ) β (π« π΅ β {β
})}) |
40 | 15, 38, 39 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((((π β TopBases β§ π:πβ1-1βΟ) β§ π₯ β π΄) β§ (π§ β π β§ (π¦ β π§ β§ π§ β π΅))) β β©
{π β ran π β£ (β‘πβπ) β (π« π΅ β {β
})} β {π β ran π β£ (β‘πβπ) β (π« π΅ β {β
})}) |
41 | 40 | rexlimdvaa 3150 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π β TopBases β§ π:πβ1-1βΟ) β§ π₯ β π΄) β (βπ§ β π (π¦ β π§ β§ π§ β π΅) β β© {π β ran π β£ (β‘πβπ) β (π« π΅ β {β
})} β {π β ran π β£ (β‘πβπ) β (π« π΅ β {β
})})) |
42 | 12, 41 | syl5 34 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β TopBases β§ π:πβ1-1βΟ) β§ π₯ β π΄) β ((π΅ β (topGenβπ) β§ π¦ β π΅) β β© {π β ran π β£ (β‘πβπ) β (π« π΅ β {β
})} β {π β ran π β£ (β‘πβπ) β (π« π΅ β {β
})})) |
43 | 42 | expdimp 454 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β TopBases β§ π:πβ1-1βΟ) β§ π₯ β π΄) β§ π΅ β (topGenβπ)) β (π¦ β π΅ β β© {π β ran π β£ (β‘πβπ) β (π« π΅ β {β
})} β {π β ran π β£ (β‘πβπ) β (π« π΅ β {β
})})) |
44 | 43 | exlimdv 1937 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β TopBases β§ π:πβ1-1βΟ) β§ π₯ β π΄) β§ π΅ β (topGenβπ)) β (βπ¦ π¦ β π΅ β β© {π β ran π β£ (β‘πβπ) β (π« π΅ β {β
})} β {π β ran π β£ (β‘πβπ) β (π« π΅ β {β
})})) |
45 | 11, 44 | biimtrid 241 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β TopBases β§ π:πβ1-1βΟ) β§ π₯ β π΄) β§ π΅ β (topGenβπ)) β (π΅ β β
β β© {π
β ran π β£ (β‘πβπ) β (π« π΅ β {β
})} β {π β ran π β£ (β‘πβπ) β (π« π΅ β {β
})})) |
46 | 45 | expimpd 455 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β TopBases β§ π:πβ1-1βΟ) β§ π₯ β π΄) β ((π΅ β (topGenβπ) β§ π΅ β β
) β β© {π
β ran π β£ (β‘πβπ) β (π« π΅ β {β
})} β {π β ran π β£ (β‘πβπ) β (π« π΅ β {β
})})) |
47 | 10, 46 | biimtrid 241 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β TopBases β§ π:πβ1-1βΟ) β§ π₯ β π΄) β (π΅ β ((topGenβπ) β {β
}) β β© {π
β ran π β£ (β‘πβπ) β (π« π΅ β {β
})} β {π β ran π β£ (β‘πβπ) β (π« π΅ β {β
})})) |
48 | 47 | impr 456 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β TopBases β§ π:πβ1-1βΟ) β§ (π₯ β π΄ β§ π΅ β ((topGenβπ) β {β
}))) β β© {π
β ran π β£ (β‘πβπ) β (π« π΅ β {β
})} β {π β ran π β£ (β‘πβπ) β (π« π΅ β {β
})}) |
49 | 9, 48 | sseldd 3946 |
. . . . . . . . . . . . . . . . 17
β’ (((π β TopBases β§ π:πβ1-1βΟ) β§ (π₯ β π΄ β§ π΅ β ((topGenβπ) β {β
}))) β β© {π
β ran π β£ (β‘πβπ) β (π« π΅ β {β
})} β
Ο) |
50 | 49 | expr 458 |
. . . . . . . . . . . . . . . 16
β’ (((π β TopBases β§ π:πβ1-1βΟ) β§ π₯ β π΄) β (π΅ β ((topGenβπ) β {β
}) β β© {π
β ran π β£ (β‘πβπ) β (π« π΅ β {β
})} β
Ο)) |
51 | 50 | ralimdva 3161 |
. . . . . . . . . . . . . . 15
β’ ((π β TopBases β§ π:πβ1-1βΟ) β (βπ₯ β π΄ π΅ β ((topGenβπ) β {β
}) β βπ₯ β π΄ β© {π β ran π β£ (β‘πβπ) β (π« π΅ β {β
})} β
Ο)) |
52 | 51 | imp 408 |
. . . . . . . . . . . . . 14
β’ (((π β TopBases β§ π:πβ1-1βΟ) β§ βπ₯ β π΄ π΅ β ((topGenβπ) β {β
})) β βπ₯ β π΄ β© {π β ran π β£ (β‘πβπ) β (π« π΅ β {β
})} β
Ο) |
53 | 52 | adantrr 716 |
. . . . . . . . . . . . 13
β’ (((π β TopBases β§ π:πβ1-1βΟ) β§ (βπ₯ β π΄ π΅ β ((topGenβπ) β {β
}) β§ βπ¦β*π₯ β π΄ π¦ β π΅)) β βπ₯ β π΄ β© {π β ran π β£ (β‘πβπ) β (π« π΅ β {β
})} β
Ο) |
54 | | eqid 2733 |
. . . . . . . . . . . . . 14
β’ (π₯ β π΄ β¦ β© {π β ran π β£ (β‘πβπ) β (π« π΅ β {β
})}) = (π₯ β π΄ β¦ β© {π β ran π β£ (β‘πβπ) β (π« π΅ β {β
})}) |
55 | 54 | fmpt 7059 |
. . . . . . . . . . . . 13
β’
(βπ₯ β
π΄ β© {π
β ran π β£ (β‘πβπ) β (π« π΅ β {β
})} β Ο β
(π₯ β π΄ β¦ β© {π β ran π β£ (β‘πβπ) β (π« π΅ β {β
})}):π΄βΆΟ) |
56 | 53, 55 | sylib 217 |
. . . . . . . . . . . 12
β’ (((π β TopBases β§ π:πβ1-1βΟ) β§ (βπ₯ β π΄ π΅ β ((topGenβπ) β {β
}) β§ βπ¦β*π₯ β π΄ π¦ β π΅)) β (π₯ β π΄ β¦ β© {π β ran π β£ (β‘πβπ) β (π« π΅ β {β
})}):π΄βΆΟ) |
57 | | neeq1 3003 |
. . . . . . . . . . . . . . . . . . 19
β’ ((β‘πβπ§) = if((β‘πβπ§) β β
, (β‘πβπ§), 1o) β ((β‘πβπ§) β β
β if((β‘πβπ§) β β
, (β‘πβπ§), 1o) β
β
)) |
58 | | neeq1 3003 |
. . . . . . . . . . . . . . . . . . 19
β’
(1o = if((β‘πβπ§) β β
, (β‘πβπ§), 1o) β (1o β
β
β if((β‘πβπ§) β β
, (β‘πβπ§), 1o) β
β
)) |
59 | | 1n0 8435 |
. . . . . . . . . . . . . . . . . . 19
β’
1o β β
|
60 | 57, 58, 59 | elimhyp 4552 |
. . . . . . . . . . . . . . . . . 18
β’ if((β‘πβπ§) β β
, (β‘πβπ§), 1o) β
β
|
61 | | n0 4307 |
. . . . . . . . . . . . . . . . . 18
β’
(if((β‘πβπ§) β β
, (β‘πβπ§), 1o) β β
β
βπ¦ π¦ β if((β‘πβπ§) β β
, (β‘πβπ§), 1o)) |
62 | 60, 61 | mpbi 229 |
. . . . . . . . . . . . . . . . 17
β’
βπ¦ π¦ β if((β‘πβπ§) β β
, (β‘πβπ§), 1o) |
63 | | 19.29r 1878 |
. . . . . . . . . . . . . . . . 17
β’
((βπ¦ π¦ β if((β‘πβπ§) β β
, (β‘πβπ§), 1o) β§ βπ¦β*π₯ β π΄ π¦ β π΅) β βπ¦(π¦ β if((β‘πβπ§) β β
, (β‘πβπ§), 1o) β§ β*π₯ β π΄ π¦ β π΅)) |
64 | 62, 63 | mpan 689 |
. . . . . . . . . . . . . . . 16
β’
(βπ¦β*π₯ β π΄ π¦ β π΅ β βπ¦(π¦ β if((β‘πβπ§) β β
, (β‘πβπ§), 1o) β§ β*π₯ β π΄ π¦ β π΅)) |
65 | | eleq1 2822 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ (π§ = β©
{π β ran π β£ (β‘πβπ) β (π« π΅ β {β
})} β (π§ β {π β ran π β£ (β‘πβπ) β (π« π΅ β {β
})} β β© {π
β ran π β£ (β‘πβπ) β (π« π΅ β {β
})} β {π β ran π β£ (β‘πβπ) β (π« π΅ β {β
})})) |
66 | 48, 65 | syl5ibrcom 247 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ (((π β TopBases β§ π:πβ1-1βΟ) β§ (π₯ β π΄ β§ π΅ β ((topGenβπ) β {β
}))) β (π§ = β©
{π β ran π β£ (β‘πβπ) β (π« π΅ β {β
})} β π§ β {π β ran π β£ (β‘πβπ) β (π« π΅ β {β
})})) |
67 | 66 | imp 408 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ ((((π β TopBases β§ π:πβ1-1βΟ) β§ (π₯ β π΄ β§ π΅ β ((topGenβπ) β {β
}))) β§ π§ = β©
{π β ran π β£ (β‘πβπ) β (π« π΅ β {β
})}) β π§ β {π β ran π β£ (β‘πβπ) β (π« π΅ β {β
})}) |
68 | | fveq2 6843 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ (π = π§ β (β‘πβπ) = (β‘πβπ§)) |
69 | 68 | eleq1d 2819 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ (π = π§ β ((β‘πβπ) β (π« π΅ β {β
}) β (β‘πβπ§) β (π« π΅ β {β
}))) |
70 | 69 | elrab 3646 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ (π§ β {π β ran π β£ (β‘πβπ) β (π« π΅ β {β
})} β (π§ β ran π β§ (β‘πβπ§) β (π« π΅ β {β
}))) |
71 | 70 | simprbi 498 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (π§ β {π β ran π β£ (β‘πβπ) β (π« π΅ β {β
})} β (β‘πβπ§) β (π« π΅ β {β
})) |
72 | 67, 71 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ ((((π β TopBases β§ π:πβ1-1βΟ) β§ (π₯ β π΄ β§ π΅ β ((topGenβπ) β {β
}))) β§ π§ = β©
{π β ran π β£ (β‘πβπ) β (π« π΅ β {β
})}) β (β‘πβπ§) β (π« π΅ β {β
})) |
73 | | eldifsn 4748 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ ((β‘πβπ§) β (π« π΅ β {β
}) β ((β‘πβπ§) β π« π΅ β§ (β‘πβπ§) β β
)) |
74 | 72, 73 | sylib 217 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((((π β TopBases β§ π:πβ1-1βΟ) β§ (π₯ β π΄ β§ π΅ β ((topGenβπ) β {β
}))) β§ π§ = β©
{π β ran π β£ (β‘πβπ) β (π« π΅ β {β
})}) β ((β‘πβπ§) β π« π΅ β§ (β‘πβπ§) β β
)) |
75 | 74 | simprd 497 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((((π β TopBases β§ π:πβ1-1βΟ) β§ (π₯ β π΄ β§ π΅ β ((topGenβπ) β {β
}))) β§ π§ = β©
{π β ran π β£ (β‘πβπ) β (π« π΅ β {β
})}) β (β‘πβπ§) β β
) |
76 | 75 | iftrued 4495 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((((π β TopBases β§ π:πβ1-1βΟ) β§ (π₯ β π΄ β§ π΅ β ((topGenβπ) β {β
}))) β§ π§ = β©
{π β ran π β£ (β‘πβπ) β (π« π΅ β {β
})}) β if((β‘πβπ§) β β
, (β‘πβπ§), 1o) = (β‘πβπ§)) |
77 | 74 | simpld 496 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((((π β TopBases β§ π:πβ1-1βΟ) β§ (π₯ β π΄ β§ π΅ β ((topGenβπ) β {β
}))) β§ π§ = β©
{π β ran π β£ (β‘πβπ) β (π« π΅ β {β
})}) β (β‘πβπ§) β π« π΅) |
78 | 77 | elpwid 4570 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((((π β TopBases β§ π:πβ1-1βΟ) β§ (π₯ β π΄ β§ π΅ β ((topGenβπ) β {β
}))) β§ π§ = β©
{π β ran π β£ (β‘πβπ) β (π« π΅ β {β
})}) β (β‘πβπ§) β π΅) |
79 | 76, 78 | eqsstrd 3983 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((((π β TopBases β§ π:πβ1-1βΟ) β§ (π₯ β π΄ β§ π΅ β ((topGenβπ) β {β
}))) β§ π§ = β©
{π β ran π β£ (β‘πβπ) β (π« π΅ β {β
})}) β if((β‘πβπ§) β β
, (β‘πβπ§), 1o) β π΅) |
80 | 79 | sseld 3944 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((((π β TopBases β§ π:πβ1-1βΟ) β§ (π₯ β π΄ β§ π΅ β ((topGenβπ) β {β
}))) β§ π§ = β©
{π β ran π β£ (β‘πβπ) β (π« π΅ β {β
})}) β (π¦ β if((β‘πβπ§) β β
, (β‘πβπ§), 1o) β π¦ β π΅)) |
81 | 80 | exp31 421 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β TopBases β§ π:πβ1-1βΟ) β ((π₯ β π΄ β§ π΅ β ((topGenβπ) β {β
})) β (π§ = β©
{π β ran π β£ (β‘πβπ) β (π« π΅ β {β
})} β (π¦ β if((β‘πβπ§) β β
, (β‘πβπ§), 1o) β π¦ β π΅)))) |
82 | 81 | com23 86 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β TopBases β§ π:πβ1-1βΟ) β (π§ = β© {π β ran π β£ (β‘πβπ) β (π« π΅ β {β
})} β ((π₯ β π΄ β§ π΅ β ((topGenβπ) β {β
})) β (π¦ β if((β‘πβπ§) β β
, (β‘πβπ§), 1o) β π¦ β π΅)))) |
83 | 82 | exp4a 433 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β TopBases β§ π:πβ1-1βΟ) β (π§ = β© {π β ran π β£ (β‘πβπ) β (π« π΅ β {β
})} β (π₯ β π΄ β (π΅ β ((topGenβπ) β {β
}) β (π¦ β if((β‘πβπ§) β β
, (β‘πβπ§), 1o) β π¦ β π΅))))) |
84 | 83 | com25 99 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β TopBases β§ π:πβ1-1βΟ) β (π¦ β if((β‘πβπ§) β β
, (β‘πβπ§), 1o) β (π₯ β π΄ β (π΅ β ((topGenβπ) β {β
}) β (π§ = β©
{π β ran π β£ (β‘πβπ) β (π« π΅ β {β
})} β π¦ β π΅))))) |
85 | 84 | imp31 419 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β TopBases β§ π:πβ1-1βΟ) β§ π¦ β if((β‘πβπ§) β β
, (β‘πβπ§), 1o)) β§ π₯ β π΄) β (π΅ β ((topGenβπ) β {β
}) β (π§ = β©
{π β ran π β£ (β‘πβπ) β (π« π΅ β {β
})} β π¦ β π΅))) |
86 | 85 | ralimdva 3161 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β TopBases β§ π:πβ1-1βΟ) β§ π¦ β if((β‘πβπ§) β β
, (β‘πβπ§), 1o)) β (βπ₯ β π΄ π΅ β ((topGenβπ) β {β
}) β βπ₯ β π΄ (π§ = β© {π β ran π β£ (β‘πβπ) β (π« π΅ β {β
})} β π¦ β π΅))) |
87 | 86 | imp 408 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β TopBases β§ π:πβ1-1βΟ) β§ π¦ β if((β‘πβπ§) β β
, (β‘πβπ§), 1o)) β§ βπ₯ β π΄ π΅ β ((topGenβπ) β {β
})) β βπ₯ β π΄ (π§ = β© {π β ran π β£ (β‘πβπ) β (π« π΅ β {β
})} β π¦ β π΅)) |
88 | 87 | an32s 651 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β TopBases β§ π:πβ1-1βΟ) β§ βπ₯ β π΄ π΅ β ((topGenβπ) β {β
})) β§ π¦ β if((β‘πβπ§) β β
, (β‘πβπ§), 1o)) β βπ₯ β π΄ (π§ = β© {π β ran π β£ (β‘πβπ) β (π« π΅ β {β
})} β π¦ β π΅)) |
89 | | rmoim 3699 |
. . . . . . . . . . . . . . . . . . 19
β’
(βπ₯ β
π΄ (π§ = β© {π β ran π β£ (β‘πβπ) β (π« π΅ β {β
})} β π¦ β π΅) β (β*π₯ β π΄ π¦ β π΅ β β*π₯ β π΄ π§ = β© {π β ran π β£ (β‘πβπ) β (π« π΅ β {β
})})) |
90 | 88, 89 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β TopBases β§ π:πβ1-1βΟ) β§ βπ₯ β π΄ π΅ β ((topGenβπ) β {β
})) β§ π¦ β if((β‘πβπ§) β β
, (β‘πβπ§), 1o)) β (β*π₯ β π΄ π¦ β π΅ β β*π₯ β π΄ π§ = β© {π β ran π β£ (β‘πβπ) β (π« π΅ β {β
})})) |
91 | 90 | expimpd 455 |
. . . . . . . . . . . . . . . . 17
β’ (((π β TopBases β§ π:πβ1-1βΟ) β§ βπ₯ β π΄ π΅ β ((topGenβπ) β {β
})) β ((π¦ β if((β‘πβπ§) β β
, (β‘πβπ§), 1o) β§ β*π₯ β π΄ π¦ β π΅) β β*π₯ β π΄ π§ = β© {π β ran π β£ (β‘πβπ) β (π« π΅ β {β
})})) |
92 | 91 | exlimdv 1937 |
. . . . . . . . . . . . . . . 16
β’ (((π β TopBases β§ π:πβ1-1βΟ) β§ βπ₯ β π΄ π΅ β ((topGenβπ) β {β
})) β (βπ¦(π¦ β if((β‘πβπ§) β β
, (β‘πβπ§), 1o) β§ β*π₯ β π΄ π¦ β π΅) β β*π₯ β π΄ π§ = β© {π β ran π β£ (β‘πβπ) β (π« π΅ β {β
})})) |
93 | 64, 92 | syl5 34 |
. . . . . . . . . . . . . . 15
β’ (((π β TopBases β§ π:πβ1-1βΟ) β§ βπ₯ β π΄ π΅ β ((topGenβπ) β {β
})) β (βπ¦β*π₯ β π΄ π¦ β π΅ β β*π₯ β π΄ π§ = β© {π β ran π β£ (β‘πβπ) β (π« π΅ β {β
})})) |
94 | 93 | impr 456 |
. . . . . . . . . . . . . 14
β’ (((π β TopBases β§ π:πβ1-1βΟ) β§ (βπ₯ β π΄ π΅ β ((topGenβπ) β {β
}) β§ βπ¦β*π₯ β π΄ π¦ β π΅)) β β*π₯ β π΄ π§ = β© {π β ran π β£ (β‘πβπ) β (π« π΅ β {β
})}) |
95 | | nfcv 2904 |
. . . . . . . . . . . . . . . . 17
β’
β²π₯π€ |
96 | | nfmpt1 5214 |
. . . . . . . . . . . . . . . . 17
β’
β²π₯(π₯ β π΄ β¦ β© {π β ran π β£ (β‘πβπ) β (π« π΅ β {β
})}) |
97 | | nfcv 2904 |
. . . . . . . . . . . . . . . . 17
β’
β²π₯π§ |
98 | 95, 96, 97 | nfbr 5153 |
. . . . . . . . . . . . . . . 16
β’
β²π₯ π€(π₯ β π΄ β¦ β© {π β ran π β£ (β‘πβπ) β (π« π΅ β {β
})})π§ |
99 | | nfv 1918 |
. . . . . . . . . . . . . . . 16
β’
β²π€(π₯ β π΄ β§ π§ = β© {π β ran π β£ (β‘πβπ) β (π« π΅ β {β
})}) |
100 | | breq1 5109 |
. . . . . . . . . . . . . . . . 17
β’ (π€ = π₯ β (π€(π₯ β π΄ β¦ β© {π β ran π β£ (β‘πβπ) β (π« π΅ β {β
})})π§ β π₯(π₯ β π΄ β¦ β© {π β ran π β£ (β‘πβπ) β (π« π΅ β {β
})})π§)) |
101 | | df-br 5107 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯(π₯ β π΄ β¦ β© {π β ran π β£ (β‘πβπ) β (π« π΅ β {β
})})π§ β β¨π₯, π§β© β (π₯ β π΄ β¦ β© {π β ran π β£ (β‘πβπ) β (π« π΅ β {β
})})) |
102 | | df-mpt 5190 |
. . . . . . . . . . . . . . . . . . 19
β’ (π₯ β π΄ β¦ β© {π β ran π β£ (β‘πβπ) β (π« π΅ β {β
})}) = {β¨π₯, π§β© β£ (π₯ β π΄ β§ π§ = β© {π β ran π β£ (β‘πβπ) β (π« π΅ β {β
})})} |
103 | 102 | eleq2i 2826 |
. . . . . . . . . . . . . . . . . 18
β’
(β¨π₯, π§β© β (π₯ β π΄ β¦ β© {π β ran π β£ (β‘πβπ) β (π« π΅ β {β
})}) β β¨π₯, π§β© β {β¨π₯, π§β© β£ (π₯ β π΄ β§ π§ = β© {π β ran π β£ (β‘πβπ) β (π« π΅ β {β
})})}) |
104 | | opabidw 5482 |
. . . . . . . . . . . . . . . . . 18
β’
(β¨π₯, π§β© β {β¨π₯, π§β© β£ (π₯ β π΄ β§ π§ = β© {π β ran π β£ (β‘πβπ) β (π« π΅ β {β
})})} β (π₯ β π΄ β§ π§ = β© {π β ran π β£ (β‘πβπ) β (π« π΅ β {β
})})) |
105 | 101, 103,
104 | 3bitri 297 |
. . . . . . . . . . . . . . . . 17
β’ (π₯(π₯ β π΄ β¦ β© {π β ran π β£ (β‘πβπ) β (π« π΅ β {β
})})π§ β (π₯ β π΄ β§ π§ = β© {π β ran π β£ (β‘πβπ) β (π« π΅ β {β
})})) |
106 | 100, 105 | bitrdi 287 |
. . . . . . . . . . . . . . . 16
β’ (π€ = π₯ β (π€(π₯ β π΄ β¦ β© {π β ran π β£ (β‘πβπ) β (π« π΅ β {β
})})π§ β (π₯ β π΄ β§ π§ = β© {π β ran π β£ (β‘πβπ) β (π« π΅ β {β
})}))) |
107 | 98, 99, 106 | cbvmow 2598 |
. . . . . . . . . . . . . . 15
β’
(β*π€ π€(π₯ β π΄ β¦ β© {π β ran π β£ (β‘πβπ) β (π« π΅ β {β
})})π§ β β*π₯(π₯ β π΄ β§ π§ = β© {π β ran π β£ (β‘πβπ) β (π« π΅ β {β
})})) |
108 | | df-rmo 3352 |
. . . . . . . . . . . . . . 15
β’
(β*π₯ β
π΄ π§ = β© {π β ran π β£ (β‘πβπ) β (π« π΅ β {β
})} β β*π₯(π₯ β π΄ β§ π§ = β© {π β ran π β£ (β‘πβπ) β (π« π΅ β {β
})})) |
109 | 107, 108 | bitr4i 278 |
. . . . . . . . . . . . . 14
β’
(β*π€ π€(π₯ β π΄ β¦ β© {π β ran π β£ (β‘πβπ) β (π« π΅ β {β
})})π§ β β*π₯ β π΄ π§ = β© {π β ran π β£ (β‘πβπ) β (π« π΅ β {β
})}) |
110 | 94, 109 | sylibr 233 |
. . . . . . . . . . . . 13
β’ (((π β TopBases β§ π:πβ1-1βΟ) β§ (βπ₯ β π΄ π΅ β ((topGenβπ) β {β
}) β§ βπ¦β*π₯ β π΄ π¦ β π΅)) β β*π€ π€(π₯ β π΄ β¦ β© {π β ran π β£ (β‘πβπ) β (π« π΅ β {β
})})π§) |
111 | 110 | alrimiv 1931 |
. . . . . . . . . . . 12
β’ (((π β TopBases β§ π:πβ1-1βΟ) β§ (βπ₯ β π΄ π΅ β ((topGenβπ) β {β
}) β§ βπ¦β*π₯ β π΄ π¦ β π΅)) β βπ§β*π€ π€(π₯ β π΄ β¦ β© {π β ran π β£ (β‘πβπ) β (π« π΅ β {β
})})π§) |
112 | | dff12 6738 |
. . . . . . . . . . . 12
β’ ((π₯ β π΄ β¦ β© {π β ran π β£ (β‘πβπ) β (π« π΅ β {β
})}):π΄β1-1βΟ β ((π₯ β π΄ β¦ β© {π β ran π β£ (β‘πβπ) β (π« π΅ β {β
})}):π΄βΆΟ β§ βπ§β*π€ π€(π₯ β π΄ β¦ β© {π β ran π β£ (β‘πβπ) β (π« π΅ β {β
})})π§)) |
113 | 56, 111, 112 | sylanbrc 584 |
. . . . . . . . . . 11
β’ (((π β TopBases β§ π:πβ1-1βΟ) β§ (βπ₯ β π΄ π΅ β ((topGenβπ) β {β
}) β§ βπ¦β*π₯ β π΄ π¦ β π΅)) β (π₯ β π΄ β¦ β© {π β ran π β£ (β‘πβπ) β (π« π΅ β {β
})}):π΄β1-1βΟ) |
114 | | f1domg 8915 |
. . . . . . . . . . 11
β’ (Ο
β V β ((π₯ β
π΄ β¦ β© {π
β ran π β£ (β‘πβπ) β (π« π΅ β {β
})}):π΄β1-1βΟ β π΄ βΌ Ο)) |
115 | 2, 113, 114 | mpsyl 68 |
. . . . . . . . . 10
β’ (((π β TopBases β§ π:πβ1-1βΟ) β§ (βπ₯ β π΄ π΅ β ((topGenβπ) β {β
}) β§ βπ¦β*π₯ β π΄ π¦ β π΅)) β π΄ βΌ Ο) |
116 | 115 | ex 414 |
. . . . . . . . 9
β’ ((π β TopBases β§ π:πβ1-1βΟ) β ((βπ₯ β π΄ π΅ β ((topGenβπ) β {β
}) β§ βπ¦β*π₯ β π΄ π¦ β π΅) β π΄ βΌ Ο)) |
117 | | difeq1 4076 |
. . . . . . . . . . . . 13
β’
((topGenβπ) =
π½ β
((topGenβπ) β
{β
}) = (π½ β
{β
})) |
118 | 117 | eleq2d 2820 |
. . . . . . . . . . . 12
β’
((topGenβπ) =
π½ β (π΅ β ((topGenβπ) β {β
}) β π΅ β (π½ β {β
}))) |
119 | 118 | ralbidv 3171 |
. . . . . . . . . . 11
β’
((topGenβπ) =
π½ β (βπ₯ β π΄ π΅ β ((topGenβπ) β {β
}) β βπ₯ β π΄ π΅ β (π½ β {β
}))) |
120 | 119 | anbi1d 631 |
. . . . . . . . . 10
β’
((topGenβπ) =
π½ β ((βπ₯ β π΄ π΅ β ((topGenβπ) β {β
}) β§ βπ¦β*π₯ β π΄ π¦ β π΅) β (βπ₯ β π΄ π΅ β (π½ β {β
}) β§ βπ¦β*π₯ β π΄ π¦ β π΅))) |
121 | 120 | imbi1d 342 |
. . . . . . . . 9
β’
((topGenβπ) =
π½ β (((βπ₯ β π΄ π΅ β ((topGenβπ) β {β
}) β§ βπ¦β*π₯ β π΄ π¦ β π΅) β π΄ βΌ Ο) β ((βπ₯ β π΄ π΅ β (π½ β {β
}) β§ βπ¦β*π₯ β π΄ π¦ β π΅) β π΄ βΌ Ο))) |
122 | 116, 121 | syl5ibcom 244 |
. . . . . . . 8
β’ ((π β TopBases β§ π:πβ1-1βΟ) β ((topGenβπ) = π½ β ((βπ₯ β π΄ π΅ β (π½ β {β
}) β§ βπ¦β*π₯ β π΄ π¦ β π΅) β π΄ βΌ Ο))) |
123 | 122 | ex 414 |
. . . . . . 7
β’ (π β TopBases β (π:πβ1-1βΟ β ((topGenβπ) = π½ β ((βπ₯ β π΄ π΅ β (π½ β {β
}) β§ βπ¦β*π₯ β π΄ π¦ β π΅) β π΄ βΌ Ο)))) |
124 | 123 | exlimdv 1937 |
. . . . . 6
β’ (π β TopBases β
(βπ π:πβ1-1βΟ β ((topGenβπ) = π½ β ((βπ₯ β π΄ π΅ β (π½ β {β
}) β§ βπ¦β*π₯ β π΄ π¦ β π΅) β π΄ βΌ Ο)))) |
125 | 3, 124 | biimtrid 241 |
. . . . 5
β’ (π β TopBases β (π βΌ Ο β
((topGenβπ) = π½ β ((βπ₯ β π΄ π΅ β (π½ β {β
}) β§ βπ¦β*π₯ β π΄ π¦ β π΅) β π΄ βΌ Ο)))) |
126 | 125 | impd 412 |
. . . 4
β’ (π β TopBases β ((π βΌ Ο β§
(topGenβπ) = π½) β ((βπ₯ β π΄ π΅ β (π½ β {β
}) β§ βπ¦β*π₯ β π΄ π¦ β π΅) β π΄ βΌ Ο))) |
127 | 126 | rexlimiv 3142 |
. . 3
β’
(βπ β
TopBases (π βΌ Ο
β§ (topGenβπ) =
π½) β ((βπ₯ β π΄ π΅ β (π½ β {β
}) β§ βπ¦β*π₯ β π΄ π¦ β π΅) β π΄ βΌ Ο)) |
128 | 1, 127 | sylbi 216 |
. 2
β’ (π½ β 2ndΟ
β ((βπ₯ β
π΄ π΅ β (π½ β {β
}) β§ βπ¦β*π₯ β π΄ π¦ β π΅) β π΄ βΌ Ο)) |
129 | 128 | 3impib 1117 |
1
β’ ((π½ β 2ndΟ
β§ βπ₯ β
π΄ π΅ β (π½ β {β
}) β§ βπ¦β*π₯ β π΄ π¦ β π΅) β π΄ βΌ Ο) |