Step | Hyp | Ref
| Expression |
1 | | is2ndc 22820 |
. 2
β’ (π
β 2ndΟ
β βπ β
TopBases (π βΌ Ο
β§ (topGenβπ) =
π
)) |
2 | | is2ndc 22820 |
. 2
β’ (π β 2ndΟ
β βπ β
TopBases (π βΌ Ο
β§ (topGenβπ ) =
π)) |
3 | | reeanv 3216 |
. . 3
β’
(βπ β
TopBases βπ β
TopBases ((π βΌ
Ο β§ (topGenβπ) = π
) β§ (π βΌ Ο β§ (topGenβπ ) = π)) β (βπ β TopBases (π βΌ Ο β§ (topGenβπ) = π
) β§ βπ β TopBases (π βΌ Ο β§ (topGenβπ ) = π))) |
4 | | an4 655 |
. . . . 5
β’ (((π βΌ Ο β§
(topGenβπ) = π
) β§ (π βΌ Ο β§ (topGenβπ ) = π)) β ((π βΌ Ο β§ π βΌ Ο) β§ ((topGenβπ) = π
β§ (topGenβπ ) = π))) |
5 | | txbasval 22980 |
. . . . . . . . . 10
β’ ((π β TopBases β§ π β TopBases) β
((topGenβπ)
Γt (topGenβπ )) = (π Γt π )) |
6 | | eqid 2733 |
. . . . . . . . . . 11
β’ ran
(π₯ β π, π¦ β π β¦ (π₯ Γ π¦)) = ran (π₯ β π, π¦ β π β¦ (π₯ Γ π¦)) |
7 | 6 | txval 22938 |
. . . . . . . . . 10
β’ ((π β TopBases β§ π β TopBases) β (π Γt π ) = (topGenβran (π₯ β π, π¦ β π β¦ (π₯ Γ π¦)))) |
8 | 5, 7 | eqtrd 2773 |
. . . . . . . . 9
β’ ((π β TopBases β§ π β TopBases) β
((topGenβπ)
Γt (topGenβπ )) = (topGenβran (π₯ β π, π¦ β π β¦ (π₯ Γ π¦)))) |
9 | 8 | adantr 482 |
. . . . . . . 8
β’ (((π β TopBases β§ π β TopBases) β§ (π βΌ Ο β§ π βΌ Ο)) β
((topGenβπ)
Γt (topGenβπ )) = (topGenβran (π₯ β π, π¦ β π β¦ (π₯ Γ π¦)))) |
10 | 6 | txbas 22941 |
. . . . . . . . . 10
β’ ((π β TopBases β§ π β TopBases) β ran
(π₯ β π, π¦ β π β¦ (π₯ Γ π¦)) β TopBases) |
11 | 10 | adantr 482 |
. . . . . . . . 9
β’ (((π β TopBases β§ π β TopBases) β§ (π βΌ Ο β§ π βΌ Ο)) β ran
(π₯ β π, π¦ β π β¦ (π₯ Γ π¦)) β TopBases) |
12 | | omelon 9590 |
. . . . . . . . . . . 12
β’ Ο
β On |
13 | | vex 3451 |
. . . . . . . . . . . . . . . 16
β’ π β V |
14 | 13 | xpdom1 9021 |
. . . . . . . . . . . . . . 15
β’ (π βΌ Ο β (π Γ π ) βΌ (Ο Γ π )) |
15 | | omex 9587 |
. . . . . . . . . . . . . . . 16
β’ Ο
β V |
16 | 15 | xpdom2 9017 |
. . . . . . . . . . . . . . 15
β’ (π βΌ Ο β (Ο
Γ π ) βΌ (Ο
Γ Ο)) |
17 | | domtr 8953 |
. . . . . . . . . . . . . . 15
β’ (((π Γ π ) βΌ (Ο Γ π ) β§ (Ο Γ π ) βΌ (Ο Γ Ο)) β
(π Γ π ) βΌ (Ο Γ
Ο)) |
18 | 14, 16, 17 | syl2an 597 |
. . . . . . . . . . . . . 14
β’ ((π βΌ Ο β§ π βΌ Ο) β (π Γ π ) βΌ (Ο Γ
Ο)) |
19 | 18 | adantl 483 |
. . . . . . . . . . . . 13
β’ (((π β TopBases β§ π β TopBases) β§ (π βΌ Ο β§ π βΌ Ο)) β (π Γ π ) βΌ (Ο Γ
Ο)) |
20 | | xpomen 9959 |
. . . . . . . . . . . . 13
β’ (Ο
Γ Ο) β Ο |
21 | | domentr 8959 |
. . . . . . . . . . . . 13
β’ (((π Γ π ) βΌ (Ο Γ Ο) β§
(Ο Γ Ο) β Ο) β (π Γ π ) βΌ Ο) |
22 | 19, 20, 21 | sylancl 587 |
. . . . . . . . . . . 12
β’ (((π β TopBases β§ π β TopBases) β§ (π βΌ Ο β§ π βΌ Ο)) β (π Γ π ) βΌ Ο) |
23 | | ondomen 9981 |
. . . . . . . . . . . 12
β’ ((Ο
β On β§ (π Γ
π ) βΌ Ο) β
(π Γ π ) β dom
card) |
24 | 12, 22, 23 | sylancr 588 |
. . . . . . . . . . 11
β’ (((π β TopBases β§ π β TopBases) β§ (π βΌ Ο β§ π βΌ Ο)) β (π Γ π ) β dom card) |
25 | | eqid 2733 |
. . . . . . . . . . . . . 14
β’ (π₯ β π, π¦ β π β¦ (π₯ Γ π¦)) = (π₯ β π, π¦ β π β¦ (π₯ Γ π¦)) |
26 | | vex 3451 |
. . . . . . . . . . . . . . 15
β’ π₯ β V |
27 | | vex 3451 |
. . . . . . . . . . . . . . 15
β’ π¦ β V |
28 | 26, 27 | xpex 7691 |
. . . . . . . . . . . . . 14
β’ (π₯ Γ π¦) β V |
29 | 25, 28 | fnmpoi 8006 |
. . . . . . . . . . . . 13
β’ (π₯ β π, π¦ β π β¦ (π₯ Γ π¦)) Fn (π Γ π ) |
30 | 29 | a1i 11 |
. . . . . . . . . . . 12
β’ (((π β TopBases β§ π β TopBases) β§ (π βΌ Ο β§ π βΌ Ο)) β (π₯ β π, π¦ β π β¦ (π₯ Γ π¦)) Fn (π Γ π )) |
31 | | dffn4 6766 |
. . . . . . . . . . . 12
β’ ((π₯ β π, π¦ β π β¦ (π₯ Γ π¦)) Fn (π Γ π ) β (π₯ β π, π¦ β π β¦ (π₯ Γ π¦)):(π Γ π )βontoβran (π₯ β π, π¦ β π β¦ (π₯ Γ π¦))) |
32 | 30, 31 | sylib 217 |
. . . . . . . . . . 11
β’ (((π β TopBases β§ π β TopBases) β§ (π βΌ Ο β§ π βΌ Ο)) β (π₯ β π, π¦ β π β¦ (π₯ Γ π¦)):(π Γ π )βontoβran (π₯ β π, π¦ β π β¦ (π₯ Γ π¦))) |
33 | | fodomnum 10001 |
. . . . . . . . . . 11
β’ ((π Γ π ) β dom card β ((π₯ β π, π¦ β π β¦ (π₯ Γ π¦)):(π Γ π )βontoβran (π₯ β π, π¦ β π β¦ (π₯ Γ π¦)) β ran (π₯ β π, π¦ β π β¦ (π₯ Γ π¦)) βΌ (π Γ π ))) |
34 | 24, 32, 33 | sylc 65 |
. . . . . . . . . 10
β’ (((π β TopBases β§ π β TopBases) β§ (π βΌ Ο β§ π βΌ Ο)) β ran
(π₯ β π, π¦ β π β¦ (π₯ Γ π¦)) βΌ (π Γ π )) |
35 | | domtr 8953 |
. . . . . . . . . 10
β’ ((ran
(π₯ β π, π¦ β π β¦ (π₯ Γ π¦)) βΌ (π Γ π ) β§ (π Γ π ) βΌ Ο) β ran (π₯ β π, π¦ β π β¦ (π₯ Γ π¦)) βΌ Ο) |
36 | 34, 22, 35 | syl2anc 585 |
. . . . . . . . 9
β’ (((π β TopBases β§ π β TopBases) β§ (π βΌ Ο β§ π βΌ Ο)) β ran
(π₯ β π, π¦ β π β¦ (π₯ Γ π¦)) βΌ Ο) |
37 | | 2ndci 22822 |
. . . . . . . . 9
β’ ((ran
(π₯ β π, π¦ β π β¦ (π₯ Γ π¦)) β TopBases β§ ran (π₯ β π, π¦ β π β¦ (π₯ Γ π¦)) βΌ Ο) β (topGenβran
(π₯ β π, π¦ β π β¦ (π₯ Γ π¦))) β
2ndΟ) |
38 | 11, 36, 37 | syl2anc 585 |
. . . . . . . 8
β’ (((π β TopBases β§ π β TopBases) β§ (π βΌ Ο β§ π βΌ Ο)) β
(topGenβran (π₯ β
π, π¦ β π β¦ (π₯ Γ π¦))) β
2ndΟ) |
39 | 9, 38 | eqeltrd 2834 |
. . . . . . 7
β’ (((π β TopBases β§ π β TopBases) β§ (π βΌ Ο β§ π βΌ Ο)) β
((topGenβπ)
Γt (topGenβπ )) β
2ndΟ) |
40 | | oveq12 7370 |
. . . . . . . 8
β’
(((topGenβπ) =
π
β§ (topGenβπ ) = π) β ((topGenβπ) Γt (topGenβπ )) = (π
Γt π)) |
41 | 40 | eleq1d 2819 |
. . . . . . 7
β’
(((topGenβπ) =
π
β§ (topGenβπ ) = π) β (((topGenβπ) Γt (topGenβπ )) β 2ndΟ
β (π
Γt π)
β 2ndΟ)) |
42 | 39, 41 | syl5ibcom 244 |
. . . . . 6
β’ (((π β TopBases β§ π β TopBases) β§ (π βΌ Ο β§ π βΌ Ο)) β
(((topGenβπ) = π
β§ (topGenβπ ) = π) β (π
Γt π) β
2ndΟ)) |
43 | 42 | expimpd 455 |
. . . . 5
β’ ((π β TopBases β§ π β TopBases) β
(((π βΌ Ο β§
π βΌ Ο) β§
((topGenβπ) = π
β§ (topGenβπ ) = π)) β (π
Γt π) β
2ndΟ)) |
44 | 4, 43 | biimtrid 241 |
. . . 4
β’ ((π β TopBases β§ π β TopBases) β
(((π βΌ Ο β§
(topGenβπ) = π
) β§ (π βΌ Ο β§ (topGenβπ ) = π)) β (π
Γt π) β
2ndΟ)) |
45 | 44 | rexlimivv 3193 |
. . 3
β’
(βπ β
TopBases βπ β
TopBases ((π βΌ
Ο β§ (topGenβπ) = π
) β§ (π βΌ Ο β§ (topGenβπ ) = π)) β (π
Γt π) β
2ndΟ) |
46 | 3, 45 | sylbir 234 |
. 2
β’
((βπ β
TopBases (π βΌ Ο
β§ (topGenβπ) =
π
) β§ βπ β TopBases (π βΌ Ο β§
(topGenβπ ) = π)) β (π
Γt π) β
2ndΟ) |
47 | 1, 2, 46 | syl2anb 599 |
1
β’ ((π
β 2ndΟ
β§ π β
2ndΟ) β (π
Γt π) β
2ndΟ) |