Step | Hyp | Ref
| Expression |
1 | | is2ndc 22813 |
. 2
β’ (π½ β 2ndΟ
β βπ β
TopBases (π βΌ Ο
β§ (topGenβπ) =
π½)) |
2 | | vex 3448 |
. . . . . . . . 9
β’ π β V |
3 | | difss 4092 |
. . . . . . . . 9
β’ (π β {β
}) β
π |
4 | | ssdomg 8943 |
. . . . . . . . 9
β’ (π β V β ((π β {β
}) β
π β (π β {β
}) βΌ
π)) |
5 | 2, 3, 4 | mp2 9 |
. . . . . . . 8
β’ (π β {β
}) βΌ
π |
6 | | simpr 486 |
. . . . . . . 8
β’ ((π β TopBases β§ π βΌ Ο) β π βΌ
Ο) |
7 | | domtr 8950 |
. . . . . . . 8
β’ (((π β {β
}) βΌ
π β§ π βΌ Ο) β (π β {β
}) βΌ
Ο) |
8 | 5, 6, 7 | sylancr 588 |
. . . . . . 7
β’ ((π β TopBases β§ π βΌ Ο) β (π β {β
}) βΌ
Ο) |
9 | | eldifsn 4748 |
. . . . . . . . 9
β’ (π¦ β (π β {β
}) β (π¦ β π β§ π¦ β β
)) |
10 | | n0 4307 |
. . . . . . . . . 10
β’ (π¦ β β
β
βπ§ π§ β π¦) |
11 | | elunii 4871 |
. . . . . . . . . . . . . . 15
β’ ((π§ β π¦ β§ π¦ β π) β π§ β βͺ π) |
12 | | simpl 484 |
. . . . . . . . . . . . . . 15
β’ ((π§ β π¦ β§ π¦ β π) β π§ β π¦) |
13 | 11, 12 | jca 513 |
. . . . . . . . . . . . . 14
β’ ((π§ β π¦ β§ π¦ β π) β (π§ β βͺ π β§ π§ β π¦)) |
14 | 13 | expcom 415 |
. . . . . . . . . . . . 13
β’ (π¦ β π β (π§ β π¦ β (π§ β βͺ π β§ π§ β π¦))) |
15 | 14 | eximdv 1921 |
. . . . . . . . . . . 12
β’ (π¦ β π β (βπ§ π§ β π¦ β βπ§(π§ β βͺ π β§ π§ β π¦))) |
16 | 15 | imp 408 |
. . . . . . . . . . 11
β’ ((π¦ β π β§ βπ§ π§ β π¦) β βπ§(π§ β βͺ π β§ π§ β π¦)) |
17 | | df-rex 3071 |
. . . . . . . . . . 11
β’
(βπ§ β
βͺ ππ§ β π¦ β βπ§(π§ β βͺ π β§ π§ β π¦)) |
18 | 16, 17 | sylibr 233 |
. . . . . . . . . 10
β’ ((π¦ β π β§ βπ§ π§ β π¦) β βπ§ β βͺ ππ§ β π¦) |
19 | 10, 18 | sylan2b 595 |
. . . . . . . . 9
β’ ((π¦ β π β§ π¦ β β
) β βπ§ β βͺ ππ§ β π¦) |
20 | 9, 19 | sylbi 216 |
. . . . . . . 8
β’ (π¦ β (π β {β
}) β βπ§ β βͺ ππ§ β π¦) |
21 | 20 | rgen 3063 |
. . . . . . 7
β’
βπ¦ β
(π β
{β
})βπ§ β
βͺ ππ§ β π¦ |
22 | | vuniex 7677 |
. . . . . . . 8
β’ βͺ π
β V |
23 | | eleq1 2822 |
. . . . . . . 8
β’ (π§ = (πβπ¦) β (π§ β π¦ β (πβπ¦) β π¦)) |
24 | 22, 23 | axcc4dom 10382 |
. . . . . . 7
β’ (((π β {β
}) βΌ
Ο β§ βπ¦
β (π β
{β
})βπ§ β
βͺ ππ§ β π¦) β βπ(π:(π β {β
})βΆβͺ π
β§ βπ¦ β
(π β {β
})(πβπ¦) β π¦)) |
25 | 8, 21, 24 | sylancl 587 |
. . . . . 6
β’ ((π β TopBases β§ π βΌ Ο) β
βπ(π:(π β {β
})βΆβͺ π
β§ βπ¦ β
(π β {β
})(πβπ¦) β π¦)) |
26 | | frn 6676 |
. . . . . . . . 9
β’ (π:(π β {β
})βΆβͺ π
β ran π β βͺ π) |
27 | 26 | ad2antrl 727 |
. . . . . . . 8
β’ (((π β TopBases β§ π βΌ Ο) β§ (π:(π β {β
})βΆβͺ π
β§ βπ¦ β
(π β {β
})(πβπ¦) β π¦)) β ran π β βͺ π) |
28 | | vex 3448 |
. . . . . . . . . 10
β’ π β V |
29 | 28 | rnex 7850 |
. . . . . . . . 9
β’ ran π β V |
30 | 29 | elpw 4565 |
. . . . . . . 8
β’ (ran
π β π« βͺ π
β ran π β βͺ π) |
31 | 27, 30 | sylibr 233 |
. . . . . . 7
β’ (((π β TopBases β§ π βΌ Ο) β§ (π:(π β {β
})βΆβͺ π
β§ βπ¦ β
(π β {β
})(πβπ¦) β π¦)) β ran π β π« βͺ π) |
32 | | omelon 9587 |
. . . . . . . . . . 11
β’ Ο
β On |
33 | 6 | adantr 482 |
. . . . . . . . . . 11
β’ (((π β TopBases β§ π βΌ Ο) β§ (π:(π β {β
})βΆβͺ π
β§ βπ¦ β
(π β {β
})(πβπ¦) β π¦)) β π βΌ Ο) |
34 | | ondomen 9978 |
. . . . . . . . . . 11
β’ ((Ο
β On β§ π βΌ
Ο) β π β
dom card) |
35 | 32, 33, 34 | sylancr 588 |
. . . . . . . . . 10
β’ (((π β TopBases β§ π βΌ Ο) β§ (π:(π β {β
})βΆβͺ π
β§ βπ¦ β
(π β {β
})(πβπ¦) β π¦)) β π β dom card) |
36 | | ssnum 9980 |
. . . . . . . . . 10
β’ ((π β dom card β§ (π β {β
}) β
π) β (π β {β
}) β dom
card) |
37 | 35, 3, 36 | sylancl 587 |
. . . . . . . . 9
β’ (((π β TopBases β§ π βΌ Ο) β§ (π:(π β {β
})βΆβͺ π
β§ βπ¦ β
(π β {β
})(πβπ¦) β π¦)) β (π β {β
}) β dom
card) |
38 | | ffn 6669 |
. . . . . . . . . . 11
β’ (π:(π β {β
})βΆβͺ π
β π Fn (π β
{β
})) |
39 | 38 | ad2antrl 727 |
. . . . . . . . . 10
β’ (((π β TopBases β§ π βΌ Ο) β§ (π:(π β {β
})βΆβͺ π
β§ βπ¦ β
(π β {β
})(πβπ¦) β π¦)) β π Fn (π β {β
})) |
40 | | dffn4 6763 |
. . . . . . . . . 10
β’ (π Fn (π β {β
}) β π:(π β {β
})βontoβran π) |
41 | 39, 40 | sylib 217 |
. . . . . . . . 9
β’ (((π β TopBases β§ π βΌ Ο) β§ (π:(π β {β
})βΆβͺ π
β§ βπ¦ β
(π β {β
})(πβπ¦) β π¦)) β π:(π β {β
})βontoβran π) |
42 | | fodomnum 9998 |
. . . . . . . . 9
β’ ((π β {β
}) β dom
card β (π:(π β {β
})βontoβran π β ran π βΌ (π β {β
}))) |
43 | 37, 41, 42 | sylc 65 |
. . . . . . . 8
β’ (((π β TopBases β§ π βΌ Ο) β§ (π:(π β {β
})βΆβͺ π
β§ βπ¦ β
(π β {β
})(πβπ¦) β π¦)) β ran π βΌ (π β {β
})) |
44 | 8 | adantr 482 |
. . . . . . . 8
β’ (((π β TopBases β§ π βΌ Ο) β§ (π:(π β {β
})βΆβͺ π
β§ βπ¦ β
(π β {β
})(πβπ¦) β π¦)) β (π β {β
}) βΌ
Ο) |
45 | | domtr 8950 |
. . . . . . . 8
β’ ((ran
π βΌ (π β {β
}) β§ (π β {β
}) βΌ
Ο) β ran π
βΌ Ο) |
46 | 43, 44, 45 | syl2anc 585 |
. . . . . . 7
β’ (((π β TopBases β§ π βΌ Ο) β§ (π:(π β {β
})βΆβͺ π
β§ βπ¦ β
(π β {β
})(πβπ¦) β π¦)) β ran π βΌ Ο) |
47 | | tgcl 22335 |
. . . . . . . . . 10
β’ (π β TopBases β
(topGenβπ) β
Top) |
48 | 47 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β TopBases β§ π βΌ Ο) β§ (π:(π β {β
})βΆβͺ π
β§ βπ¦ β
(π β {β
})(πβπ¦) β π¦)) β (topGenβπ) β Top) |
49 | | unitg 22333 |
. . . . . . . . . . . 12
β’ (π β V β βͺ (topGenβπ) = βͺ π) |
50 | 49 | elv 3450 |
. . . . . . . . . . 11
β’ βͺ (topGenβπ) = βͺ π |
51 | 50 | eqcomi 2742 |
. . . . . . . . . 10
β’ βͺ π =
βͺ (topGenβπ) |
52 | 51 | clsss3 22426 |
. . . . . . . . 9
β’
(((topGenβπ)
β Top β§ ran π
β βͺ π) β ((clsβ(topGenβπ))βran π) β βͺ π) |
53 | 48, 27, 52 | syl2anc 585 |
. . . . . . . 8
β’ (((π β TopBases β§ π βΌ Ο) β§ (π:(π β {β
})βΆβͺ π
β§ βπ¦ β
(π β {β
})(πβπ¦) β π¦)) β ((clsβ(topGenβπ))βran π) β βͺ π) |
54 | | ne0i 4295 |
. . . . . . . . . . . . . . . 16
β’ (π₯ β π¦ β π¦ β β
) |
55 | 54 | anim2i 618 |
. . . . . . . . . . . . . . 15
β’ ((π¦ β π β§ π₯ β π¦) β (π¦ β π β§ π¦ β β
)) |
56 | 55, 9 | sylibr 233 |
. . . . . . . . . . . . . 14
β’ ((π¦ β π β§ π₯ β π¦) β π¦ β (π β {β
})) |
57 | | fnfvelrn 7032 |
. . . . . . . . . . . . . . . . . 18
β’ ((π Fn (π β {β
}) β§ π¦ β (π β {β
})) β (πβπ¦) β ran π) |
58 | 38, 57 | sylan 581 |
. . . . . . . . . . . . . . . . 17
β’ ((π:(π β {β
})βΆβͺ π
β§ π¦ β (π β {β
})) β
(πβπ¦) β ran π) |
59 | | inelcm 4425 |
. . . . . . . . . . . . . . . . . 18
β’ (((πβπ¦) β π¦ β§ (πβπ¦) β ran π) β (π¦ β© ran π) β β
) |
60 | 59 | expcom 415 |
. . . . . . . . . . . . . . . . 17
β’ ((πβπ¦) β ran π β ((πβπ¦) β π¦ β (π¦ β© ran π) β β
)) |
61 | 58, 60 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ ((π:(π β {β
})βΆβͺ π
β§ π¦ β (π β {β
})) β
((πβπ¦) β π¦ β (π¦ β© ran π) β β
)) |
62 | 61 | ex 414 |
. . . . . . . . . . . . . . 15
β’ (π:(π β {β
})βΆβͺ π
β (π¦ β (π β {β
}) β
((πβπ¦) β π¦ β (π¦ β© ran π) β β
))) |
63 | 62 | a2d 29 |
. . . . . . . . . . . . . 14
β’ (π:(π β {β
})βΆβͺ π
β ((π¦ β (π β {β
}) β
(πβπ¦) β π¦) β (π¦ β (π β {β
}) β (π¦ β© ran π) β β
))) |
64 | 56, 63 | syl7 74 |
. . . . . . . . . . . . 13
β’ (π:(π β {β
})βΆβͺ π
β ((π¦ β (π β {β
}) β
(πβπ¦) β π¦) β ((π¦ β π β§ π₯ β π¦) β (π¦ β© ran π) β β
))) |
65 | 64 | exp4a 433 |
. . . . . . . . . . . 12
β’ (π:(π β {β
})βΆβͺ π
β ((π¦ β (π β {β
}) β
(πβπ¦) β π¦) β (π¦ β π β (π₯ β π¦ β (π¦ β© ran π) β β
)))) |
66 | 65 | ralimdv2 3157 |
. . . . . . . . . . 11
β’ (π:(π β {β
})βΆβͺ π
β (βπ¦ β
(π β {β
})(πβπ¦) β π¦ β βπ¦ β π (π₯ β π¦ β (π¦ β© ran π) β β
))) |
67 | 66 | imp 408 |
. . . . . . . . . 10
β’ ((π:(π β {β
})βΆβͺ π
β§ βπ¦ β
(π β {β
})(πβπ¦) β π¦) β βπ¦ β π (π₯ β π¦ β (π¦ β© ran π) β β
)) |
68 | 67 | ad2antlr 726 |
. . . . . . . . 9
β’ ((((π β TopBases β§ π βΌ Ο) β§ (π:(π β {β
})βΆβͺ π
β§ βπ¦ β
(π β {β
})(πβπ¦) β π¦)) β§ π₯ β βͺ π) β βπ¦ β π (π₯ β π¦ β (π¦ β© ran π) β β
)) |
69 | | eqidd 2734 |
. . . . . . . . . 10
β’ ((((π β TopBases β§ π βΌ Ο) β§ (π:(π β {β
})βΆβͺ π
β§ βπ¦ β
(π β {β
})(πβπ¦) β π¦)) β§ π₯ β βͺ π) β (topGenβπ) = (topGenβπ)) |
70 | 51 | a1i 11 |
. . . . . . . . . 10
β’ ((((π β TopBases β§ π βΌ Ο) β§ (π:(π β {β
})βΆβͺ π
β§ βπ¦ β
(π β {β
})(πβπ¦) β π¦)) β§ π₯ β βͺ π) β βͺ π =
βͺ (topGenβπ)) |
71 | | simplll 774 |
. . . . . . . . . 10
β’ ((((π β TopBases β§ π βΌ Ο) β§ (π:(π β {β
})βΆβͺ π
β§ βπ¦ β
(π β {β
})(πβπ¦) β π¦)) β§ π₯ β βͺ π) β π β TopBases) |
72 | 27 | adantr 482 |
. . . . . . . . . 10
β’ ((((π β TopBases β§ π βΌ Ο) β§ (π:(π β {β
})βΆβͺ π
β§ βπ¦ β
(π β {β
})(πβπ¦) β π¦)) β§ π₯ β βͺ π) β ran π β βͺ π) |
73 | | simpr 486 |
. . . . . . . . . 10
β’ ((((π β TopBases β§ π βΌ Ο) β§ (π:(π β {β
})βΆβͺ π
β§ βπ¦ β
(π β {β
})(πβπ¦) β π¦)) β§ π₯ β βͺ π) β π₯ β βͺ π) |
74 | 69, 70, 71, 72, 73 | elcls3 22450 |
. . . . . . . . 9
β’ ((((π β TopBases β§ π βΌ Ο) β§ (π:(π β {β
})βΆβͺ π
β§ βπ¦ β
(π β {β
})(πβπ¦) β π¦)) β§ π₯ β βͺ π) β (π₯ β ((clsβ(topGenβπ))βran π) β βπ¦ β π (π₯ β π¦ β (π¦ β© ran π) β β
))) |
75 | 68, 74 | mpbird 257 |
. . . . . . . 8
β’ ((((π β TopBases β§ π βΌ Ο) β§ (π:(π β {β
})βΆβͺ π
β§ βπ¦ β
(π β {β
})(πβπ¦) β π¦)) β§ π₯ β βͺ π) β π₯ β ((clsβ(topGenβπ))βran π)) |
76 | 53, 75 | eqelssd 3966 |
. . . . . . 7
β’ (((π β TopBases β§ π βΌ Ο) β§ (π:(π β {β
})βΆβͺ π
β§ βπ¦ β
(π β {β
})(πβπ¦) β π¦)) β ((clsβ(topGenβπ))βran π) = βͺ π) |
77 | | breq1 5109 |
. . . . . . . . 9
β’ (π₯ = ran π β (π₯ βΌ Ο β ran π βΌ
Ο)) |
78 | | fveqeq2 6852 |
. . . . . . . . 9
β’ (π₯ = ran π β (((clsβ(topGenβπ))βπ₯) = βͺ π β
((clsβ(topGenβπ))βran π) = βͺ π)) |
79 | 77, 78 | anbi12d 632 |
. . . . . . . 8
β’ (π₯ = ran π β ((π₯ βΌ Ο β§
((clsβ(topGenβπ))βπ₯) = βͺ π) β (ran π βΌ Ο β§
((clsβ(topGenβπ))βran π) = βͺ π))) |
80 | 79 | rspcev 3580 |
. . . . . . 7
β’ ((ran
π β π« βͺ π
β§ (ran π βΌ
Ο β§ ((clsβ(topGenβπ))βran π) = βͺ π)) β βπ₯ β π« βͺ π(π₯ βΌ Ο β§
((clsβ(topGenβπ))βπ₯) = βͺ π)) |
81 | 31, 46, 76, 80 | syl12anc 836 |
. . . . . 6
β’ (((π β TopBases β§ π βΌ Ο) β§ (π:(π β {β
})βΆβͺ π
β§ βπ¦ β
(π β {β
})(πβπ¦) β π¦)) β βπ₯ β π« βͺ π(π₯ βΌ Ο β§
((clsβ(topGenβπ))βπ₯) = βͺ π)) |
82 | 25, 81 | exlimddv 1939 |
. . . . 5
β’ ((π β TopBases β§ π βΌ Ο) β
βπ₯ β π«
βͺ π(π₯ βΌ Ο β§
((clsβ(topGenβπ))βπ₯) = βͺ π)) |
83 | | unieq 4877 |
. . . . . . . 8
β’
((topGenβπ) =
π½ β βͺ (topGenβπ) = βͺ π½) |
84 | | 2ndcsep.1 |
. . . . . . . 8
β’ π = βͺ
π½ |
85 | 83, 51, 84 | 3eqtr4g 2798 |
. . . . . . 7
β’
((topGenβπ) =
π½ β βͺ π =
π) |
86 | 85 | pweqd 4578 |
. . . . . 6
β’
((topGenβπ) =
π½ β π« βͺ π =
π« π) |
87 | | fveq2 6843 |
. . . . . . . . 9
β’
((topGenβπ) =
π½ β
(clsβ(topGenβπ)) = (clsβπ½)) |
88 | 87 | fveq1d 6845 |
. . . . . . . 8
β’
((topGenβπ) =
π½ β
((clsβ(topGenβπ))βπ₯) = ((clsβπ½)βπ₯)) |
89 | 88, 85 | eqeq12d 2749 |
. . . . . . 7
β’
((topGenβπ) =
π½ β
(((clsβ(topGenβπ))βπ₯) = βͺ π β ((clsβπ½)βπ₯) = π)) |
90 | 89 | anbi2d 630 |
. . . . . 6
β’
((topGenβπ) =
π½ β ((π₯ βΌ Ο β§
((clsβ(topGenβπ))βπ₯) = βͺ π) β (π₯ βΌ Ο β§ ((clsβπ½)βπ₯) = π))) |
91 | 86, 90 | rexeqbidv 3319 |
. . . . 5
β’
((topGenβπ) =
π½ β (βπ₯ β π« βͺ π(π₯ βΌ Ο β§
((clsβ(topGenβπ))βπ₯) = βͺ π) β βπ₯ β π« π(π₯ βΌ Ο β§ ((clsβπ½)βπ₯) = π))) |
92 | 82, 91 | syl5ibcom 244 |
. . . 4
β’ ((π β TopBases β§ π βΌ Ο) β
((topGenβπ) = π½ β βπ₯ β π« π(π₯ βΌ Ο β§ ((clsβπ½)βπ₯) = π))) |
93 | 92 | impr 456 |
. . 3
β’ ((π β TopBases β§ (π βΌ Ο β§
(topGenβπ) = π½)) β βπ₯ β π« π(π₯ βΌ Ο β§ ((clsβπ½)βπ₯) = π)) |
94 | 93 | rexlimiva 3141 |
. 2
β’
(βπ β
TopBases (π βΌ Ο
β§ (topGenβπ) =
π½) β βπ₯ β π« π(π₯ βΌ Ο β§ ((clsβπ½)βπ₯) = π)) |
95 | 1, 94 | sylbi 216 |
1
β’ (π½ β 2ndΟ
β βπ₯ β
π« π(π₯ βΌ Ο β§
((clsβπ½)βπ₯) = π)) |