Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. . 3
β’ ran
(π’ β π
, π£ β π β¦ (π’ Γ π£)) = ran (π’ β π
, π£ β π β¦ (π’ Γ π£)) |
2 | 1 | txval 22938 |
. 2
β’ ((π
β π β§ π β π) β (π
Γt π) = (topGenβran (π’ β π
, π£ β π β¦ (π’ Γ π£)))) |
3 | | bastg 22339 |
. . . . . . 7
β’ (π
β π β π
β (topGenβπ
)) |
4 | | bastg 22339 |
. . . . . . 7
β’ (π β π β π β (topGenβπ)) |
5 | | resmpo 7480 |
. . . . . . 7
β’ ((π
β (topGenβπ
) β§ π β (topGenβπ)) β ((π’ β (topGenβπ
), π£ β (topGenβπ) β¦ (π’ Γ π£)) βΎ (π
Γ π)) = (π’ β π
, π£ β π β¦ (π’ Γ π£))) |
6 | 3, 4, 5 | syl2an 597 |
. . . . . 6
β’ ((π
β π β§ π β π) β ((π’ β (topGenβπ
), π£ β (topGenβπ) β¦ (π’ Γ π£)) βΎ (π
Γ π)) = (π’ β π
, π£ β π β¦ (π’ Γ π£))) |
7 | | resss 5966 |
. . . . . 6
β’ ((π’ β (topGenβπ
), π£ β (topGenβπ) β¦ (π’ Γ π£)) βΎ (π
Γ π)) β (π’ β (topGenβπ
), π£ β (topGenβπ) β¦ (π’ Γ π£)) |
8 | 6, 7 | eqsstrrdi 4003 |
. . . . 5
β’ ((π
β π β§ π β π) β (π’ β π
, π£ β π β¦ (π’ Γ π£)) β (π’ β (topGenβπ
), π£ β (topGenβπ) β¦ (π’ Γ π£))) |
9 | | rnss 5898 |
. . . . 5
β’ ((π’ β π
, π£ β π β¦ (π’ Γ π£)) β (π’ β (topGenβπ
), π£ β (topGenβπ) β¦ (π’ Γ π£)) β ran (π’ β π
, π£ β π β¦ (π’ Γ π£)) β ran (π’ β (topGenβπ
), π£ β (topGenβπ) β¦ (π’ Γ π£))) |
10 | 8, 9 | syl 17 |
. . . 4
β’ ((π
β π β§ π β π) β ran (π’ β π
, π£ β π β¦ (π’ Γ π£)) β ran (π’ β (topGenβπ
), π£ β (topGenβπ) β¦ (π’ Γ π£))) |
11 | | eltg3 22335 |
. . . . . . . . . 10
β’ (π
β π β (π’ β (topGenβπ
) β βπ(π β π
β§ π’ = βͺ π))) |
12 | | eltg3 22335 |
. . . . . . . . . 10
β’ (π β π β (π£ β (topGenβπ) β βπ(π β π β§ π£ = βͺ π))) |
13 | 11, 12 | bi2anan9 638 |
. . . . . . . . 9
β’ ((π
β π β§ π β π) β ((π’ β (topGenβπ
) β§ π£ β (topGenβπ)) β (βπ(π β π
β§ π’ = βͺ π) β§ βπ(π β π β§ π£ = βͺ π)))) |
14 | | exdistrv 1960 |
. . . . . . . . . 10
β’
(βπβπ((π β π
β§ π’ = βͺ π) β§ (π β π β§ π£ = βͺ π)) β (βπ(π β π
β§ π’ = βͺ π) β§ βπ(π β π β§ π£ = βͺ π))) |
15 | | an4 655 |
. . . . . . . . . . . 12
β’ (((π β π
β§ π’ = βͺ π) β§ (π β π β§ π£ = βͺ π)) β ((π β π
β§ π β π) β§ (π’ = βͺ π β§ π£ = βͺ π))) |
16 | | uniiun 5022 |
. . . . . . . . . . . . . . . . 17
β’ βͺ π =
βͺ π₯ β π π₯ |
17 | | uniiun 5022 |
. . . . . . . . . . . . . . . . 17
β’ βͺ π =
βͺ π¦ β π π¦ |
18 | 16, 17 | xpeq12i 5665 |
. . . . . . . . . . . . . . . 16
β’ (βͺ π
Γ βͺ π) = (βͺ
π₯ β π π₯ Γ βͺ
π¦ β π π¦) |
19 | | xpiundir 5707 |
. . . . . . . . . . . . . . . 16
β’ (βͺ π₯ β π π₯ Γ βͺ
π¦ β π π¦) = βͺ π₯ β π (π₯ Γ βͺ
π¦ β π π¦) |
20 | | xpiundi 5706 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ Γ βͺ π¦ β π π¦) = βͺ π¦ β π (π₯ Γ π¦) |
21 | 20 | a1i 11 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ β π β (π₯ Γ βͺ
π¦ β π π¦) = βͺ π¦ β π (π₯ Γ π¦)) |
22 | 21 | iuneq2i 4979 |
. . . . . . . . . . . . . . . 16
β’ βͺ π₯ β π (π₯ Γ βͺ
π¦ β π π¦) = βͺ π₯ β π βͺ π¦ β π (π₯ Γ π¦) |
23 | 18, 19, 22 | 3eqtri 2765 |
. . . . . . . . . . . . . . 15
β’ (βͺ π
Γ βͺ π) = βͺ π₯ β π βͺ π¦ β π (π₯ Γ π¦) |
24 | | ovex 7394 |
. . . . . . . . . . . . . . . . 17
β’ (π
Γt π) β V |
25 | | ssel2 3943 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β π
β§ π₯ β π) β π₯ β π
) |
26 | | ssel2 3943 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β π β§ π¦ β π) β π¦ β π) |
27 | 25, 26 | anim12i 614 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π β π
β§ π₯ β π) β§ (π β π β§ π¦ β π)) β (π₯ β π
β§ π¦ β π)) |
28 | 27 | an4s 659 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β π
β§ π β π) β§ (π₯ β π β§ π¦ β π)) β (π₯ β π
β§ π¦ β π)) |
29 | | txopn 22976 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π
β π β§ π β π) β§ (π₯ β π
β§ π¦ β π)) β (π₯ Γ π¦) β (π
Γt π)) |
30 | 28, 29 | sylan2 594 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π
β π β§ π β π) β§ ((π β π
β§ π β π) β§ (π₯ β π β§ π¦ β π))) β (π₯ Γ π¦) β (π
Γt π)) |
31 | 30 | anassrs 469 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π
β π β§ π β π) β§ (π β π
β§ π β π)) β§ (π₯ β π β§ π¦ β π)) β (π₯ Γ π¦) β (π
Γt π)) |
32 | 31 | anassrs 469 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((π
β π β§ π β π) β§ (π β π
β§ π β π)) β§ π₯ β π) β§ π¦ β π) β (π₯ Γ π¦) β (π
Γt π)) |
33 | 32 | ralrimiva 3140 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π
β π β§ π β π) β§ (π β π
β§ π β π)) β§ π₯ β π) β βπ¦ β π (π₯ Γ π¦) β (π
Γt π)) |
34 | | tgiun 22352 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π
Γt π) β V β§ βπ¦ β π (π₯ Γ π¦) β (π
Γt π)) β βͺ π¦ β π (π₯ Γ π¦) β (topGenβ(π
Γt π))) |
35 | 24, 33, 34 | sylancr 588 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π
β π β§ π β π) β§ (π β π
β§ π β π)) β§ π₯ β π) β βͺ
π¦ β π (π₯ Γ π¦) β (topGenβ(π
Γt π))) |
36 | 1 | txbasex 22940 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π
β π β§ π β π) β ran (π’ β π
, π£ β π β¦ (π’ Γ π£)) β V) |
37 | | tgidm 22353 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (ran
(π’ β π
, π£ β π β¦ (π’ Γ π£)) β V β
(topGenβ(topGenβran (π’ β π
, π£ β π β¦ (π’ Γ π£)))) = (topGenβran (π’ β π
, π£ β π β¦ (π’ Γ π£)))) |
38 | 36, 37 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π
β π β§ π β π) β (topGenβ(topGenβran
(π’ β π
, π£ β π β¦ (π’ Γ π£)))) = (topGenβran (π’ β π
, π£ β π β¦ (π’ Γ π£)))) |
39 | 2 | fveq2d 6850 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π
β π β§ π β π) β (topGenβ(π
Γt π)) = (topGenβ(topGenβran (π’ β π
, π£ β π β¦ (π’ Γ π£))))) |
40 | 38, 39, 2 | 3eqtr4d 2783 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π
β π β§ π β π) β (topGenβ(π
Γt π)) = (π
Γt π)) |
41 | 40 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π
β π β§ π β π) β§ (π β π
β§ π β π)) β (topGenβ(π
Γt π)) = (π
Γt π)) |
42 | 41 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π
β π β§ π β π) β§ (π β π
β§ π β π)) β§ π₯ β π) β (topGenβ(π
Γt π)) = (π
Γt π)) |
43 | 35, 42 | eleqtrd 2836 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π
β π β§ π β π) β§ (π β π
β§ π β π)) β§ π₯ β π) β βͺ
π¦ β π (π₯ Γ π¦) β (π
Γt π)) |
44 | 43 | ralrimiva 3140 |
. . . . . . . . . . . . . . . . 17
β’ (((π
β π β§ π β π) β§ (π β π
β§ π β π)) β βπ₯ β π βͺ π¦ β π (π₯ Γ π¦) β (π
Γt π)) |
45 | | tgiun 22352 |
. . . . . . . . . . . . . . . . 17
β’ (((π
Γt π) β V β§ βπ₯ β π βͺ π¦ β π (π₯ Γ π¦) β (π
Γt π)) β βͺ π₯ β π βͺ π¦ β π (π₯ Γ π¦) β (topGenβ(π
Γt π))) |
46 | 24, 44, 45 | sylancr 588 |
. . . . . . . . . . . . . . . 16
β’ (((π
β π β§ π β π) β§ (π β π
β§ π β π)) β βͺ π₯ β π βͺ π¦ β π (π₯ Γ π¦) β (topGenβ(π
Γt π))) |
47 | 46, 41 | eleqtrd 2836 |
. . . . . . . . . . . . . . 15
β’ (((π
β π β§ π β π) β§ (π β π
β§ π β π)) β βͺ π₯ β π βͺ π¦ β π (π₯ Γ π¦) β (π
Γt π)) |
48 | 23, 47 | eqeltrid 2838 |
. . . . . . . . . . . . . 14
β’ (((π
β π β§ π β π) β§ (π β π
β§ π β π)) β (βͺ
π Γ βͺ π)
β (π
Γt π)) |
49 | | xpeq12 5662 |
. . . . . . . . . . . . . . 15
β’ ((π’ = βͺ
π β§ π£ = βͺ π) β (π’ Γ π£) = (βͺ π Γ βͺ π)) |
50 | 49 | eleq1d 2819 |
. . . . . . . . . . . . . 14
β’ ((π’ = βͺ
π β§ π£ = βͺ π) β ((π’ Γ π£) β (π
Γt π) β (βͺ π Γ βͺ π)
β (π
Γt π))) |
51 | 48, 50 | syl5ibrcom 247 |
. . . . . . . . . . . . 13
β’ (((π
β π β§ π β π) β§ (π β π
β§ π β π)) β ((π’ = βͺ π β§ π£ = βͺ π) β (π’ Γ π£) β (π
Γt π))) |
52 | 51 | expimpd 455 |
. . . . . . . . . . . 12
β’ ((π
β π β§ π β π) β (((π β π
β§ π β π) β§ (π’ = βͺ π β§ π£ = βͺ π)) β (π’ Γ π£) β (π
Γt π))) |
53 | 15, 52 | biimtrid 241 |
. . . . . . . . . . 11
β’ ((π
β π β§ π β π) β (((π β π
β§ π’ = βͺ π) β§ (π β π β§ π£ = βͺ π)) β (π’ Γ π£) β (π
Γt π))) |
54 | 53 | exlimdvv 1938 |
. . . . . . . . . 10
β’ ((π
β π β§ π β π) β (βπβπ((π β π
β§ π’ = βͺ π) β§ (π β π β§ π£ = βͺ π)) β (π’ Γ π£) β (π
Γt π))) |
55 | 14, 54 | biimtrrid 242 |
. . . . . . . . 9
β’ ((π
β π β§ π β π) β ((βπ(π β π
β§ π’ = βͺ π) β§ βπ(π β π β§ π£ = βͺ π)) β (π’ Γ π£) β (π
Γt π))) |
56 | 13, 55 | sylbid 239 |
. . . . . . . 8
β’ ((π
β π β§ π β π) β ((π’ β (topGenβπ
) β§ π£ β (topGenβπ)) β (π’ Γ π£) β (π
Γt π))) |
57 | 56 | ralrimivv 3192 |
. . . . . . 7
β’ ((π
β π β§ π β π) β βπ’ β (topGenβπ
)βπ£ β (topGenβπ)(π’ Γ π£) β (π
Γt π)) |
58 | | eqid 2733 |
. . . . . . . 8
β’ (π’ β (topGenβπ
), π£ β (topGenβπ) β¦ (π’ Γ π£)) = (π’ β (topGenβπ
), π£ β (topGenβπ) β¦ (π’ Γ π£)) |
59 | 58 | fmpo 8004 |
. . . . . . 7
β’
(βπ’ β
(topGenβπ
)βπ£ β (topGenβπ)(π’ Γ π£) β (π
Γt π) β (π’ β (topGenβπ
), π£ β (topGenβπ) β¦ (π’ Γ π£)):((topGenβπ
) Γ (topGenβπ))βΆ(π
Γt π)) |
60 | 57, 59 | sylib 217 |
. . . . . 6
β’ ((π
β π β§ π β π) β (π’ β (topGenβπ
), π£ β (topGenβπ) β¦ (π’ Γ π£)):((topGenβπ
) Γ (topGenβπ))βΆ(π
Γt π)) |
61 | 60 | frnd 6680 |
. . . . 5
β’ ((π
β π β§ π β π) β ran (π’ β (topGenβπ
), π£ β (topGenβπ) β¦ (π’ Γ π£)) β (π
Γt π)) |
62 | 61, 2 | sseqtrd 3988 |
. . . 4
β’ ((π
β π β§ π β π) β ran (π’ β (topGenβπ
), π£ β (topGenβπ) β¦ (π’ Γ π£)) β (topGenβran (π’ β π
, π£ β π β¦ (π’ Γ π£)))) |
63 | | 2basgen 22363 |
. . . 4
β’ ((ran
(π’ β π
, π£ β π β¦ (π’ Γ π£)) β ran (π’ β (topGenβπ
), π£ β (topGenβπ) β¦ (π’ Γ π£)) β§ ran (π’ β (topGenβπ
), π£ β (topGenβπ) β¦ (π’ Γ π£)) β (topGenβran (π’ β π
, π£ β π β¦ (π’ Γ π£)))) β (topGenβran (π’ β π
, π£ β π β¦ (π’ Γ π£))) = (topGenβran (π’ β (topGenβπ
), π£ β (topGenβπ) β¦ (π’ Γ π£)))) |
64 | 10, 62, 63 | syl2anc 585 |
. . 3
β’ ((π
β π β§ π β π) β (topGenβran (π’ β π
, π£ β π β¦ (π’ Γ π£))) = (topGenβran (π’ β (topGenβπ
), π£ β (topGenβπ) β¦ (π’ Γ π£)))) |
65 | | fvex 6859 |
. . . 4
β’
(topGenβπ
)
β V |
66 | | fvex 6859 |
. . . 4
β’
(topGenβπ)
β V |
67 | | eqid 2733 |
. . . . 5
β’ ran
(π’ β
(topGenβπ
), π£ β (topGenβπ) β¦ (π’ Γ π£)) = ran (π’ β (topGenβπ
), π£ β (topGenβπ) β¦ (π’ Γ π£)) |
68 | 67 | txval 22938 |
. . . 4
β’
(((topGenβπ
)
β V β§ (topGenβπ) β V) β ((topGenβπ
) Γt
(topGenβπ)) =
(topGenβran (π’ β
(topGenβπ
), π£ β (topGenβπ) β¦ (π’ Γ π£)))) |
69 | 65, 66, 68 | mp2an 691 |
. . 3
β’
((topGenβπ
)
Γt (topGenβπ)) = (topGenβran (π’ β (topGenβπ
), π£ β (topGenβπ) β¦ (π’ Γ π£))) |
70 | 64, 69 | eqtr4di 2791 |
. 2
β’ ((π
β π β§ π β π) β (topGenβran (π’ β π
, π£ β π β¦ (π’ Γ π£))) = ((topGenβπ
) Γt (topGenβπ))) |
71 | 2, 70 | eqtr2d 2774 |
1
β’ ((π
β π β§ π β π) β ((topGenβπ
) Γt (topGenβπ)) = (π
Γt π)) |