Step | Hyp | Ref
| Expression |
1 | | simpr 486 |
. . 3
β’ ((π΅ β TopBases β§ π½ β 2ndΟ)
β π½ β
2ndΟ) |
2 | | is2ndc 22813 |
. . 3
β’ (π½ β 2ndΟ
β βπ β
TopBases (π βΌ Ο
β§ (topGenβπ) =
π½)) |
3 | 1, 2 | sylib 217 |
. 2
β’ ((π΅ β TopBases β§ π½ β 2ndΟ)
β βπ β
TopBases (π βΌ Ο
β§ (topGenβπ) =
π½)) |
4 | | vex 3452 |
. . . . . . 7
β’ π β V |
5 | 4, 4 | xpex 7692 |
. . . . . 6
β’ (π Γ π) β V |
6 | | 3simpa 1149 |
. . . . . . . 8
β’ ((π’ β π β§ π£ β π β§ βπ€ β π΅ (π’ β π€ β§ π€ β π£)) β (π’ β π β§ π£ β π)) |
7 | 6 | ssopab2i 5512 |
. . . . . . 7
β’
{β¨π’, π£β© β£ (π’ β π β§ π£ β π β§ βπ€ β π΅ (π’ β π€ β§ π€ β π£))} β {β¨π’, π£β© β£ (π’ β π β§ π£ β π)} |
8 | | 2ndcctbss.2 |
. . . . . . 7
β’ π = {β¨π’, π£β© β£ (π’ β π β§ π£ β π β§ βπ€ β π΅ (π’ β π€ β§ π€ β π£))} |
9 | | df-xp 5644 |
. . . . . . 7
β’ (π Γ π) = {β¨π’, π£β© β£ (π’ β π β§ π£ β π)} |
10 | 7, 8, 9 | 3sstr4i 3992 |
. . . . . 6
β’ π β (π Γ π) |
11 | | ssdomg 8947 |
. . . . . 6
β’ ((π Γ π) β V β (π β (π Γ π) β π βΌ (π Γ π))) |
12 | 5, 10, 11 | mp2 9 |
. . . . 5
β’ π βΌ (π Γ π) |
13 | 4 | xpdom1 9022 |
. . . . . . . . 9
β’ (π βΌ Ο β (π Γ π) βΌ (Ο Γ π)) |
14 | | omex 9586 |
. . . . . . . . . 10
β’ Ο
β V |
15 | 14 | xpdom2 9018 |
. . . . . . . . 9
β’ (π βΌ Ο β (Ο
Γ π) βΌ (Ο
Γ Ο)) |
16 | | domtr 8954 |
. . . . . . . . 9
β’ (((π Γ π) βΌ (Ο Γ π) β§ (Ο Γ π) βΌ (Ο Γ Ο)) β
(π Γ π) βΌ (Ο Γ
Ο)) |
17 | 13, 15, 16 | syl2anc 585 |
. . . . . . . 8
β’ (π βΌ Ο β (π Γ π) βΌ (Ο Γ
Ο)) |
18 | | xpomen 9958 |
. . . . . . . 8
β’ (Ο
Γ Ο) β Ο |
19 | | domentr 8960 |
. . . . . . . 8
β’ (((π Γ π) βΌ (Ο Γ Ο) β§
(Ο Γ Ο) β Ο) β (π Γ π) βΌ Ο) |
20 | 17, 18, 19 | sylancl 587 |
. . . . . . 7
β’ (π βΌ Ο β (π Γ π) βΌ Ο) |
21 | 20 | adantr 482 |
. . . . . 6
β’ ((π βΌ Ο β§
(topGenβπ) = π½) β (π Γ π) βΌ Ο) |
22 | 21 | ad2antll 728 |
. . . . 5
β’ (((π΅ β TopBases β§ π½ β 2ndΟ)
β§ (π β TopBases
β§ (π βΌ Ο
β§ (topGenβπ) =
π½))) β (π Γ π) βΌ Ο) |
23 | | domtr 8954 |
. . . . 5
β’ ((π βΌ (π Γ π) β§ (π Γ π) βΌ Ο) β π βΌ Ο) |
24 | 12, 22, 23 | sylancr 588 |
. . . 4
β’ (((π΅ β TopBases β§ π½ β 2ndΟ)
β§ (π β TopBases
β§ (π βΌ Ο
β§ (topGenβπ) =
π½))) β π βΌ
Ο) |
25 | 8 | relopabiv 5781 |
. . . . . . . . 9
β’ Rel π |
26 | | simpr 486 |
. . . . . . . . 9
β’ ((((π΅ β TopBases β§ π½ β 2ndΟ)
β§ (π β TopBases
β§ (π βΌ Ο
β§ (topGenβπ) =
π½))) β§ π₯ β π) β π₯ β π) |
27 | | 1st2nd 7976 |
. . . . . . . . 9
β’ ((Rel
π β§ π₯ β π) β π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) |
28 | 25, 26, 27 | sylancr 588 |
. . . . . . . 8
β’ ((((π΅ β TopBases β§ π½ β 2ndΟ)
β§ (π β TopBases
β§ (π βΌ Ο
β§ (topGenβπ) =
π½))) β§ π₯ β π) β π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) |
29 | 28, 26 | eqeltrrd 2839 |
. . . . . . 7
β’ ((((π΅ β TopBases β§ π½ β 2ndΟ)
β§ (π β TopBases
β§ (π βΌ Ο
β§ (topGenβπ) =
π½))) β§ π₯ β π) β β¨(1st βπ₯), (2nd βπ₯)β© β π) |
30 | | df-br 5111 |
. . . . . . . . 9
β’
((1st βπ₯)π(2nd βπ₯) β β¨(1st βπ₯), (2nd βπ₯)β© β π) |
31 | | fvex 6860 |
. . . . . . . . . 10
β’
(1st βπ₯) β V |
32 | | fvex 6860 |
. . . . . . . . . 10
β’
(2nd βπ₯) β V |
33 | | simpl 484 |
. . . . . . . . . . . 12
β’ ((π’ = (1st βπ₯) β§ π£ = (2nd βπ₯)) β π’ = (1st βπ₯)) |
34 | 33 | eleq1d 2823 |
. . . . . . . . . . 11
β’ ((π’ = (1st βπ₯) β§ π£ = (2nd βπ₯)) β (π’ β π β (1st βπ₯) β π)) |
35 | | simpr 486 |
. . . . . . . . . . . 12
β’ ((π’ = (1st βπ₯) β§ π£ = (2nd βπ₯)) β π£ = (2nd βπ₯)) |
36 | 35 | eleq1d 2823 |
. . . . . . . . . . 11
β’ ((π’ = (1st βπ₯) β§ π£ = (2nd βπ₯)) β (π£ β π β (2nd βπ₯) β π)) |
37 | | sseq1 3974 |
. . . . . . . . . . . . 13
β’ (π’ = (1st βπ₯) β (π’ β π€ β (1st βπ₯) β π€)) |
38 | | sseq2 3975 |
. . . . . . . . . . . . 13
β’ (π£ = (2nd βπ₯) β (π€ β π£ β π€ β (2nd βπ₯))) |
39 | 37, 38 | bi2anan9 638 |
. . . . . . . . . . . 12
β’ ((π’ = (1st βπ₯) β§ π£ = (2nd βπ₯)) β ((π’ β π€ β§ π€ β π£) β ((1st βπ₯) β π€ β§ π€ β (2nd βπ₯)))) |
40 | 39 | rexbidv 3176 |
. . . . . . . . . . 11
β’ ((π’ = (1st βπ₯) β§ π£ = (2nd βπ₯)) β (βπ€ β π΅ (π’ β π€ β§ π€ β π£) β βπ€ β π΅ ((1st βπ₯) β π€ β§ π€ β (2nd βπ₯)))) |
41 | 34, 36, 40 | 3anbi123d 1437 |
. . . . . . . . . 10
β’ ((π’ = (1st βπ₯) β§ π£ = (2nd βπ₯)) β ((π’ β π β§ π£ β π β§ βπ€ β π΅ (π’ β π€ β§ π€ β π£)) β ((1st βπ₯) β π β§ (2nd βπ₯) β π β§ βπ€ β π΅ ((1st βπ₯) β π€ β§ π€ β (2nd βπ₯))))) |
42 | 31, 32, 41, 8 | braba 5499 |
. . . . . . . . 9
β’
((1st βπ₯)π(2nd βπ₯) β ((1st βπ₯) β π β§ (2nd βπ₯) β π β§ βπ€ β π΅ ((1st βπ₯) β π€ β§ π€ β (2nd βπ₯)))) |
43 | 30, 42 | bitr3i 277 |
. . . . . . . 8
β’
(β¨(1st βπ₯), (2nd βπ₯)β© β π β ((1st βπ₯) β π β§ (2nd βπ₯) β π β§ βπ€ β π΅ ((1st βπ₯) β π€ β§ π€ β (2nd βπ₯)))) |
44 | 43 | simp3bi 1148 |
. . . . . . 7
β’
(β¨(1st βπ₯), (2nd βπ₯)β© β π β βπ€ β π΅ ((1st βπ₯) β π€ β§ π€ β (2nd βπ₯))) |
45 | 29, 44 | syl 17 |
. . . . . 6
β’ ((((π΅ β TopBases β§ π½ β 2ndΟ)
β§ (π β TopBases
β§ (π βΌ Ο
β§ (topGenβπ) =
π½))) β§ π₯ β π) β βπ€ β π΅ ((1st βπ₯) β π€ β§ π€ β (2nd βπ₯))) |
46 | | fvi 6922 |
. . . . . . . 8
β’ (π΅ β TopBases β ( I
βπ΅) = π΅) |
47 | 46 | ad3antrrr 729 |
. . . . . . 7
β’ ((((π΅ β TopBases β§ π½ β 2ndΟ)
β§ (π β TopBases
β§ (π βΌ Ο
β§ (topGenβπ) =
π½))) β§ π₯ β π) β ( I βπ΅) = π΅) |
48 | 47 | rexeqdv 3317 |
. . . . . 6
β’ ((((π΅ β TopBases β§ π½ β 2ndΟ)
β§ (π β TopBases
β§ (π βΌ Ο
β§ (topGenβπ) =
π½))) β§ π₯ β π) β (βπ€ β ( I βπ΅)((1st βπ₯) β π€ β§ π€ β (2nd βπ₯)) β βπ€ β π΅ ((1st βπ₯) β π€ β§ π€ β (2nd βπ₯)))) |
49 | 45, 48 | mpbird 257 |
. . . . 5
β’ ((((π΅ β TopBases β§ π½ β 2ndΟ)
β§ (π β TopBases
β§ (π βΌ Ο
β§ (topGenβπ) =
π½))) β§ π₯ β π) β βπ€ β ( I βπ΅)((1st βπ₯) β π€ β§ π€ β (2nd βπ₯))) |
50 | 49 | ralrimiva 3144 |
. . . 4
β’ (((π΅ β TopBases β§ π½ β 2ndΟ)
β§ (π β TopBases
β§ (π βΌ Ο
β§ (topGenβπ) =
π½))) β βπ₯ β π βπ€ β ( I βπ΅)((1st βπ₯) β π€ β§ π€ β (2nd βπ₯))) |
51 | | fvex 6860 |
. . . . 5
β’ ( I
βπ΅) β
V |
52 | | sseq2 3975 |
. . . . . 6
β’ (π€ = (πβπ₯) β ((1st βπ₯) β π€ β (1st βπ₯) β (πβπ₯))) |
53 | | sseq1 3974 |
. . . . . 6
β’ (π€ = (πβπ₯) β (π€ β (2nd βπ₯) β (πβπ₯) β (2nd βπ₯))) |
54 | 52, 53 | anbi12d 632 |
. . . . 5
β’ (π€ = (πβπ₯) β (((1st βπ₯) β π€ β§ π€ β (2nd βπ₯)) β ((1st
βπ₯) β (πβπ₯) β§ (πβπ₯) β (2nd βπ₯)))) |
55 | 51, 54 | axcc4dom 10384 |
. . . 4
β’ ((π βΌ Ο β§
βπ₯ β π βπ€ β ( I βπ΅)((1st βπ₯) β π€ β§ π€ β (2nd βπ₯))) β βπ(π:πβΆ( I βπ΅) β§ βπ₯ β π ((1st βπ₯) β (πβπ₯) β§ (πβπ₯) β (2nd βπ₯)))) |
56 | 24, 50, 55 | syl2anc 585 |
. . 3
β’ (((π΅ β TopBases β§ π½ β 2ndΟ)
β§ (π β TopBases
β§ (π βΌ Ο
β§ (topGenβπ) =
π½))) β βπ(π:πβΆ( I βπ΅) β§ βπ₯ β π ((1st βπ₯) β (πβπ₯) β§ (πβπ₯) β (2nd βπ₯)))) |
57 | 46 | ad2antrr 725 |
. . . . . . 7
β’ (((π΅ β TopBases β§ π½ β 2ndΟ)
β§ (π β TopBases
β§ (π βΌ Ο
β§ (topGenβπ) =
π½))) β ( I
βπ΅) = π΅) |
58 | 57 | feq3d 6660 |
. . . . . 6
β’ (((π΅ β TopBases β§ π½ β 2ndΟ)
β§ (π β TopBases
β§ (π βΌ Ο
β§ (topGenβπ) =
π½))) β (π:πβΆ( I βπ΅) β π:πβΆπ΅)) |
59 | 58 | anbi1d 631 |
. . . . 5
β’ (((π΅ β TopBases β§ π½ β 2ndΟ)
β§ (π β TopBases
β§ (π βΌ Ο
β§ (topGenβπ) =
π½))) β ((π:πβΆ( I βπ΅) β§ βπ₯ β π ((1st βπ₯) β (πβπ₯) β§ (πβπ₯) β (2nd βπ₯))) β (π:πβΆπ΅ β§ βπ₯ β π ((1st βπ₯) β (πβπ₯) β§ (πβπ₯) β (2nd βπ₯))))) |
60 | | 2ndctop 22814 |
. . . . . . . . . . . 12
β’ (π½ β 2ndΟ
β π½ β
Top) |
61 | 60 | adantl 483 |
. . . . . . . . . . 11
β’ ((π΅ β TopBases β§ π½ β 2ndΟ)
β π½ β
Top) |
62 | 61 | ad2antrr 725 |
. . . . . . . . . 10
β’ ((((π΅ β TopBases β§ π½ β 2ndΟ)
β§ (π β TopBases
β§ (π βΌ Ο
β§ (topGenβπ) =
π½))) β§ (π:πβΆπ΅ β§ βπ₯ β π ((1st βπ₯) β (πβπ₯) β§ (πβπ₯) β (2nd βπ₯)))) β π½ β Top) |
63 | | frn 6680 |
. . . . . . . . . . . 12
β’ (π:πβΆπ΅ β ran π β π΅) |
64 | 63 | ad2antrl 727 |
. . . . . . . . . . 11
β’ ((((π΅ β TopBases β§ π½ β 2ndΟ)
β§ (π β TopBases
β§ (π βΌ Ο
β§ (topGenβπ) =
π½))) β§ (π:πβΆπ΅ β§ βπ₯ β π ((1st βπ₯) β (πβπ₯) β§ (πβπ₯) β (2nd βπ₯)))) β ran π β π΅) |
65 | | bastg 22332 |
. . . . . . . . . . . . 13
β’ (π΅ β TopBases β π΅ β (topGenβπ΅)) |
66 | 65 | ad3antrrr 729 |
. . . . . . . . . . . 12
β’ ((((π΅ β TopBases β§ π½ β 2ndΟ)
β§ (π β TopBases
β§ (π βΌ Ο
β§ (topGenβπ) =
π½))) β§ (π:πβΆπ΅ β§ βπ₯ β π ((1st βπ₯) β (πβπ₯) β§ (πβπ₯) β (2nd βπ₯)))) β π΅ β (topGenβπ΅)) |
67 | | 2ndcctbss.1 |
. . . . . . . . . . . 12
β’ π½ = (topGenβπ΅) |
68 | 66, 67 | sseqtrrdi 4000 |
. . . . . . . . . . 11
β’ ((((π΅ β TopBases β§ π½ β 2ndΟ)
β§ (π β TopBases
β§ (π βΌ Ο
β§ (topGenβπ) =
π½))) β§ (π:πβΆπ΅ β§ βπ₯ β π ((1st βπ₯) β (πβπ₯) β§ (πβπ₯) β (2nd βπ₯)))) β π΅ β π½) |
69 | 64, 68 | sstrd 3959 |
. . . . . . . . . 10
β’ ((((π΅ β TopBases β§ π½ β 2ndΟ)
β§ (π β TopBases
β§ (π βΌ Ο
β§ (topGenβπ) =
π½))) β§ (π:πβΆπ΅ β§ βπ₯ β π ((1st βπ₯) β (πβπ₯) β§ (πβπ₯) β (2nd βπ₯)))) β ran π β π½) |
70 | | simprrl 780 |
. . . . . . . . . . . . . . 15
β’ ((((π΅ β TopBases β§ π½ β 2ndΟ)
β§ (π β TopBases
β§ (π βΌ Ο
β§ (topGenβπ) =
π½))) β§ ((π:πβΆπ΅ β§ βπ₯ β π ((1st βπ₯) β (πβπ₯) β§ (πβπ₯) β (2nd βπ₯))) β§ (π β π½ β§ π‘ β π))) β π β π½) |
71 | | simprr 772 |
. . . . . . . . . . . . . . . 16
β’ ((π β TopBases β§ (π βΌ Ο β§
(topGenβπ) = π½)) β (topGenβπ) = π½) |
72 | 71 | ad2antlr 726 |
. . . . . . . . . . . . . . 15
β’ ((((π΅ β TopBases β§ π½ β 2ndΟ)
β§ (π β TopBases
β§ (π βΌ Ο
β§ (topGenβπ) =
π½))) β§ ((π:πβΆπ΅ β§ βπ₯ β π ((1st βπ₯) β (πβπ₯) β§ (πβπ₯) β (2nd βπ₯))) β§ (π β π½ β§ π‘ β π))) β (topGenβπ) = π½) |
73 | 70, 72 | eleqtrrd 2841 |
. . . . . . . . . . . . . 14
β’ ((((π΅ β TopBases β§ π½ β 2ndΟ)
β§ (π β TopBases
β§ (π βΌ Ο
β§ (topGenβπ) =
π½))) β§ ((π:πβΆπ΅ β§ βπ₯ β π ((1st βπ₯) β (πβπ₯) β§ (πβπ₯) β (2nd βπ₯))) β§ (π β π½ β§ π‘ β π))) β π β (topGenβπ)) |
74 | | simprrr 781 |
. . . . . . . . . . . . . 14
β’ ((((π΅ β TopBases β§ π½ β 2ndΟ)
β§ (π β TopBases
β§ (π βΌ Ο
β§ (topGenβπ) =
π½))) β§ ((π:πβΆπ΅ β§ βπ₯ β π ((1st βπ₯) β (πβπ₯) β§ (πβπ₯) β (2nd βπ₯))) β§ (π β π½ β§ π‘ β π))) β π‘ β π) |
75 | | tg2 22331 |
. . . . . . . . . . . . . 14
β’ ((π β (topGenβπ) β§ π‘ β π) β βπ β π (π‘ β π β§ π β π)) |
76 | 73, 74, 75 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ ((((π΅ β TopBases β§ π½ β 2ndΟ)
β§ (π β TopBases
β§ (π βΌ Ο
β§ (topGenβπ) =
π½))) β§ ((π:πβΆπ΅ β§ βπ₯ β π ((1st βπ₯) β (πβπ₯) β§ (πβπ₯) β (2nd βπ₯))) β§ (π β π½ β§ π‘ β π))) β βπ β π (π‘ β π β§ π β π)) |
77 | | bastg 22332 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β TopBases β π β (topGenβπ)) |
78 | 77 | ad2antrl 727 |
. . . . . . . . . . . . . . . . . 18
β’ (((π΅ β TopBases β§ π½ β 2ndΟ)
β§ (π β TopBases
β§ (π βΌ Ο
β§ (topGenβπ) =
π½))) β π β (topGenβπ)) |
79 | 78 | ad2antrr 725 |
. . . . . . . . . . . . . . . . 17
β’
(((((π΅ β
TopBases β§ π½ β
2ndΟ) β§ (π β TopBases β§ (π βΌ Ο β§ (topGenβπ) = π½))) β§ ((π:πβΆπ΅ β§ βπ₯ β π ((1st βπ₯) β (πβπ₯) β§ (πβπ₯) β (2nd βπ₯))) β§ (π β π½ β§ π‘ β π))) β§ (π β π β§ (π‘ β π β§ π β π))) β π β (topGenβπ)) |
80 | 67 | eqeq2i 2750 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((topGenβπ) =
π½ β
(topGenβπ) =
(topGenβπ΅)) |
81 | 80 | biimpi 215 |
. . . . . . . . . . . . . . . . . . . 20
β’
((topGenβπ) =
π½ β
(topGenβπ) =
(topGenβπ΅)) |
82 | 81 | adantl 483 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π βΌ Ο β§
(topGenβπ) = π½) β (topGenβπ) = (topGenβπ΅)) |
83 | 82 | ad2antll 728 |
. . . . . . . . . . . . . . . . . 18
β’ (((π΅ β TopBases β§ π½ β 2ndΟ)
β§ (π β TopBases
β§ (π βΌ Ο
β§ (topGenβπ) =
π½))) β
(topGenβπ) =
(topGenβπ΅)) |
84 | 83 | ad2antrr 725 |
. . . . . . . . . . . . . . . . 17
β’
(((((π΅ β
TopBases β§ π½ β
2ndΟ) β§ (π β TopBases β§ (π βΌ Ο β§ (topGenβπ) = π½))) β§ ((π:πβΆπ΅ β§ βπ₯ β π ((1st βπ₯) β (πβπ₯) β§ (πβπ₯) β (2nd βπ₯))) β§ (π β π½ β§ π‘ β π))) β§ (π β π β§ (π‘ β π β§ π β π))) β (topGenβπ) = (topGenβπ΅)) |
85 | 79, 84 | sseqtrd 3989 |
. . . . . . . . . . . . . . . 16
β’
(((((π΅ β
TopBases β§ π½ β
2ndΟ) β§ (π β TopBases β§ (π βΌ Ο β§ (topGenβπ) = π½))) β§ ((π:πβΆπ΅ β§ βπ₯ β π ((1st βπ₯) β (πβπ₯) β§ (πβπ₯) β (2nd βπ₯))) β§ (π β π½ β§ π‘ β π))) β§ (π β π β§ (π‘ β π β§ π β π))) β π β (topGenβπ΅)) |
86 | | simprl 770 |
. . . . . . . . . . . . . . . 16
β’
(((((π΅ β
TopBases β§ π½ β
2ndΟ) β§ (π β TopBases β§ (π βΌ Ο β§ (topGenβπ) = π½))) β§ ((π:πβΆπ΅ β§ βπ₯ β π ((1st βπ₯) β (πβπ₯) β§ (πβπ₯) β (2nd βπ₯))) β§ (π β π½ β§ π‘ β π))) β§ (π β π β§ (π‘ β π β§ π β π))) β π β π) |
87 | 85, 86 | sseldd 3950 |
. . . . . . . . . . . . . . 15
β’
(((((π΅ β
TopBases β§ π½ β
2ndΟ) β§ (π β TopBases β§ (π βΌ Ο β§ (topGenβπ) = π½))) β§ ((π:πβΆπ΅ β§ βπ₯ β π ((1st βπ₯) β (πβπ₯) β§ (πβπ₯) β (2nd βπ₯))) β§ (π β π½ β§ π‘ β π))) β§ (π β π β§ (π‘ β π β§ π β π))) β π β (topGenβπ΅)) |
88 | | simprrl 780 |
. . . . . . . . . . . . . . 15
β’
(((((π΅ β
TopBases β§ π½ β
2ndΟ) β§ (π β TopBases β§ (π βΌ Ο β§ (topGenβπ) = π½))) β§ ((π:πβΆπ΅ β§ βπ₯ β π ((1st βπ₯) β (πβπ₯) β§ (πβπ₯) β (2nd βπ₯))) β§ (π β π½ β§ π‘ β π))) β§ (π β π β§ (π‘ β π β§ π β π))) β π‘ β π) |
89 | | tg2 22331 |
. . . . . . . . . . . . . . 15
β’ ((π β (topGenβπ΅) β§ π‘ β π) β βπ β π΅ (π‘ β π β§ π β π)) |
90 | 87, 88, 89 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’
(((((π΅ β
TopBases β§ π½ β
2ndΟ) β§ (π β TopBases β§ (π βΌ Ο β§ (topGenβπ) = π½))) β§ ((π:πβΆπ΅ β§ βπ₯ β π ((1st βπ₯) β (πβπ₯) β§ (πβπ₯) β (2nd βπ₯))) β§ (π β π½ β§ π‘ β π))) β§ (π β π β§ (π‘ β π β§ π β π))) β βπ β π΅ (π‘ β π β§ π β π)) |
91 | 65 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π΅ β TopBases β§ π½ β 2ndΟ)
β§ (π β TopBases
β§ (π βΌ Ο
β§ (topGenβπ) =
π½))) β§ ((π:πβΆπ΅ β§ βπ₯ β π ((1st βπ₯) β (πβπ₯) β§ (πβπ₯) β (2nd βπ₯))) β§ (π β π½ β§ π‘ β π))) β π΅ β (topGenβπ΅)) |
92 | 91 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . 18
β’
((((((π΅ β
TopBases β§ π½ β
2ndΟ) β§ (π β TopBases β§ (π βΌ Ο β§ (topGenβπ) = π½))) β§ ((π:πβΆπ΅ β§ βπ₯ β π ((1st βπ₯) β (πβπ₯) β§ (πβπ₯) β (2nd βπ₯))) β§ (π β π½ β§ π‘ β π))) β§ (π β π β§ (π‘ β π β§ π β π))) β§ (π β π΅ β§ (π‘ β π β§ π β π))) β π΅ β (topGenβπ΅)) |
93 | 72 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . 19
β’
((((((π΅ β
TopBases β§ π½ β
2ndΟ) β§ (π β TopBases β§ (π βΌ Ο β§ (topGenβπ) = π½))) β§ ((π:πβΆπ΅ β§ βπ₯ β π ((1st βπ₯) β (πβπ₯) β§ (πβπ₯) β (2nd βπ₯))) β§ (π β π½ β§ π‘ β π))) β§ (π β π β§ (π‘ β π β§ π β π))) β§ (π β π΅ β§ (π‘ β π β§ π β π))) β (topGenβπ) = π½) |
94 | 93, 67 | eqtr2di 2794 |
. . . . . . . . . . . . . . . . . 18
β’
((((((π΅ β
TopBases β§ π½ β
2ndΟ) β§ (π β TopBases β§ (π βΌ Ο β§ (topGenβπ) = π½))) β§ ((π:πβΆπ΅ β§ βπ₯ β π ((1st βπ₯) β (πβπ₯) β§ (πβπ₯) β (2nd βπ₯))) β§ (π β π½ β§ π‘ β π))) β§ (π β π β§ (π‘ β π β§ π β π))) β§ (π β π΅ β§ (π‘ β π β§ π β π))) β (topGenβπ΅) = (topGenβπ)) |
95 | 92, 94 | sseqtrd 3989 |
. . . . . . . . . . . . . . . . 17
β’
((((((π΅ β
TopBases β§ π½ β
2ndΟ) β§ (π β TopBases β§ (π βΌ Ο β§ (topGenβπ) = π½))) β§ ((π:πβΆπ΅ β§ βπ₯ β π ((1st βπ₯) β (πβπ₯) β§ (πβπ₯) β (2nd βπ₯))) β§ (π β π½ β§ π‘ β π))) β§ (π β π β§ (π‘ β π β§ π β π))) β§ (π β π΅ β§ (π‘ β π β§ π β π))) β π΅ β (topGenβπ)) |
96 | | simprl 770 |
. . . . . . . . . . . . . . . . 17
β’
((((((π΅ β
TopBases β§ π½ β
2ndΟ) β§ (π β TopBases β§ (π βΌ Ο β§ (topGenβπ) = π½))) β§ ((π:πβΆπ΅ β§ βπ₯ β π ((1st βπ₯) β (πβπ₯) β§ (πβπ₯) β (2nd βπ₯))) β§ (π β π½ β§ π‘ β π))) β§ (π β π β§ (π‘ β π β§ π β π))) β§ (π β π΅ β§ (π‘ β π β§ π β π))) β π β π΅) |
97 | 95, 96 | sseldd 3950 |
. . . . . . . . . . . . . . . 16
β’
((((((π΅ β
TopBases β§ π½ β
2ndΟ) β§ (π β TopBases β§ (π βΌ Ο β§ (topGenβπ) = π½))) β§ ((π:πβΆπ΅ β§ βπ₯ β π ((1st βπ₯) β (πβπ₯) β§ (πβπ₯) β (2nd βπ₯))) β§ (π β π½ β§ π‘ β π))) β§ (π β π β§ (π‘ β π β§ π β π))) β§ (π β π΅ β§ (π‘ β π β§ π β π))) β π β (topGenβπ)) |
98 | | simprrl 780 |
. . . . . . . . . . . . . . . 16
β’
((((((π΅ β
TopBases β§ π½ β
2ndΟ) β§ (π β TopBases β§ (π βΌ Ο β§ (topGenβπ) = π½))) β§ ((π:πβΆπ΅ β§ βπ₯ β π ((1st βπ₯) β (πβπ₯) β§ (πβπ₯) β (2nd βπ₯))) β§ (π β π½ β§ π‘ β π))) β§ (π β π β§ (π‘ β π β§ π β π))) β§ (π β π΅ β§ (π‘ β π β§ π β π))) β π‘ β π) |
99 | | tg2 22331 |
. . . . . . . . . . . . . . . 16
β’ ((π β (topGenβπ) β§ π‘ β π) β βπ β π (π‘ β π β§ π β π)) |
100 | 97, 98, 99 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’
((((((π΅ β
TopBases β§ π½ β
2ndΟ) β§ (π β TopBases β§ (π βΌ Ο β§ (topGenβπ) = π½))) β§ ((π:πβΆπ΅ β§ βπ₯ β π ((1st βπ₯) β (πβπ₯) β§ (πβπ₯) β (2nd βπ₯))) β§ (π β π½ β§ π‘ β π))) β§ (π β π β§ (π‘ β π β§ π β π))) β§ (π β π΅ β§ (π‘ β π β§ π β π))) β βπ β π (π‘ β π β§ π β π)) |
101 | | ffn 6673 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π:πβΆπ΅ β π Fn π) |
102 | 101 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π:πβΆπ΅ β§ βπ₯ β π ((1st βπ₯) β (πβπ₯) β§ (πβπ₯) β (2nd βπ₯))) β§ (π β π½ β§ π‘ β π)) β π Fn π) |
103 | 102 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π΅ β
TopBases β§ π½ β
2ndΟ) β§ (π β TopBases β§ (π βΌ Ο β§ (topGenβπ) = π½))) β§ ((π:πβΆπ΅ β§ βπ₯ β π ((1st βπ₯) β (πβπ₯) β§ (πβπ₯) β (2nd βπ₯))) β§ (π β π½ β§ π‘ β π))) β§ (π β π β§ (π‘ β π β§ π β π))) β π Fn π) |
104 | 103 | ad2antrr 725 |
. . . . . . . . . . . . . . . . 17
β’
(((((((π΅ β
TopBases β§ π½ β
2ndΟ) β§ (π β TopBases β§ (π βΌ Ο β§ (topGenβπ) = π½))) β§ ((π:πβΆπ΅ β§ βπ₯ β π ((1st βπ₯) β (πβπ₯) β§ (πβπ₯) β (2nd βπ₯))) β§ (π β π½ β§ π‘ β π))) β§ (π β π β§ (π‘ β π β§ π β π))) β§ (π β π΅ β§ (π‘ β π β§ π β π))) β§ (π β π β§ (π‘ β π β§ π β π))) β π Fn π) |
105 | | simprl 770 |
. . . . . . . . . . . . . . . . . 18
β’
(((((((π΅ β
TopBases β§ π½ β
2ndΟ) β§ (π β TopBases β§ (π βΌ Ο β§ (topGenβπ) = π½))) β§ ((π:πβΆπ΅ β§ βπ₯ β π ((1st βπ₯) β (πβπ₯) β§ (πβπ₯) β (2nd βπ₯))) β§ (π β π½ β§ π‘ β π))) β§ (π β π β§ (π‘ β π β§ π β π))) β§ (π β π΅ β§ (π‘ β π β§ π β π))) β§ (π β π β§ (π‘ β π β§ π β π))) β π β π) |
106 | 86 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . 18
β’
(((((((π΅ β
TopBases β§ π½ β
2ndΟ) β§ (π β TopBases β§ (π βΌ Ο β§ (topGenβπ) = π½))) β§ ((π:πβΆπ΅ β§ βπ₯ β π ((1st βπ₯) β (πβπ₯) β§ (πβπ₯) β (2nd βπ₯))) β§ (π β π½ β§ π‘ β π))) β§ (π β π β§ (π‘ β π β§ π β π))) β§ (π β π΅ β§ (π‘ β π β§ π β π))) β§ (π β π β§ (π‘ β π β§ π β π))) β π β π) |
107 | | simplrl 776 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((((π΅ β
TopBases β§ π½ β
2ndΟ) β§ (π β TopBases β§ (π βΌ Ο β§ (topGenβπ) = π½))) β§ ((π:πβΆπ΅ β§ βπ₯ β π ((1st βπ₯) β (πβπ₯) β§ (πβπ₯) β (2nd βπ₯))) β§ (π β π½ β§ π‘ β π))) β§ (π β π β§ (π‘ β π β§ π β π))) β§ (π β π΅ β§ (π‘ β π β§ π β π))) β§ (π β π β§ (π‘ β π β§ π β π))) β π β π΅) |
108 | | simprrr 781 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((((π΅ β
TopBases β§ π½ β
2ndΟ) β§ (π β TopBases β§ (π βΌ Ο β§ (topGenβπ) = π½))) β§ ((π:πβΆπ΅ β§ βπ₯ β π ((1st βπ₯) β (πβπ₯) β§ (πβπ₯) β (2nd βπ₯))) β§ (π β π½ β§ π‘ β π))) β§ (π β π β§ (π‘ β π β§ π β π))) β§ (π β π΅ β§ (π‘ β π β§ π β π))) β§ (π β π β§ (π‘ β π β§ π β π))) β π β π) |
109 | | simprr 772 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β π΅ β§ (π‘ β π β§ π β π)) β π β π) |
110 | 109 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((((π΅ β
TopBases β§ π½ β
2ndΟ) β§ (π β TopBases β§ (π βΌ Ο β§ (topGenβπ) = π½))) β§ ((π:πβΆπ΅ β§ βπ₯ β π ((1st βπ₯) β (πβπ₯) β§ (πβπ₯) β (2nd βπ₯))) β§ (π β π½ β§ π‘ β π))) β§ (π β π β§ (π‘ β π β§ π β π))) β§ (π β π΅ β§ (π‘ β π β§ π β π))) β§ (π β π β§ (π‘ β π β§ π β π))) β π β π) |
111 | | sseq2 3975 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π€ = π β (π β π€ β π β π)) |
112 | | sseq1 3974 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π€ = π β (π€ β π β π β π)) |
113 | 111, 112 | anbi12d 632 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π€ = π β ((π β π€ β§ π€ β π) β (π β π β§ π β π))) |
114 | 113 | rspcev 3584 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β π΅ β§ (π β π β§ π β π)) β βπ€ β π΅ (π β π€ β§ π€ β π)) |
115 | 107, 108,
110, 114 | syl12anc 836 |
. . . . . . . . . . . . . . . . . 18
β’
(((((((π΅ β
TopBases β§ π½ β
2ndΟ) β§ (π β TopBases β§ (π βΌ Ο β§ (topGenβπ) = π½))) β§ ((π:πβΆπ΅ β§ βπ₯ β π ((1st βπ₯) β (πβπ₯) β§ (πβπ₯) β (2nd βπ₯))) β§ (π β π½ β§ π‘ β π))) β§ (π β π β§ (π‘ β π β§ π β π))) β§ (π β π΅ β§ (π‘ β π β§ π β π))) β§ (π β π β§ (π‘ β π β§ π β π))) β βπ€ β π΅ (π β π€ β§ π€ β π)) |
116 | | df-br 5111 |
. . . . . . . . . . . . . . . . . . 19
β’ (πππ β β¨π, πβ© β π) |
117 | | vex 3452 |
. . . . . . . . . . . . . . . . . . . 20
β’ π β V |
118 | | vex 3452 |
. . . . . . . . . . . . . . . . . . . 20
β’ π β V |
119 | | simpl 484 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π’ = π β§ π£ = π) β π’ = π) |
120 | 119 | eleq1d 2823 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π’ = π β§ π£ = π) β (π’ β π β π β π)) |
121 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π’ = π β§ π£ = π) β π£ = π) |
122 | 121 | eleq1d 2823 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π’ = π β§ π£ = π) β (π£ β π β π β π)) |
123 | | sseq1 3974 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π’ = π β (π’ β π€ β π β π€)) |
124 | | sseq2 3975 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π£ = π β (π€ β π£ β π€ β π)) |
125 | 123, 124 | bi2anan9 638 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π’ = π β§ π£ = π) β ((π’ β π€ β§ π€ β π£) β (π β π€ β§ π€ β π))) |
126 | 125 | rexbidv 3176 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π’ = π β§ π£ = π) β (βπ€ β π΅ (π’ β π€ β§ π€ β π£) β βπ€ β π΅ (π β π€ β§ π€ β π))) |
127 | 120, 122,
126 | 3anbi123d 1437 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π’ = π β§ π£ = π) β ((π’ β π β§ π£ β π β§ βπ€ β π΅ (π’ β π€ β§ π€ β π£)) β (π β π β§ π β π β§ βπ€ β π΅ (π β π€ β§ π€ β π)))) |
128 | 117, 118,
127, 8 | braba 5499 |
. . . . . . . . . . . . . . . . . . 19
β’ (πππ β (π β π β§ π β π β§ βπ€ β π΅ (π β π€ β§ π€ β π))) |
129 | 116, 128 | bitr3i 277 |
. . . . . . . . . . . . . . . . . 18
β’
(β¨π, πβ© β π β (π β π β§ π β π β§ βπ€ β π΅ (π β π€ β§ π€ β π))) |
130 | 105, 106,
115, 129 | syl3anbrc 1344 |
. . . . . . . . . . . . . . . . 17
β’
(((((((π΅ β
TopBases β§ π½ β
2ndΟ) β§ (π β TopBases β§ (π βΌ Ο β§ (topGenβπ) = π½))) β§ ((π:πβΆπ΅ β§ βπ₯ β π ((1st βπ₯) β (πβπ₯) β§ (πβπ₯) β (2nd βπ₯))) β§ (π β π½ β§ π‘ β π))) β§ (π β π β§ (π‘ β π β§ π β π))) β§ (π β π΅ β§ (π‘ β π β§ π β π))) β§ (π β π β§ (π‘ β π β§ π β π))) β β¨π, πβ© β π) |
131 | | fnfvelrn 7036 |
. . . . . . . . . . . . . . . . 17
β’ ((π Fn π β§ β¨π, πβ© β π) β (πββ¨π, πβ©) β ran π) |
132 | 104, 130,
131 | syl2anc 585 |
. . . . . . . . . . . . . . . 16
β’
(((((((π΅ β
TopBases β§ π½ β
2ndΟ) β§ (π β TopBases β§ (π βΌ Ο β§ (topGenβπ) = π½))) β§ ((π:πβΆπ΅ β§ βπ₯ β π ((1st βπ₯) β (πβπ₯) β§ (πβπ₯) β (2nd βπ₯))) β§ (π β π½ β§ π‘ β π))) β§ (π β π β§ (π‘ β π β§ π β π))) β§ (π β π΅ β§ (π‘ β π β§ π β π))) β§ (π β π β§ (π‘ β π β§ π β π))) β (πββ¨π, πβ©) β ran π) |
133 | | simprl 770 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β π β§ (π‘ β π β§ π β π)) β§ (π β π΅ β§ (π‘ β π β§ π β π))) β§ (π β π β§ (π‘ β π β§ π β π))) β π β π) |
134 | | simplll 774 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β π β§ (π‘ β π β§ π β π)) β§ (π β π΅ β§ (π‘ β π β§ π β π))) β§ (π β π β§ (π‘ β π β§ π β π))) β π β π) |
135 | | simplrl 776 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π β π β§ (π‘ β π β§ π β π)) β§ (π β π΅ β§ (π‘ β π β§ π β π))) β§ (π β π β§ (π‘ β π β§ π β π))) β π β π΅) |
136 | | simprrr 781 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π β π β§ (π‘ β π β§ π β π)) β§ (π β π΅ β§ (π‘ β π β§ π β π))) β§ (π β π β§ (π‘ β π β§ π β π))) β π β π) |
137 | 109 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π β π β§ (π‘ β π β§ π β π)) β§ (π β π΅ β§ (π‘ β π β§ π β π))) β§ (π β π β§ (π‘ β π β§ π β π))) β π β π) |
138 | 135, 136,
137, 114 | syl12anc 836 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β π β§ (π‘ β π β§ π β π)) β§ (π β π΅ β§ (π‘ β π β§ π β π))) β§ (π β π β§ (π‘ β π β§ π β π))) β βπ€ β π΅ (π β π€ β§ π€ β π)) |
139 | 133, 134,
138, 129 | syl3anbrc 1344 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β π β§ (π‘ β π β§ π β π)) β§ (π β π΅ β§ (π‘ β π β§ π β π))) β§ (π β π β§ (π‘ β π β§ π β π))) β β¨π, πβ© β π) |
140 | | fveq2 6847 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π₯ = β¨π, πβ© β (1st βπ₯) = (1st
ββ¨π, πβ©)) |
141 | | fveq2 6847 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π₯ = β¨π, πβ© β (πβπ₯) = (πββ¨π, πβ©)) |
142 | 140, 141 | sseq12d 3982 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π₯ = β¨π, πβ© β ((1st βπ₯) β (πβπ₯) β (1st ββ¨π, πβ©) β (πββ¨π, πβ©))) |
143 | | fveq2 6847 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π₯ = β¨π, πβ© β (2nd βπ₯) = (2nd
ββ¨π, πβ©)) |
144 | 141, 143 | sseq12d 3982 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π₯ = β¨π, πβ© β ((πβπ₯) β (2nd βπ₯) β (πββ¨π, πβ©) β (2nd
ββ¨π, πβ©))) |
145 | 142, 144 | anbi12d 632 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π₯ = β¨π, πβ© β (((1st βπ₯) β (πβπ₯) β§ (πβπ₯) β (2nd βπ₯)) β ((1st
ββ¨π, πβ©) β (πββ¨π, πβ©) β§ (πββ¨π, πβ©) β (2nd
ββ¨π, πβ©)))) |
146 | 145 | rspcv 3580 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(β¨π, πβ© β π β (βπ₯ β π ((1st βπ₯) β (πβπ₯) β§ (πβπ₯) β (2nd βπ₯)) β ((1st
ββ¨π, πβ©) β (πββ¨π, πβ©) β§ (πββ¨π, πβ©) β (2nd
ββ¨π, πβ©)))) |
147 | 139, 146 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β π β§ (π‘ β π β§ π β π)) β§ (π β π΅ β§ (π‘ β π β§ π β π))) β§ (π β π β§ (π‘ β π β§ π β π))) β (βπ₯ β π ((1st βπ₯) β (πβπ₯) β§ (πβπ₯) β (2nd βπ₯)) β ((1st
ββ¨π, πβ©) β (πββ¨π, πβ©) β§ (πββ¨π, πβ©) β (2nd
ββ¨π, πβ©)))) |
148 | 117, 118 | op1st 7934 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(1st ββ¨π, πβ©) = π |
149 | 148 | sseq1i 3977 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
((1st ββ¨π, πβ©) β (πββ¨π, πβ©) β π β (πββ¨π, πβ©)) |
150 | 117, 118 | op2nd 7935 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(2nd ββ¨π, πβ©) = π |
151 | 150 | sseq2i 3978 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((πββ¨π, πβ©) β (2nd
ββ¨π, πβ©) β (πββ¨π, πβ©) β π) |
152 | 149, 151 | anbi12i 628 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(((1st ββ¨π, πβ©) β (πββ¨π, πβ©) β§ (πββ¨π, πβ©) β (2nd
ββ¨π, πβ©)) β (π β (πββ¨π, πβ©) β§ (πββ¨π, πβ©) β π)) |
153 | | simprl 770 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
(((((π β π β§ (π‘ β π β§ π β π)) β§ (π β π΅ β§ (π‘ β π β§ π β π))) β§ (π β π β§ (π‘ β π β§ π β π))) β§ (π β (πββ¨π, πβ©) β§ (πββ¨π, πβ©) β π)) β π β (πββ¨π, πβ©)) |
154 | | simprl 770 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β π β§ (π‘ β π β§ π β π)) β π‘ β π) |
155 | 154 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
(((((π β π β§ (π‘ β π β§ π β π)) β§ (π β π΅ β§ (π‘ β π β§ π β π))) β§ (π β π β§ (π‘ β π β§ π β π))) β§ (π β (πββ¨π, πβ©) β§ (πββ¨π, πβ©) β π)) β π‘ β π) |
156 | 153, 155 | sseldd 3950 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(((((π β π β§ (π‘ β π β§ π β π)) β§ (π β π΅ β§ (π‘ β π β§ π β π))) β§ (π β π β§ (π‘ β π β§ π β π))) β§ (π β (πββ¨π, πβ©) β§ (πββ¨π, πβ©) β π)) β π‘ β (πββ¨π, πβ©)) |
157 | | simprr 772 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
(((((π β π β§ (π‘ β π β§ π β π)) β§ (π β π΅ β§ (π‘ β π β§ π β π))) β§ (π β π β§ (π‘ β π β§ π β π))) β§ (π β (πββ¨π, πβ©) β§ (πββ¨π, πβ©) β π)) β (πββ¨π, πβ©) β π) |
158 | | simplrr 777 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π β π β§ (π‘ β π β§ π β π)) β§ (π β π΅ β§ (π‘ β π β§ π β π))) β π β π) |
159 | 158 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
(((((π β π β§ (π‘ β π β§ π β π)) β§ (π β π΅ β§ (π‘ β π β§ π β π))) β§ (π β π β§ (π‘ β π β§ π β π))) β§ (π β (πββ¨π, πβ©) β§ (πββ¨π, πβ©) β π)) β π β π) |
160 | 157, 159 | sstrd 3959 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(((((π β π β§ (π‘ β π β§ π β π)) β§ (π β π΅ β§ (π‘ β π β§ π β π))) β§ (π β π β§ (π‘ β π β§ π β π))) β§ (π β (πββ¨π, πβ©) β§ (πββ¨π, πβ©) β π)) β (πββ¨π, πβ©) β π) |
161 | 156, 160 | jca 513 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(((((π β π β§ (π‘ β π β§ π β π)) β§ (π β π΅ β§ (π‘ β π β§ π β π))) β§ (π β π β§ (π‘ β π β§ π β π))) β§ (π β (πββ¨π, πβ©) β§ (πββ¨π, πβ©) β π)) β (π‘ β (πββ¨π, πβ©) β§ (πββ¨π, πβ©) β π)) |
162 | 161 | ex 414 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β π β§ (π‘ β π β§ π β π)) β§ (π β π΅ β§ (π‘ β π β§ π β π))) β§ (π β π β§ (π‘ β π β§ π β π))) β ((π β (πββ¨π, πβ©) β§ (πββ¨π, πβ©) β π) β (π‘ β (πββ¨π, πβ©) β§ (πββ¨π, πβ©) β π))) |
163 | 152, 162 | biimtrid 241 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β π β§ (π‘ β π β§ π β π)) β§ (π β π΅ β§ (π‘ β π β§ π β π))) β§ (π β π β§ (π‘ β π β§ π β π))) β (((1st
ββ¨π, πβ©) β (πββ¨π, πβ©) β§ (πββ¨π, πβ©) β (2nd
ββ¨π, πβ©)) β (π‘ β (πββ¨π, πβ©) β§ (πββ¨π, πβ©) β π))) |
164 | 147, 163 | syldc 48 |
. . . . . . . . . . . . . . . . . . . 20
β’
(βπ₯ β
π ((1st
βπ₯) β (πβπ₯) β§ (πβπ₯) β (2nd βπ₯)) β ((((π β π β§ (π‘ β π β§ π β π)) β§ (π β π΅ β§ (π‘ β π β§ π β π))) β§ (π β π β§ (π‘ β π β§ π β π))) β (π‘ β (πββ¨π, πβ©) β§ (πββ¨π, πβ©) β π))) |
165 | 164 | exp4c 434 |
. . . . . . . . . . . . . . . . . . 19
β’
(βπ₯ β
π ((1st
βπ₯) β (πβπ₯) β§ (πβπ₯) β (2nd βπ₯)) β ((π β π β§ (π‘ β π β§ π β π)) β ((π β π΅ β§ (π‘ β π β§ π β π)) β ((π β π β§ (π‘ β π β§ π β π)) β (π‘ β (πββ¨π, πβ©) β§ (πββ¨π, πβ©) β π))))) |
166 | 165 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . 18
β’ (((π:πβΆπ΅ β§ βπ₯ β π ((1st βπ₯) β (πβπ₯) β§ (πβπ₯) β (2nd βπ₯))) β§ (π β π½ β§ π‘ β π)) β ((π β π β§ (π‘ β π β§ π β π)) β ((π β π΅ β§ (π‘ β π β§ π β π)) β ((π β π β§ (π‘ β π β§ π β π)) β (π‘ β (πββ¨π, πβ©) β§ (πββ¨π, πβ©) β π))))) |
167 | 166 | adantl 483 |
. . . . . . . . . . . . . . . . 17
β’ ((((π΅ β TopBases β§ π½ β 2ndΟ)
β§ (π β TopBases
β§ (π βΌ Ο
β§ (topGenβπ) =
π½))) β§ ((π:πβΆπ΅ β§ βπ₯ β π ((1st βπ₯) β (πβπ₯) β§ (πβπ₯) β (2nd βπ₯))) β§ (π β π½ β§ π‘ β π))) β ((π β π β§ (π‘ β π β§ π β π)) β ((π β π΅ β§ (π‘ β π β§ π β π)) β ((π β π β§ (π‘ β π β§ π β π)) β (π‘ β (πββ¨π, πβ©) β§ (πββ¨π, πβ©) β π))))) |
168 | 167 | imp41 427 |
. . . . . . . . . . . . . . . 16
β’
(((((((π΅ β
TopBases β§ π½ β
2ndΟ) β§ (π β TopBases β§ (π βΌ Ο β§ (topGenβπ) = π½))) β§ ((π:πβΆπ΅ β§ βπ₯ β π ((1st βπ₯) β (πβπ₯) β§ (πβπ₯) β (2nd βπ₯))) β§ (π β π½ β§ π‘ β π))) β§ (π β π β§ (π‘ β π β§ π β π))) β§ (π β π΅ β§ (π‘ β π β§ π β π))) β§ (π β π β§ (π‘ β π β§ π β π))) β (π‘ β (πββ¨π, πβ©) β§ (πββ¨π, πβ©) β π)) |
169 | | eleq2 2827 |
. . . . . . . . . . . . . . . . . 18
β’ (π = (πββ¨π, πβ©) β (π‘ β π β π‘ β (πββ¨π, πβ©))) |
170 | | sseq1 3974 |
. . . . . . . . . . . . . . . . . 18
β’ (π = (πββ¨π, πβ©) β (π β π β (πββ¨π, πβ©) β π)) |
171 | 169, 170 | anbi12d 632 |
. . . . . . . . . . . . . . . . 17
β’ (π = (πββ¨π, πβ©) β ((π‘ β π β§ π β π) β (π‘ β (πββ¨π, πβ©) β§ (πββ¨π, πβ©) β π))) |
172 | 171 | rspcev 3584 |
. . . . . . . . . . . . . . . 16
β’ (((πββ¨π, πβ©) β ran π β§ (π‘ β (πββ¨π, πβ©) β§ (πββ¨π, πβ©) β π)) β βπ β ran π(π‘ β π β§ π β π)) |
173 | 132, 168,
172 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’
(((((((π΅ β
TopBases β§ π½ β
2ndΟ) β§ (π β TopBases β§ (π βΌ Ο β§ (topGenβπ) = π½))) β§ ((π:πβΆπ΅ β§ βπ₯ β π ((1st βπ₯) β (πβπ₯) β§ (πβπ₯) β (2nd βπ₯))) β§ (π β π½ β§ π‘ β π))) β§ (π β π β§ (π‘ β π β§ π β π))) β§ (π β π΅ β§ (π‘ β π β§ π β π))) β§ (π β π β§ (π‘ β π β§ π β π))) β βπ β ran π(π‘ β π β§ π β π)) |
174 | 100, 173 | rexlimddv 3159 |
. . . . . . . . . . . . . 14
β’
((((((π΅ β
TopBases β§ π½ β
2ndΟ) β§ (π β TopBases β§ (π βΌ Ο β§ (topGenβπ) = π½))) β§ ((π:πβΆπ΅ β§ βπ₯ β π ((1st βπ₯) β (πβπ₯) β§ (πβπ₯) β (2nd βπ₯))) β§ (π β π½ β§ π‘ β π))) β§ (π β π β§ (π‘ β π β§ π β π))) β§ (π β π΅ β§ (π‘ β π β§ π β π))) β βπ β ran π(π‘ β π β§ π β π)) |
175 | 90, 174 | rexlimddv 3159 |
. . . . . . . . . . . . 13
β’
(((((π΅ β
TopBases β§ π½ β
2ndΟ) β§ (π β TopBases β§ (π βΌ Ο β§ (topGenβπ) = π½))) β§ ((π:πβΆπ΅ β§ βπ₯ β π ((1st βπ₯) β (πβπ₯) β§ (πβπ₯) β (2nd βπ₯))) β§ (π β π½ β§ π‘ β π))) β§ (π β π β§ (π‘ β π β§ π β π))) β βπ β ran π(π‘ β π β§ π β π)) |
176 | 76, 175 | rexlimddv 3159 |
. . . . . . . . . . . 12
β’ ((((π΅ β TopBases β§ π½ β 2ndΟ)
β§ (π β TopBases
β§ (π βΌ Ο
β§ (topGenβπ) =
π½))) β§ ((π:πβΆπ΅ β§ βπ₯ β π ((1st βπ₯) β (πβπ₯) β§ (πβπ₯) β (2nd βπ₯))) β§ (π β π½ β§ π‘ β π))) β βπ β ran π(π‘ β π β§ π β π)) |
177 | 176 | expr 458 |
. . . . . . . . . . 11
β’ ((((π΅ β TopBases β§ π½ β 2ndΟ)
β§ (π β TopBases
β§ (π βΌ Ο
β§ (topGenβπ) =
π½))) β§ (π:πβΆπ΅ β§ βπ₯ β π ((1st βπ₯) β (πβπ₯) β§ (πβπ₯) β (2nd βπ₯)))) β ((π β π½ β§ π‘ β π) β βπ β ran π(π‘ β π β§ π β π))) |
178 | 177 | ralrimivv 3196 |
. . . . . . . . . 10
β’ ((((π΅ β TopBases β§ π½ β 2ndΟ)
β§ (π β TopBases
β§ (π βΌ Ο
β§ (topGenβπ) =
π½))) β§ (π:πβΆπ΅ β§ βπ₯ β π ((1st βπ₯) β (πβπ₯) β§ (πβπ₯) β (2nd βπ₯)))) β βπ β π½ βπ‘ β π βπ β ran π(π‘ β π β§ π β π)) |
179 | | basgen2 22355 |
. . . . . . . . . 10
β’ ((π½ β Top β§ ran π β π½ β§ βπ β π½ βπ‘ β π βπ β ran π(π‘ β π β§ π β π)) β (topGenβran π) = π½) |
180 | 62, 69, 178, 179 | syl3anc 1372 |
. . . . . . . . 9
β’ ((((π΅ β TopBases β§ π½ β 2ndΟ)
β§ (π β TopBases
β§ (π βΌ Ο
β§ (topGenβπ) =
π½))) β§ (π:πβΆπ΅ β§ βπ₯ β π ((1st βπ₯) β (πβπ₯) β§ (πβπ₯) β (2nd βπ₯)))) β (topGenβran
π) = π½) |
181 | 180, 62 | eqeltrd 2838 |
. . . . . . . 8
β’ ((((π΅ β TopBases β§ π½ β 2ndΟ)
β§ (π β TopBases
β§ (π βΌ Ο
β§ (topGenβπ) =
π½))) β§ (π:πβΆπ΅ β§ βπ₯ β π ((1st βπ₯) β (πβπ₯) β§ (πβπ₯) β (2nd βπ₯)))) β (topGenβran
π) β
Top) |
182 | | tgclb 22336 |
. . . . . . . 8
β’ (ran
π β TopBases β
(topGenβran π) β
Top) |
183 | 181, 182 | sylibr 233 |
. . . . . . 7
β’ ((((π΅ β TopBases β§ π½ β 2ndΟ)
β§ (π β TopBases
β§ (π βΌ Ο
β§ (topGenβπ) =
π½))) β§ (π:πβΆπ΅ β§ βπ₯ β π ((1st βπ₯) β (πβπ₯) β§ (πβπ₯) β (2nd βπ₯)))) β ran π β
TopBases) |
184 | | omelon 9589 |
. . . . . . . . . 10
β’ Ο
β On |
185 | 24 | adantr 482 |
. . . . . . . . . 10
β’ ((((π΅ β TopBases β§ π½ β 2ndΟ)
β§ (π β TopBases
β§ (π βΌ Ο
β§ (topGenβπ) =
π½))) β§ (π:πβΆπ΅ β§ βπ₯ β π ((1st βπ₯) β (πβπ₯) β§ (πβπ₯) β (2nd βπ₯)))) β π βΌ Ο) |
186 | | ondomen 9980 |
. . . . . . . . . 10
β’ ((Ο
β On β§ π βΌ
Ο) β π β
dom card) |
187 | 184, 185,
186 | sylancr 588 |
. . . . . . . . 9
β’ ((((π΅ β TopBases β§ π½ β 2ndΟ)
β§ (π β TopBases
β§ (π βΌ Ο
β§ (topGenβπ) =
π½))) β§ (π:πβΆπ΅ β§ βπ₯ β π ((1st βπ₯) β (πβπ₯) β§ (πβπ₯) β (2nd βπ₯)))) β π β dom card) |
188 | 101 | ad2antrl 727 |
. . . . . . . . . 10
β’ ((((π΅ β TopBases β§ π½ β 2ndΟ)
β§ (π β TopBases
β§ (π βΌ Ο
β§ (topGenβπ) =
π½))) β§ (π:πβΆπ΅ β§ βπ₯ β π ((1st βπ₯) β (πβπ₯) β§ (πβπ₯) β (2nd βπ₯)))) β π Fn π) |
189 | | dffn4 6767 |
. . . . . . . . . 10
β’ (π Fn π β π:πβontoβran π) |
190 | 188, 189 | sylib 217 |
. . . . . . . . 9
β’ ((((π΅ β TopBases β§ π½ β 2ndΟ)
β§ (π β TopBases
β§ (π βΌ Ο
β§ (topGenβπ) =
π½))) β§ (π:πβΆπ΅ β§ βπ₯ β π ((1st βπ₯) β (πβπ₯) β§ (πβπ₯) β (2nd βπ₯)))) β π:πβontoβran π) |
191 | | fodomnum 10000 |
. . . . . . . . 9
β’ (π β dom card β (π:πβontoβran π β ran π βΌ π)) |
192 | 187, 190,
191 | sylc 65 |
. . . . . . . 8
β’ ((((π΅ β TopBases β§ π½ β 2ndΟ)
β§ (π β TopBases
β§ (π βΌ Ο
β§ (topGenβπ) =
π½))) β§ (π:πβΆπ΅ β§ βπ₯ β π ((1st βπ₯) β (πβπ₯) β§ (πβπ₯) β (2nd βπ₯)))) β ran π βΌ π) |
193 | | domtr 8954 |
. . . . . . . 8
β’ ((ran
π βΌ π β§ π βΌ Ο) β ran π βΌ
Ο) |
194 | 192, 185,
193 | syl2anc 585 |
. . . . . . 7
β’ ((((π΅ β TopBases β§ π½ β 2ndΟ)
β§ (π β TopBases
β§ (π βΌ Ο
β§ (topGenβπ) =
π½))) β§ (π:πβΆπ΅ β§ βπ₯ β π ((1st βπ₯) β (πβπ₯) β§ (πβπ₯) β (2nd βπ₯)))) β ran π βΌ
Ο) |
195 | 180 | eqcomd 2743 |
. . . . . . 7
β’ ((((π΅ β TopBases β§ π½ β 2ndΟ)
β§ (π β TopBases
β§ (π βΌ Ο
β§ (topGenβπ) =
π½))) β§ (π:πβΆπ΅ β§ βπ₯ β π ((1st βπ₯) β (πβπ₯) β§ (πβπ₯) β (2nd βπ₯)))) β π½ = (topGenβran π)) |
196 | | breq1 5113 |
. . . . . . . . 9
β’ (π = ran π β (π βΌ Ο β ran π βΌ
Ο)) |
197 | | sseq1 3974 |
. . . . . . . . 9
β’ (π = ran π β (π β π΅ β ran π β π΅)) |
198 | | fveq2 6847 |
. . . . . . . . . 10
β’ (π = ran π β (topGenβπ) = (topGenβran π)) |
199 | 198 | eqeq2d 2748 |
. . . . . . . . 9
β’ (π = ran π β (π½ = (topGenβπ) β π½ = (topGenβran π))) |
200 | 196, 197,
199 | 3anbi123d 1437 |
. . . . . . . 8
β’ (π = ran π β ((π βΌ Ο β§ π β π΅ β§ π½ = (topGenβπ)) β (ran π βΌ Ο β§ ran π β π΅ β§ π½ = (topGenβran π)))) |
201 | 200 | rspcev 3584 |
. . . . . . 7
β’ ((ran
π β TopBases β§
(ran π βΌ Ο
β§ ran π β π΅ β§ π½ = (topGenβran π))) β βπ β TopBases (π βΌ Ο β§ π β π΅ β§ π½ = (topGenβπ))) |
202 | 183, 194,
64, 195, 201 | syl13anc 1373 |
. . . . . 6
β’ ((((π΅ β TopBases β§ π½ β 2ndΟ)
β§ (π β TopBases
β§ (π βΌ Ο
β§ (topGenβπ) =
π½))) β§ (π:πβΆπ΅ β§ βπ₯ β π ((1st βπ₯) β (πβπ₯) β§ (πβπ₯) β (2nd βπ₯)))) β βπ β TopBases (π βΌ Ο β§ π β π΅ β§ π½ = (topGenβπ))) |
203 | 202 | ex 414 |
. . . . 5
β’ (((π΅ β TopBases β§ π½ β 2ndΟ)
β§ (π β TopBases
β§ (π βΌ Ο
β§ (topGenβπ) =
π½))) β ((π:πβΆπ΅ β§ βπ₯ β π ((1st βπ₯) β (πβπ₯) β§ (πβπ₯) β (2nd βπ₯))) β βπ β TopBases (π βΌ Ο β§ π β π΅ β§ π½ = (topGenβπ)))) |
204 | 59, 203 | sylbid 239 |
. . . 4
β’ (((π΅ β TopBases β§ π½ β 2ndΟ)
β§ (π β TopBases
β§ (π βΌ Ο
β§ (topGenβπ) =
π½))) β ((π:πβΆ( I βπ΅) β§ βπ₯ β π ((1st βπ₯) β (πβπ₯) β§ (πβπ₯) β (2nd βπ₯))) β βπ β TopBases (π βΌ Ο β§ π β π΅ β§ π½ = (topGenβπ)))) |
205 | 204 | exlimdv 1937 |
. . 3
β’ (((π΅ β TopBases β§ π½ β 2ndΟ)
β§ (π β TopBases
β§ (π βΌ Ο
β§ (topGenβπ) =
π½))) β (βπ(π:πβΆ( I βπ΅) β§ βπ₯ β π ((1st βπ₯) β (πβπ₯) β§ (πβπ₯) β (2nd βπ₯))) β βπ β TopBases (π βΌ Ο β§ π β π΅ β§ π½ = (topGenβπ)))) |
206 | 56, 205 | mpd 15 |
. 2
β’ (((π΅ β TopBases β§ π½ β 2ndΟ)
β§ (π β TopBases
β§ (π βΌ Ο
β§ (topGenβπ) =
π½))) β βπ β TopBases (π βΌ Ο β§ π β π΅ β§ π½ = (topGenβπ))) |
207 | 3, 206 | rexlimddv 3159 |
1
β’ ((π΅ β TopBases β§ π½ β 2ndΟ)
β βπ β
TopBases (π βΌ Ο
β§ π β π΅ β§ π½ = (topGenβπ))) |