Step | Hyp | Ref
| Expression |
1 | | eqid 2177 |
. . . 4
β’ ran
(π’ β π
, π£ β π β¦ (π’ Γ π£)) = ran (π’ β π
, π£ β π β¦ (π’ Γ π£)) |
2 | 1 | txbasex 13727 |
. . 3
β’ ((π
β π β§ π β π) β ran (π’ β π
, π£ β π β¦ (π’ Γ π£)) β V) |
3 | | bastg 13531 |
. . . . . 6
β’ (π
β π β π
β (topGenβπ
)) |
4 | | bastg 13531 |
. . . . . 6
β’ (π β π β π β (topGenβπ)) |
5 | | resmpo 5972 |
. . . . . 6
β’ ((π
β (topGenβπ
) β§ π β (topGenβπ)) β ((π’ β (topGenβπ
), π£ β (topGenβπ) β¦ (π’ Γ π£)) βΎ (π
Γ π)) = (π’ β π
, π£ β π β¦ (π’ Γ π£))) |
6 | 3, 4, 5 | syl2an 289 |
. . . . 5
β’ ((π
β π β§ π β π) β ((π’ β (topGenβπ
), π£ β (topGenβπ) β¦ (π’ Γ π£)) βΎ (π
Γ π)) = (π’ β π
, π£ β π β¦ (π’ Γ π£))) |
7 | | resss 4931 |
. . . . 5
β’ ((π’ β (topGenβπ
), π£ β (topGenβπ) β¦ (π’ Γ π£)) βΎ (π
Γ π)) β (π’ β (topGenβπ
), π£ β (topGenβπ) β¦ (π’ Γ π£)) |
8 | 6, 7 | eqsstrrdi 3208 |
. . . 4
β’ ((π
β π β§ π β π) β (π’ β π
, π£ β π β¦ (π’ Γ π£)) β (π’ β (topGenβπ
), π£ β (topGenβπ) β¦ (π’ Γ π£))) |
9 | | rnss 4857 |
. . . 4
β’ ((π’ β π
, π£ β π β¦ (π’ Γ π£)) β (π’ β (topGenβπ
), π£ β (topGenβπ) β¦ (π’ Γ π£)) β ran (π’ β π
, π£ β π β¦ (π’ Γ π£)) β ran (π’ β (topGenβπ
), π£ β (topGenβπ) β¦ (π’ Γ π£))) |
10 | 8, 9 | syl 14 |
. . 3
β’ ((π
β π β§ π β π) β ran (π’ β π
, π£ β π β¦ (π’ Γ π£)) β ran (π’ β (topGenβπ
), π£ β (topGenβπ) β¦ (π’ Γ π£))) |
11 | | eltg3 13527 |
. . . . . . . . 9
β’ (π
β π β (π’ β (topGenβπ
) β βπ(π β π
β§ π’ = βͺ π))) |
12 | | eltg3 13527 |
. . . . . . . . 9
β’ (π β π β (π£ β (topGenβπ) β βπ(π β π β§ π£ = βͺ π))) |
13 | 11, 12 | bi2anan9 606 |
. . . . . . . 8
β’ ((π
β π β§ π β π) β ((π’ β (topGenβπ
) β§ π£ β (topGenβπ)) β (βπ(π β π
β§ π’ = βͺ π) β§ βπ(π β π β§ π£ = βͺ π)))) |
14 | | exdistrv 1910 |
. . . . . . . . 9
β’
(βπβπ((π β π
β§ π’ = βͺ π) β§ (π β π β§ π£ = βͺ π)) β (βπ(π β π
β§ π’ = βͺ π) β§ βπ(π β π β§ π£ = βͺ π))) |
15 | | an4 586 |
. . . . . . . . . . 11
β’ (((π β π
β§ π’ = βͺ π) β§ (π β π β§ π£ = βͺ π)) β ((π β π
β§ π β π) β§ (π’ = βͺ π β§ π£ = βͺ π))) |
16 | | uniiun 3940 |
. . . . . . . . . . . . . . . 16
β’ βͺ π =
βͺ π₯ β π π₯ |
17 | | uniiun 3940 |
. . . . . . . . . . . . . . . 16
β’ βͺ π =
βͺ π¦ β π π¦ |
18 | 16, 17 | xpeq12i 4648 |
. . . . . . . . . . . . . . 15
β’ (βͺ π
Γ βͺ π) = (βͺ
π₯ β π π₯ Γ βͺ
π¦ β π π¦) |
19 | | xpiundir 4685 |
. . . . . . . . . . . . . . 15
β’ (βͺ π₯ β π π₯ Γ βͺ
π¦ β π π¦) = βͺ π₯ β π (π₯ Γ βͺ
π¦ β π π¦) |
20 | | xpiundi 4684 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ Γ βͺ π¦ β π π¦) = βͺ π¦ β π (π₯ Γ π¦) |
21 | 20 | a1i 9 |
. . . . . . . . . . . . . . . 16
β’ (π₯ β π β (π₯ Γ βͺ
π¦ β π π¦) = βͺ π¦ β π (π₯ Γ π¦)) |
22 | 21 | iuneq2i 3904 |
. . . . . . . . . . . . . . 15
β’ βͺ π₯ β π (π₯ Γ βͺ
π¦ β π π¦) = βͺ π₯ β π βͺ π¦ β π (π₯ Γ π¦) |
23 | 18, 19, 22 | 3eqtri 2202 |
. . . . . . . . . . . . . 14
β’ (βͺ π
Γ βͺ π) = βͺ π₯ β π βͺ π¦ β π (π₯ Γ π¦) |
24 | | txvalex 13724 |
. . . . . . . . . . . . . . . . 17
β’ ((π
β π β§ π β π) β (π
Γt π) β V) |
25 | 24 | adantr 276 |
. . . . . . . . . . . . . . . 16
β’ (((π
β π β§ π β π) β§ (π β π
β§ π β π)) β (π
Γt π) β V) |
26 | 24 | ad2antrr 488 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π
β π β§ π β π) β§ (π β π
β§ π β π)) β§ π₯ β π) β (π
Γt π) β V) |
27 | | ssel2 3150 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β π
β§ π₯ β π) β π₯ β π
) |
28 | | ssel2 3150 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β π β§ π¦ β π) β π¦ β π) |
29 | 27, 28 | anim12i 338 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β π
β§ π₯ β π) β§ (π β π β§ π¦ β π)) β (π₯ β π
β§ π¦ β π)) |
30 | 29 | an4s 588 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β π
β§ π β π) β§ (π₯ β π β§ π¦ β π)) β (π₯ β π
β§ π¦ β π)) |
31 | | txopn 13735 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π
β π β§ π β π) β§ (π₯ β π
β§ π¦ β π)) β (π₯ Γ π¦) β (π
Γt π)) |
32 | 30, 31 | sylan2 286 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π
β π β§ π β π) β§ ((π β π
β§ π β π) β§ (π₯ β π β§ π¦ β π))) β (π₯ Γ π¦) β (π
Γt π)) |
33 | 32 | anassrs 400 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π
β π β§ π β π) β§ (π β π
β§ π β π)) β§ (π₯ β π β§ π¦ β π)) β (π₯ Γ π¦) β (π
Γt π)) |
34 | 33 | anassrs 400 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((π
β π β§ π β π) β§ (π β π
β§ π β π)) β§ π₯ β π) β§ π¦ β π) β (π₯ Γ π¦) β (π
Γt π)) |
35 | 34 | ralrimiva 2550 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π
β π β§ π β π) β§ (π β π
β§ π β π)) β§ π₯ β π) β βπ¦ β π (π₯ Γ π¦) β (π
Γt π)) |
36 | | tgiun 13543 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π
Γt π) β V β§ βπ¦ β π (π₯ Γ π¦) β (π
Γt π)) β βͺ π¦ β π (π₯ Γ π¦) β (topGenβ(π
Γt π))) |
37 | 26, 35, 36 | syl2anc 411 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π
β π β§ π β π) β§ (π β π
β§ π β π)) β§ π₯ β π) β βͺ
π¦ β π (π₯ Γ π¦) β (topGenβ(π
Γt π))) |
38 | | tgidm 13544 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (ran
(π’ β π
, π£ β π β¦ (π’ Γ π£)) β V β
(topGenβ(topGenβran (π’ β π
, π£ β π β¦ (π’ Γ π£)))) = (topGenβran (π’ β π
, π£ β π β¦ (π’ Γ π£)))) |
39 | 2, 38 | syl 14 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π
β π β§ π β π) β (topGenβ(topGenβran
(π’ β π
, π£ β π β¦ (π’ Γ π£)))) = (topGenβran (π’ β π
, π£ β π β¦ (π’ Γ π£)))) |
40 | 1 | txval 13725 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π
β π β§ π β π) β (π
Γt π) = (topGenβran (π’ β π
, π£ β π β¦ (π’ Γ π£)))) |
41 | 40 | fveq2d 5519 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π
β π β§ π β π) β (topGenβ(π
Γt π)) = (topGenβ(topGenβran (π’ β π
, π£ β π β¦ (π’ Γ π£))))) |
42 | 39, 41, 40 | 3eqtr4d 2220 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π
β π β§ π β π) β (topGenβ(π
Γt π)) = (π
Γt π)) |
43 | 42 | adantr 276 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π
β π β§ π β π) β§ (π β π
β§ π β π)) β (topGenβ(π
Γt π)) = (π
Γt π)) |
44 | 43 | adantr 276 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π
β π β§ π β π) β§ (π β π
β§ π β π)) β§ π₯ β π) β (topGenβ(π
Γt π)) = (π
Γt π)) |
45 | 37, 44 | eleqtrd 2256 |
. . . . . . . . . . . . . . . . 17
β’ ((((π
β π β§ π β π) β§ (π β π
β§ π β π)) β§ π₯ β π) β βͺ
π¦ β π (π₯ Γ π¦) β (π
Γt π)) |
46 | 45 | ralrimiva 2550 |
. . . . . . . . . . . . . . . 16
β’ (((π
β π β§ π β π) β§ (π β π
β§ π β π)) β βπ₯ β π βͺ π¦ β π (π₯ Γ π¦) β (π
Γt π)) |
47 | | tgiun 13543 |
. . . . . . . . . . . . . . . 16
β’ (((π
Γt π) β V β§ βπ₯ β π βͺ π¦ β π (π₯ Γ π¦) β (π
Γt π)) β βͺ π₯ β π βͺ π¦ β π (π₯ Γ π¦) β (topGenβ(π
Γt π))) |
48 | 25, 46, 47 | syl2anc 411 |
. . . . . . . . . . . . . . 15
β’ (((π
β π β§ π β π) β§ (π β π
β§ π β π)) β βͺ π₯ β π βͺ π¦ β π (π₯ Γ π¦) β (topGenβ(π
Γt π))) |
49 | 48, 43 | eleqtrd 2256 |
. . . . . . . . . . . . . 14
β’ (((π
β π β§ π β π) β§ (π β π
β§ π β π)) β βͺ π₯ β π βͺ π¦ β π (π₯ Γ π¦) β (π
Γt π)) |
50 | 23, 49 | eqeltrid 2264 |
. . . . . . . . . . . . 13
β’ (((π
β π β§ π β π) β§ (π β π
β§ π β π)) β (βͺ
π Γ βͺ π)
β (π
Γt π)) |
51 | | xpeq12 4645 |
. . . . . . . . . . . . . 14
β’ ((π’ = βͺ
π β§ π£ = βͺ π) β (π’ Γ π£) = (βͺ π Γ βͺ π)) |
52 | 51 | eleq1d 2246 |
. . . . . . . . . . . . 13
β’ ((π’ = βͺ
π β§ π£ = βͺ π) β ((π’ Γ π£) β (π
Γt π) β (βͺ π Γ βͺ π)
β (π
Γt π))) |
53 | 50, 52 | syl5ibrcom 157 |
. . . . . . . . . . . 12
β’ (((π
β π β§ π β π) β§ (π β π
β§ π β π)) β ((π’ = βͺ π β§ π£ = βͺ π) β (π’ Γ π£) β (π
Γt π))) |
54 | 53 | expimpd 363 |
. . . . . . . . . . 11
β’ ((π
β π β§ π β π) β (((π β π
β§ π β π) β§ (π’ = βͺ π β§ π£ = βͺ π)) β (π’ Γ π£) β (π
Γt π))) |
55 | 15, 54 | biimtrid 152 |
. . . . . . . . . 10
β’ ((π
β π β§ π β π) β (((π β π
β§ π’ = βͺ π) β§ (π β π β§ π£ = βͺ π)) β (π’ Γ π£) β (π
Γt π))) |
56 | 55 | exlimdvv 1897 |
. . . . . . . . 9
β’ ((π
β π β§ π β π) β (βπβπ((π β π
β§ π’ = βͺ π) β§ (π β π β§ π£ = βͺ π)) β (π’ Γ π£) β (π
Γt π))) |
57 | 14, 56 | biimtrrid 153 |
. . . . . . . 8
β’ ((π
β π β§ π β π) β ((βπ(π β π
β§ π’ = βͺ π) β§ βπ(π β π β§ π£ = βͺ π)) β (π’ Γ π£) β (π
Γt π))) |
58 | 13, 57 | sylbid 150 |
. . . . . . 7
β’ ((π
β π β§ π β π) β ((π’ β (topGenβπ
) β§ π£ β (topGenβπ)) β (π’ Γ π£) β (π
Γt π))) |
59 | 58 | ralrimivv 2558 |
. . . . . 6
β’ ((π
β π β§ π β π) β βπ’ β (topGenβπ
)βπ£ β (topGenβπ)(π’ Γ π£) β (π
Γt π)) |
60 | | eqid 2177 |
. . . . . . 7
β’ (π’ β (topGenβπ
), π£ β (topGenβπ) β¦ (π’ Γ π£)) = (π’ β (topGenβπ
), π£ β (topGenβπ) β¦ (π’ Γ π£)) |
61 | 60 | fmpo 6201 |
. . . . . 6
β’
(βπ’ β
(topGenβπ
)βπ£ β (topGenβπ)(π’ Γ π£) β (π
Γt π) β (π’ β (topGenβπ
), π£ β (topGenβπ) β¦ (π’ Γ π£)):((topGenβπ
) Γ (topGenβπ))βΆ(π
Γt π)) |
62 | 59, 61 | sylib 122 |
. . . . 5
β’ ((π
β π β§ π β π) β (π’ β (topGenβπ
), π£ β (topGenβπ) β¦ (π’ Γ π£)):((topGenβπ
) Γ (topGenβπ))βΆ(π
Γt π)) |
63 | 62 | frnd 5375 |
. . . 4
β’ ((π
β π β§ π β π) β ran (π’ β (topGenβπ
), π£ β (topGenβπ) β¦ (π’ Γ π£)) β (π
Γt π)) |
64 | 63, 40 | sseqtrd 3193 |
. . 3
β’ ((π
β π β§ π β π) β ran (π’ β (topGenβπ
), π£ β (topGenβπ) β¦ (π’ Γ π£)) β (topGenβran (π’ β π
, π£ β π β¦ (π’ Γ π£)))) |
65 | | 2basgeng 13552 |
. . 3
β’ ((ran
(π’ β π
, π£ β π β¦ (π’ Γ π£)) β V β§ ran (π’ β π
, π£ β π β¦ (π’ Γ π£)) β ran (π’ β (topGenβπ
), π£ β (topGenβπ) β¦ (π’ Γ π£)) β§ ran (π’ β (topGenβπ
), π£ β (topGenβπ) β¦ (π’ Γ π£)) β (topGenβran (π’ β π
, π£ β π β¦ (π’ Γ π£)))) β (topGenβran (π’ β π
, π£ β π β¦ (π’ Γ π£))) = (topGenβran (π’ β (topGenβπ
), π£ β (topGenβπ) β¦ (π’ Γ π£)))) |
66 | 2, 10, 64, 65 | syl3anc 1238 |
. 2
β’ ((π
β π β§ π β π) β (topGenβran (π’ β π
, π£ β π β¦ (π’ Γ π£))) = (topGenβran (π’ β (topGenβπ
), π£ β (topGenβπ) β¦ (π’ Γ π£)))) |
67 | | tgvalex 12711 |
. . 3
β’ (π
β π β (topGenβπ
) β V) |
68 | | tgvalex 12711 |
. . 3
β’ (π β π β (topGenβπ) β V) |
69 | | eqid 2177 |
. . . 4
β’ ran
(π’ β
(topGenβπ
), π£ β (topGenβπ) β¦ (π’ Γ π£)) = ran (π’ β (topGenβπ
), π£ β (topGenβπ) β¦ (π’ Γ π£)) |
70 | 69 | txval 13725 |
. . 3
β’
(((topGenβπ
)
β V β§ (topGenβπ) β V) β ((topGenβπ
) Γt
(topGenβπ)) =
(topGenβran (π’ β
(topGenβπ
), π£ β (topGenβπ) β¦ (π’ Γ π£)))) |
71 | 67, 68, 70 | syl2an 289 |
. 2
β’ ((π
β π β§ π β π) β ((topGenβπ
) Γt (topGenβπ)) = (topGenβran (π’ β (topGenβπ
), π£ β (topGenβπ) β¦ (π’ Γ π£)))) |
72 | 66, 40, 71 | 3eqtr4rd 2221 |
1
β’ ((π
β π β§ π β π) β ((topGenβπ
) Γt (topGenβπ)) = (π
Γt π)) |