Step | Hyp | Ref
| Expression |
1 | | 2ndcomap.5 |
. . . . . 6
β’ (π β πΉ β (π½ Cn πΎ)) |
2 | | cntop2 22595 |
. . . . . 6
β’ (πΉ β (π½ Cn πΎ) β πΎ β Top) |
3 | 1, 2 | syl 17 |
. . . . 5
β’ (π β πΎ β Top) |
4 | 3 | ad2antrr 725 |
. . . 4
β’ (((π β§ π β TopBases) β§ (π βΌ Ο β§ (topGenβπ) = π½)) β πΎ β Top) |
5 | | simplll 774 |
. . . . . . 7
β’ ((((π β§ π β TopBases) β§ (π βΌ Ο β§ (topGenβπ) = π½)) β§ π₯ β π) β π) |
6 | | bastg 22319 |
. . . . . . . . . 10
β’ (π β TopBases β π β (topGenβπ)) |
7 | 6 | ad2antlr 726 |
. . . . . . . . 9
β’ (((π β§ π β TopBases) β§ (π βΌ Ο β§ (topGenβπ) = π½)) β π β (topGenβπ)) |
8 | | simprr 772 |
. . . . . . . . 9
β’ (((π β§ π β TopBases) β§ (π βΌ Ο β§ (topGenβπ) = π½)) β (topGenβπ) = π½) |
9 | 7, 8 | sseqtrd 3985 |
. . . . . . . 8
β’ (((π β§ π β TopBases) β§ (π βΌ Ο β§ (topGenβπ) = π½)) β π β π½) |
10 | 9 | sselda 3945 |
. . . . . . 7
β’ ((((π β§ π β TopBases) β§ (π βΌ Ο β§ (topGenβπ) = π½)) β§ π₯ β π) β π₯ β π½) |
11 | | 2ndcomap.7 |
. . . . . . 7
β’ ((π β§ π₯ β π½) β (πΉ β π₯) β πΎ) |
12 | 5, 10, 11 | syl2anc 585 |
. . . . . 6
β’ ((((π β§ π β TopBases) β§ (π βΌ Ο β§ (topGenβπ) = π½)) β§ π₯ β π) β (πΉ β π₯) β πΎ) |
13 | 12 | fmpttd 7064 |
. . . . 5
β’ (((π β§ π β TopBases) β§ (π βΌ Ο β§ (topGenβπ) = π½)) β (π₯ β π β¦ (πΉ β π₯)):πβΆπΎ) |
14 | 13 | frnd 6677 |
. . . 4
β’ (((π β§ π β TopBases) β§ (π βΌ Ο β§ (topGenβπ) = π½)) β ran (π₯ β π β¦ (πΉ β π₯)) β πΎ) |
15 | | elunii 4871 |
. . . . . . . . . . 11
β’ ((π§ β π β§ π β πΎ) β π§ β βͺ πΎ) |
16 | | 2ndcomap.2 |
. . . . . . . . . . 11
β’ π = βͺ
πΎ |
17 | 15, 16 | eleqtrrdi 2849 |
. . . . . . . . . 10
β’ ((π§ β π β§ π β πΎ) β π§ β π) |
18 | 17 | ancoms 460 |
. . . . . . . . 9
β’ ((π β πΎ β§ π§ β π) β π§ β π) |
19 | 18 | adantl 483 |
. . . . . . . 8
β’ ((((π β§ π β TopBases) β§ (π βΌ Ο β§ (topGenβπ) = π½)) β§ (π β πΎ β§ π§ β π)) β π§ β π) |
20 | | 2ndcomap.6 |
. . . . . . . . 9
β’ (π β ran πΉ = π) |
21 | 20 | ad3antrrr 729 |
. . . . . . . 8
β’ ((((π β§ π β TopBases) β§ (π βΌ Ο β§ (topGenβπ) = π½)) β§ (π β πΎ β§ π§ β π)) β ran πΉ = π) |
22 | 19, 21 | eleqtrrd 2841 |
. . . . . . 7
β’ ((((π β§ π β TopBases) β§ (π βΌ Ο β§ (topGenβπ) = π½)) β§ (π β πΎ β§ π§ β π)) β π§ β ran πΉ) |
23 | | eqid 2737 |
. . . . . . . . . . 11
β’ βͺ π½ =
βͺ π½ |
24 | 23, 16 | cnf 22600 |
. . . . . . . . . 10
β’ (πΉ β (π½ Cn πΎ) β πΉ:βͺ π½βΆπ) |
25 | 1, 24 | syl 17 |
. . . . . . . . 9
β’ (π β πΉ:βͺ π½βΆπ) |
26 | 25 | ad3antrrr 729 |
. . . . . . . 8
β’ ((((π β§ π β TopBases) β§ (π βΌ Ο β§ (topGenβπ) = π½)) β§ (π β πΎ β§ π§ β π)) β πΉ:βͺ π½βΆπ) |
27 | | ffn 6669 |
. . . . . . . 8
β’ (πΉ:βͺ
π½βΆπ β πΉ Fn βͺ π½) |
28 | | fvelrnb 6904 |
. . . . . . . 8
β’ (πΉ Fn βͺ
π½ β (π§ β ran πΉ β βπ‘ β βͺ π½(πΉβπ‘) = π§)) |
29 | 26, 27, 28 | 3syl 18 |
. . . . . . 7
β’ ((((π β§ π β TopBases) β§ (π βΌ Ο β§ (topGenβπ) = π½)) β§ (π β πΎ β§ π§ β π)) β (π§ β ran πΉ β βπ‘ β βͺ π½(πΉβπ‘) = π§)) |
30 | 22, 29 | mpbid 231 |
. . . . . 6
β’ ((((π β§ π β TopBases) β§ (π βΌ Ο β§ (topGenβπ) = π½)) β§ (π β πΎ β§ π§ β π)) β βπ‘ β βͺ π½(πΉβπ‘) = π§) |
31 | 1 | ad3antrrr 729 |
. . . . . . . . . . 11
β’ ((((π β§ π β TopBases) β§ (π βΌ Ο β§ (topGenβπ) = π½)) β§ ((π β πΎ β§ π§ β π) β§ (π‘ β βͺ π½ β§ (πΉβπ‘) = π§))) β πΉ β (π½ Cn πΎ)) |
32 | | simprll 778 |
. . . . . . . . . . 11
β’ ((((π β§ π β TopBases) β§ (π βΌ Ο β§ (topGenβπ) = π½)) β§ ((π β πΎ β§ π§ β π) β§ (π‘ β βͺ π½ β§ (πΉβπ‘) = π§))) β π β πΎ) |
33 | | cnima 22619 |
. . . . . . . . . . 11
β’ ((πΉ β (π½ Cn πΎ) β§ π β πΎ) β (β‘πΉ β π) β π½) |
34 | 31, 32, 33 | syl2anc 585 |
. . . . . . . . . 10
β’ ((((π β§ π β TopBases) β§ (π βΌ Ο β§ (topGenβπ) = π½)) β§ ((π β πΎ β§ π§ β π) β§ (π‘ β βͺ π½ β§ (πΉβπ‘) = π§))) β (β‘πΉ β π) β π½) |
35 | 8 | adantr 482 |
. . . . . . . . . 10
β’ ((((π β§ π β TopBases) β§ (π βΌ Ο β§ (topGenβπ) = π½)) β§ ((π β πΎ β§ π§ β π) β§ (π‘ β βͺ π½ β§ (πΉβπ‘) = π§))) β (topGenβπ) = π½) |
36 | 34, 35 | eleqtrrd 2841 |
. . . . . . . . 9
β’ ((((π β§ π β TopBases) β§ (π βΌ Ο β§ (topGenβπ) = π½)) β§ ((π β πΎ β§ π§ β π) β§ (π‘ β βͺ π½ β§ (πΉβπ‘) = π§))) β (β‘πΉ β π) β (topGenβπ)) |
37 | | simprrl 780 |
. . . . . . . . . 10
β’ ((((π β§ π β TopBases) β§ (π βΌ Ο β§ (topGenβπ) = π½)) β§ ((π β πΎ β§ π§ β π) β§ (π‘ β βͺ π½ β§ (πΉβπ‘) = π§))) β π‘ β βͺ π½) |
38 | | simprrr 781 |
. . . . . . . . . . 11
β’ ((((π β§ π β TopBases) β§ (π βΌ Ο β§ (topGenβπ) = π½)) β§ ((π β πΎ β§ π§ β π) β§ (π‘ β βͺ π½ β§ (πΉβπ‘) = π§))) β (πΉβπ‘) = π§) |
39 | | simprlr 779 |
. . . . . . . . . . 11
β’ ((((π β§ π β TopBases) β§ (π βΌ Ο β§ (topGenβπ) = π½)) β§ ((π β πΎ β§ π§ β π) β§ (π‘ β βͺ π½ β§ (πΉβπ‘) = π§))) β π§ β π) |
40 | 38, 39 | eqeltrd 2838 |
. . . . . . . . . 10
β’ ((((π β§ π β TopBases) β§ (π βΌ Ο β§ (topGenβπ) = π½)) β§ ((π β πΎ β§ π§ β π) β§ (π‘ β βͺ π½ β§ (πΉβπ‘) = π§))) β (πΉβπ‘) β π) |
41 | 26 | ffnd 6670 |
. . . . . . . . . . . 12
β’ ((((π β§ π β TopBases) β§ (π βΌ Ο β§ (topGenβπ) = π½)) β§ (π β πΎ β§ π§ β π)) β πΉ Fn βͺ π½) |
42 | 41 | adantrr 716 |
. . . . . . . . . . 11
β’ ((((π β§ π β TopBases) β§ (π βΌ Ο β§ (topGenβπ) = π½)) β§ ((π β πΎ β§ π§ β π) β§ (π‘ β βͺ π½ β§ (πΉβπ‘) = π§))) β πΉ Fn βͺ π½) |
43 | | elpreima 7009 |
. . . . . . . . . . 11
β’ (πΉ Fn βͺ
π½ β (π‘ β (β‘πΉ β π) β (π‘ β βͺ π½ β§ (πΉβπ‘) β π))) |
44 | 42, 43 | syl 17 |
. . . . . . . . . 10
β’ ((((π β§ π β TopBases) β§ (π βΌ Ο β§ (topGenβπ) = π½)) β§ ((π β πΎ β§ π§ β π) β§ (π‘ β βͺ π½ β§ (πΉβπ‘) = π§))) β (π‘ β (β‘πΉ β π) β (π‘ β βͺ π½ β§ (πΉβπ‘) β π))) |
45 | 37, 40, 44 | mpbir2and 712 |
. . . . . . . . 9
β’ ((((π β§ π β TopBases) β§ (π βΌ Ο β§ (topGenβπ) = π½)) β§ ((π β πΎ β§ π§ β π) β§ (π‘ β βͺ π½ β§ (πΉβπ‘) = π§))) β π‘ β (β‘πΉ β π)) |
46 | | tg2 22318 |
. . . . . . . . 9
β’ (((β‘πΉ β π) β (topGenβπ) β§ π‘ β (β‘πΉ β π)) β βπ β π (π‘ β π β§ π β (β‘πΉ β π))) |
47 | 36, 45, 46 | syl2anc 585 |
. . . . . . . 8
β’ ((((π β§ π β TopBases) β§ (π βΌ Ο β§ (topGenβπ) = π½)) β§ ((π β πΎ β§ π§ β π) β§ (π‘ β βͺ π½ β§ (πΉβπ‘) = π§))) β βπ β π (π‘ β π β§ π β (β‘πΉ β π))) |
48 | | simprl 770 |
. . . . . . . . . . 11
β’
(((((π β§ π β TopBases) β§ (π βΌ Ο β§
(topGenβπ) = π½)) β§ ((π β πΎ β§ π§ β π) β§ (π‘ β βͺ π½ β§ (πΉβπ‘) = π§))) β§ (π β π β§ (π‘ β π β§ π β (β‘πΉ β π)))) β π β π) |
49 | | eqid 2737 |
. . . . . . . . . . 11
β’ (πΉ β π) = (πΉ β π) |
50 | | imaeq2 6010 |
. . . . . . . . . . . 12
β’ (π₯ = π β (πΉ β π₯) = (πΉ β π)) |
51 | 50 | rspceeqv 3596 |
. . . . . . . . . . 11
β’ ((π β π β§ (πΉ β π) = (πΉ β π)) β βπ₯ β π (πΉ β π) = (πΉ β π₯)) |
52 | 48, 49, 51 | sylancl 587 |
. . . . . . . . . 10
β’
(((((π β§ π β TopBases) β§ (π βΌ Ο β§
(topGenβπ) = π½)) β§ ((π β πΎ β§ π§ β π) β§ (π‘ β βͺ π½ β§ (πΉβπ‘) = π§))) β§ (π β π β§ (π‘ β π β§ π β (β‘πΉ β π)))) β βπ₯ β π (πΉ β π) = (πΉ β π₯)) |
53 | 42 | adantr 482 |
. . . . . . . . . . . . . 14
β’
(((((π β§ π β TopBases) β§ (π βΌ Ο β§
(topGenβπ) = π½)) β§ ((π β πΎ β§ π§ β π) β§ (π‘ β βͺ π½ β§ (πΉβπ‘) = π§))) β§ (π β π β§ (π‘ β π β§ π β (β‘πΉ β π)))) β πΉ Fn βͺ π½) |
54 | | fnfun 6603 |
. . . . . . . . . . . . . 14
β’ (πΉ Fn βͺ
π½ β Fun πΉ) |
55 | 53, 54 | syl 17 |
. . . . . . . . . . . . 13
β’
(((((π β§ π β TopBases) β§ (π βΌ Ο β§
(topGenβπ) = π½)) β§ ((π β πΎ β§ π§ β π) β§ (π‘ β βͺ π½ β§ (πΉβπ‘) = π§))) β§ (π β π β§ (π‘ β π β§ π β (β‘πΉ β π)))) β Fun πΉ) |
56 | | simprrr 781 |
. . . . . . . . . . . . 13
β’
(((((π β§ π β TopBases) β§ (π βΌ Ο β§
(topGenβπ) = π½)) β§ ((π β πΎ β§ π§ β π) β§ (π‘ β βͺ π½ β§ (πΉβπ‘) = π§))) β§ (π β π β§ (π‘ β π β§ π β (β‘πΉ β π)))) β π β (β‘πΉ β π)) |
57 | | funimass2 6585 |
. . . . . . . . . . . . 13
β’ ((Fun
πΉ β§ π β (β‘πΉ β π)) β (πΉ β π) β π) |
58 | 55, 56, 57 | syl2anc 585 |
. . . . . . . . . . . 12
β’
(((((π β§ π β TopBases) β§ (π βΌ Ο β§
(topGenβπ) = π½)) β§ ((π β πΎ β§ π§ β π) β§ (π‘ β βͺ π½ β§ (πΉβπ‘) = π§))) β§ (π β π β§ (π‘ β π β§ π β (β‘πΉ β π)))) β (πΉ β π) β π) |
59 | | vex 3450 |
. . . . . . . . . . . 12
β’ π β V |
60 | | ssexg 5281 |
. . . . . . . . . . . 12
β’ (((πΉ β π) β π β§ π β V) β (πΉ β π) β V) |
61 | 58, 59, 60 | sylancl 587 |
. . . . . . . . . . 11
β’
(((((π β§ π β TopBases) β§ (π βΌ Ο β§
(topGenβπ) = π½)) β§ ((π β πΎ β§ π§ β π) β§ (π‘ β βͺ π½ β§ (πΉβπ‘) = π§))) β§ (π β π β§ (π‘ β π β§ π β (β‘πΉ β π)))) β (πΉ β π) β V) |
62 | | eqid 2737 |
. . . . . . . . . . . 12
β’ (π₯ β π β¦ (πΉ β π₯)) = (π₯ β π β¦ (πΉ β π₯)) |
63 | 62 | elrnmpt 5912 |
. . . . . . . . . . 11
β’ ((πΉ β π) β V β ((πΉ β π) β ran (π₯ β π β¦ (πΉ β π₯)) β βπ₯ β π (πΉ β π) = (πΉ β π₯))) |
64 | 61, 63 | syl 17 |
. . . . . . . . . 10
β’
(((((π β§ π β TopBases) β§ (π βΌ Ο β§
(topGenβπ) = π½)) β§ ((π β πΎ β§ π§ β π) β§ (π‘ β βͺ π½ β§ (πΉβπ‘) = π§))) β§ (π β π β§ (π‘ β π β§ π β (β‘πΉ β π)))) β ((πΉ β π) β ran (π₯ β π β¦ (πΉ β π₯)) β βπ₯ β π (πΉ β π) = (πΉ β π₯))) |
65 | 52, 64 | mpbird 257 |
. . . . . . . . 9
β’
(((((π β§ π β TopBases) β§ (π βΌ Ο β§
(topGenβπ) = π½)) β§ ((π β πΎ β§ π§ β π) β§ (π‘ β βͺ π½ β§ (πΉβπ‘) = π§))) β§ (π β π β§ (π‘ β π β§ π β (β‘πΉ β π)))) β (πΉ β π) β ran (π₯ β π β¦ (πΉ β π₯))) |
66 | 38 | adantr 482 |
. . . . . . . . . 10
β’
(((((π β§ π β TopBases) β§ (π βΌ Ο β§
(topGenβπ) = π½)) β§ ((π β πΎ β§ π§ β π) β§ (π‘ β βͺ π½ β§ (πΉβπ‘) = π§))) β§ (π β π β§ (π‘ β π β§ π β (β‘πΉ β π)))) β (πΉβπ‘) = π§) |
67 | | simprrl 780 |
. . . . . . . . . . 11
β’
(((((π β§ π β TopBases) β§ (π βΌ Ο β§
(topGenβπ) = π½)) β§ ((π β πΎ β§ π§ β π) β§ (π‘ β βͺ π½ β§ (πΉβπ‘) = π§))) β§ (π β π β§ (π‘ β π β§ π β (β‘πΉ β π)))) β π‘ β π) |
68 | | cnvimass 6034 |
. . . . . . . . . . . . 13
β’ (β‘πΉ β π) β dom πΉ |
69 | 56, 68 | sstrdi 3957 |
. . . . . . . . . . . 12
β’
(((((π β§ π β TopBases) β§ (π βΌ Ο β§
(topGenβπ) = π½)) β§ ((π β πΎ β§ π§ β π) β§ (π‘ β βͺ π½ β§ (πΉβπ‘) = π§))) β§ (π β π β§ (π‘ β π β§ π β (β‘πΉ β π)))) β π β dom πΉ) |
70 | | funfvima2 7182 |
. . . . . . . . . . . 12
β’ ((Fun
πΉ β§ π β dom πΉ) β (π‘ β π β (πΉβπ‘) β (πΉ β π))) |
71 | 55, 69, 70 | syl2anc 585 |
. . . . . . . . . . 11
β’
(((((π β§ π β TopBases) β§ (π βΌ Ο β§
(topGenβπ) = π½)) β§ ((π β πΎ β§ π§ β π) β§ (π‘ β βͺ π½ β§ (πΉβπ‘) = π§))) β§ (π β π β§ (π‘ β π β§ π β (β‘πΉ β π)))) β (π‘ β π β (πΉβπ‘) β (πΉ β π))) |
72 | 67, 71 | mpd 15 |
. . . . . . . . . 10
β’
(((((π β§ π β TopBases) β§ (π βΌ Ο β§
(topGenβπ) = π½)) β§ ((π β πΎ β§ π§ β π) β§ (π‘ β βͺ π½ β§ (πΉβπ‘) = π§))) β§ (π β π β§ (π‘ β π β§ π β (β‘πΉ β π)))) β (πΉβπ‘) β (πΉ β π)) |
73 | 66, 72 | eqeltrrd 2839 |
. . . . . . . . 9
β’
(((((π β§ π β TopBases) β§ (π βΌ Ο β§
(topGenβπ) = π½)) β§ ((π β πΎ β§ π§ β π) β§ (π‘ β βͺ π½ β§ (πΉβπ‘) = π§))) β§ (π β π β§ (π‘ β π β§ π β (β‘πΉ β π)))) β π§ β (πΉ β π)) |
74 | | eleq2 2827 |
. . . . . . . . . . 11
β’ (π€ = (πΉ β π) β (π§ β π€ β π§ β (πΉ β π))) |
75 | | sseq1 3970 |
. . . . . . . . . . 11
β’ (π€ = (πΉ β π) β (π€ β π β (πΉ β π) β π)) |
76 | 74, 75 | anbi12d 632 |
. . . . . . . . . 10
β’ (π€ = (πΉ β π) β ((π§ β π€ β§ π€ β π) β (π§ β (πΉ β π) β§ (πΉ β π) β π))) |
77 | 76 | rspcev 3582 |
. . . . . . . . 9
β’ (((πΉ β π) β ran (π₯ β π β¦ (πΉ β π₯)) β§ (π§ β (πΉ β π) β§ (πΉ β π) β π)) β βπ€ β ran (π₯ β π β¦ (πΉ β π₯))(π§ β π€ β§ π€ β π)) |
78 | 65, 73, 58, 77 | syl12anc 836 |
. . . . . . . 8
β’
(((((π β§ π β TopBases) β§ (π βΌ Ο β§
(topGenβπ) = π½)) β§ ((π β πΎ β§ π§ β π) β§ (π‘ β βͺ π½ β§ (πΉβπ‘) = π§))) β§ (π β π β§ (π‘ β π β§ π β (β‘πΉ β π)))) β βπ€ β ran (π₯ β π β¦ (πΉ β π₯))(π§ β π€ β§ π€ β π)) |
79 | 47, 78 | rexlimddv 3159 |
. . . . . . 7
β’ ((((π β§ π β TopBases) β§ (π βΌ Ο β§ (topGenβπ) = π½)) β§ ((π β πΎ β§ π§ β π) β§ (π‘ β βͺ π½ β§ (πΉβπ‘) = π§))) β βπ€ β ran (π₯ β π β¦ (πΉ β π₯))(π§ β π€ β§ π€ β π)) |
80 | 79 | anassrs 469 |
. . . . . 6
β’
(((((π β§ π β TopBases) β§ (π βΌ Ο β§
(topGenβπ) = π½)) β§ (π β πΎ β§ π§ β π)) β§ (π‘ β βͺ π½ β§ (πΉβπ‘) = π§)) β βπ€ β ran (π₯ β π β¦ (πΉ β π₯))(π§ β π€ β§ π€ β π)) |
81 | 30, 80 | rexlimddv 3159 |
. . . . 5
β’ ((((π β§ π β TopBases) β§ (π βΌ Ο β§ (topGenβπ) = π½)) β§ (π β πΎ β§ π§ β π)) β βπ€ β ran (π₯ β π β¦ (πΉ β π₯))(π§ β π€ β§ π€ β π)) |
82 | 81 | ralrimivva 3198 |
. . . 4
β’ (((π β§ π β TopBases) β§ (π βΌ Ο β§ (topGenβπ) = π½)) β βπ β πΎ βπ§ β π βπ€ β ran (π₯ β π β¦ (πΉ β π₯))(π§ β π€ β§ π€ β π)) |
83 | | basgen2 22342 |
. . . 4
β’ ((πΎ β Top β§ ran (π₯ β π β¦ (πΉ β π₯)) β πΎ β§ βπ β πΎ βπ§ β π βπ€ β ran (π₯ β π β¦ (πΉ β π₯))(π§ β π€ β§ π€ β π)) β (topGenβran (π₯ β π β¦ (πΉ β π₯))) = πΎ) |
84 | 4, 14, 82, 83 | syl3anc 1372 |
. . 3
β’ (((π β§ π β TopBases) β§ (π βΌ Ο β§ (topGenβπ) = π½)) β (topGenβran (π₯ β π β¦ (πΉ β π₯))) = πΎ) |
85 | 84, 4 | eqeltrd 2838 |
. . . . 5
β’ (((π β§ π β TopBases) β§ (π βΌ Ο β§ (topGenβπ) = π½)) β (topGenβran (π₯ β π β¦ (πΉ β π₯))) β Top) |
86 | | tgclb 22323 |
. . . . 5
β’ (ran
(π₯ β π β¦ (πΉ β π₯)) β TopBases β (topGenβran
(π₯ β π β¦ (πΉ β π₯))) β Top) |
87 | 85, 86 | sylibr 233 |
. . . 4
β’ (((π β§ π β TopBases) β§ (π βΌ Ο β§ (topGenβπ) = π½)) β ran (π₯ β π β¦ (πΉ β π₯)) β TopBases) |
88 | | omelon 9583 |
. . . . . . 7
β’ Ο
β On |
89 | | simprl 770 |
. . . . . . 7
β’ (((π β§ π β TopBases) β§ (π βΌ Ο β§ (topGenβπ) = π½)) β π βΌ Ο) |
90 | | ondomen 9974 |
. . . . . . 7
β’ ((Ο
β On β§ π βΌ
Ο) β π β
dom card) |
91 | 88, 89, 90 | sylancr 588 |
. . . . . 6
β’ (((π β§ π β TopBases) β§ (π βΌ Ο β§ (topGenβπ) = π½)) β π β dom card) |
92 | 13 | ffnd 6670 |
. . . . . . 7
β’ (((π β§ π β TopBases) β§ (π βΌ Ο β§ (topGenβπ) = π½)) β (π₯ β π β¦ (πΉ β π₯)) Fn π) |
93 | | dffn4 6763 |
. . . . . . 7
β’ ((π₯ β π β¦ (πΉ β π₯)) Fn π β (π₯ β π β¦ (πΉ β π₯)):πβontoβran (π₯ β π β¦ (πΉ β π₯))) |
94 | 92, 93 | sylib 217 |
. . . . . 6
β’ (((π β§ π β TopBases) β§ (π βΌ Ο β§ (topGenβπ) = π½)) β (π₯ β π β¦ (πΉ β π₯)):πβontoβran (π₯ β π β¦ (πΉ β π₯))) |
95 | | fodomnum 9994 |
. . . . . 6
β’ (π β dom card β ((π₯ β π β¦ (πΉ β π₯)):πβontoβran (π₯ β π β¦ (πΉ β π₯)) β ran (π₯ β π β¦ (πΉ β π₯)) βΌ π)) |
96 | 91, 94, 95 | sylc 65 |
. . . . 5
β’ (((π β§ π β TopBases) β§ (π βΌ Ο β§ (topGenβπ) = π½)) β ran (π₯ β π β¦ (πΉ β π₯)) βΌ π) |
97 | | domtr 8948 |
. . . . 5
β’ ((ran
(π₯ β π β¦ (πΉ β π₯)) βΌ π β§ π βΌ Ο) β ran (π₯ β π β¦ (πΉ β π₯)) βΌ Ο) |
98 | 96, 89, 97 | syl2anc 585 |
. . . 4
β’ (((π β§ π β TopBases) β§ (π βΌ Ο β§ (topGenβπ) = π½)) β ran (π₯ β π β¦ (πΉ β π₯)) βΌ Ο) |
99 | | 2ndci 22802 |
. . . 4
β’ ((ran
(π₯ β π β¦ (πΉ β π₯)) β TopBases β§ ran (π₯ β π β¦ (πΉ β π₯)) βΌ Ο) β (topGenβran
(π₯ β π β¦ (πΉ β π₯))) β
2ndΟ) |
100 | 87, 98, 99 | syl2anc 585 |
. . 3
β’ (((π β§ π β TopBases) β§ (π βΌ Ο β§ (topGenβπ) = π½)) β (topGenβran (π₯ β π β¦ (πΉ β π₯))) β
2ndΟ) |
101 | 84, 100 | eqeltrrd 2839 |
. 2
β’ (((π β§ π β TopBases) β§ (π βΌ Ο β§ (topGenβπ) = π½)) β πΎ β
2ndΟ) |
102 | | 2ndcomap.3 |
. . 3
β’ (π β π½ β
2ndΟ) |
103 | | is2ndc 22800 |
. . 3
β’ (π½ β 2ndΟ
β βπ β
TopBases (π βΌ Ο
β§ (topGenβπ) =
π½)) |
104 | 102, 103 | sylib 217 |
. 2
β’ (π β βπ β TopBases (π βΌ Ο β§ (topGenβπ) = π½)) |
105 | 101, 104 | r19.29a 3160 |
1
β’ (π β πΎ β
2ndΟ) |