Step | Hyp | Ref
| Expression |
1 | | txcnmpt.1 |
. . . . . . 7
β’ π = βͺ
π |
2 | | eqid 2733 |
. . . . . . 7
β’ βͺ π
=
βͺ π
|
3 | 1, 2 | cnf 22750 |
. . . . . 6
β’ (πΉ β (π Cn π
) β πΉ:πβΆβͺ π
) |
4 | 3 | adantr 482 |
. . . . 5
β’ ((πΉ β (π Cn π
) β§ πΊ β (π Cn π)) β πΉ:πβΆβͺ π
) |
5 | 4 | ffvelcdmda 7087 |
. . . 4
β’ (((πΉ β (π Cn π
) β§ πΊ β (π Cn π)) β§ π₯ β π) β (πΉβπ₯) β βͺ π
) |
6 | | eqid 2733 |
. . . . . . 7
β’ βͺ π =
βͺ π |
7 | 1, 6 | cnf 22750 |
. . . . . 6
β’ (πΊ β (π Cn π) β πΊ:πβΆβͺ π) |
8 | 7 | adantl 483 |
. . . . 5
β’ ((πΉ β (π Cn π
) β§ πΊ β (π Cn π)) β πΊ:πβΆβͺ π) |
9 | 8 | ffvelcdmda 7087 |
. . . 4
β’ (((πΉ β (π Cn π
) β§ πΊ β (π Cn π)) β§ π₯ β π) β (πΊβπ₯) β βͺ π) |
10 | 5, 9 | opelxpd 5716 |
. . 3
β’ (((πΉ β (π Cn π
) β§ πΊ β (π Cn π)) β§ π₯ β π) β β¨(πΉβπ₯), (πΊβπ₯)β© β (βͺ
π
Γ βͺ π)) |
11 | | txcnmpt.2 |
. . 3
β’ π» = (π₯ β π β¦ β¨(πΉβπ₯), (πΊβπ₯)β©) |
12 | 10, 11 | fmptd 7114 |
. 2
β’ ((πΉ β (π Cn π
) β§ πΊ β (π Cn π)) β π»:πβΆ(βͺ π
Γ βͺ π)) |
13 | 11 | mptpreima 6238 |
. . . . . 6
β’ (β‘π» β (π Γ π )) = {π₯ β π β£ β¨(πΉβπ₯), (πΊβπ₯)β© β (π Γ π )} |
14 | 4 | adantr 482 |
. . . . . . . . . . . . 13
β’ (((πΉ β (π Cn π
) β§ πΊ β (π Cn π)) β§ (π β π
β§ π β π)) β πΉ:πβΆβͺ π
) |
15 | 14 | adantr 482 |
. . . . . . . . . . . 12
β’ ((((πΉ β (π Cn π
) β§ πΊ β (π Cn π)) β§ (π β π
β§ π β π)) β§ π₯ β π) β πΉ:πβΆβͺ π
) |
16 | | ffn 6718 |
. . . . . . . . . . . 12
β’ (πΉ:πβΆβͺ π
β πΉ Fn π) |
17 | | elpreima 7060 |
. . . . . . . . . . . 12
β’ (πΉ Fn π β (π₯ β (β‘πΉ β π) β (π₯ β π β§ (πΉβπ₯) β π))) |
18 | 15, 16, 17 | 3syl 18 |
. . . . . . . . . . 11
β’ ((((πΉ β (π Cn π
) β§ πΊ β (π Cn π)) β§ (π β π
β§ π β π)) β§ π₯ β π) β (π₯ β (β‘πΉ β π) β (π₯ β π β§ (πΉβπ₯) β π))) |
19 | | ibar 530 |
. . . . . . . . . . . 12
β’ (π₯ β π β ((πΉβπ₯) β π β (π₯ β π β§ (πΉβπ₯) β π))) |
20 | 19 | adantl 483 |
. . . . . . . . . . 11
β’ ((((πΉ β (π Cn π
) β§ πΊ β (π Cn π)) β§ (π β π
β§ π β π)) β§ π₯ β π) β ((πΉβπ₯) β π β (π₯ β π β§ (πΉβπ₯) β π))) |
21 | 18, 20 | bitr4d 282 |
. . . . . . . . . 10
β’ ((((πΉ β (π Cn π
) β§ πΊ β (π Cn π)) β§ (π β π
β§ π β π)) β§ π₯ β π) β (π₯ β (β‘πΉ β π) β (πΉβπ₯) β π)) |
22 | 8 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ ((((πΉ β (π Cn π
) β§ πΊ β (π Cn π)) β§ (π β π
β§ π β π)) β§ π₯ β π) β πΊ:πβΆβͺ π) |
23 | | ffn 6718 |
. . . . . . . . . . . 12
β’ (πΊ:πβΆβͺ π β πΊ Fn π) |
24 | | elpreima 7060 |
. . . . . . . . . . . 12
β’ (πΊ Fn π β (π₯ β (β‘πΊ β π ) β (π₯ β π β§ (πΊβπ₯) β π ))) |
25 | 22, 23, 24 | 3syl 18 |
. . . . . . . . . . 11
β’ ((((πΉ β (π Cn π
) β§ πΊ β (π Cn π)) β§ (π β π
β§ π β π)) β§ π₯ β π) β (π₯ β (β‘πΊ β π ) β (π₯ β π β§ (πΊβπ₯) β π ))) |
26 | | ibar 530 |
. . . . . . . . . . . 12
β’ (π₯ β π β ((πΊβπ₯) β π β (π₯ β π β§ (πΊβπ₯) β π ))) |
27 | 26 | adantl 483 |
. . . . . . . . . . 11
β’ ((((πΉ β (π Cn π
) β§ πΊ β (π Cn π)) β§ (π β π
β§ π β π)) β§ π₯ β π) β ((πΊβπ₯) β π β (π₯ β π β§ (πΊβπ₯) β π ))) |
28 | 25, 27 | bitr4d 282 |
. . . . . . . . . 10
β’ ((((πΉ β (π Cn π
) β§ πΊ β (π Cn π)) β§ (π β π
β§ π β π)) β§ π₯ β π) β (π₯ β (β‘πΊ β π ) β (πΊβπ₯) β π )) |
29 | 21, 28 | anbi12d 632 |
. . . . . . . . 9
β’ ((((πΉ β (π Cn π
) β§ πΊ β (π Cn π)) β§ (π β π
β§ π β π)) β§ π₯ β π) β ((π₯ β (β‘πΉ β π) β§ π₯ β (β‘πΊ β π )) β ((πΉβπ₯) β π β§ (πΊβπ₯) β π ))) |
30 | | elin 3965 |
. . . . . . . . 9
β’ (π₯ β ((β‘πΉ β π) β© (β‘πΊ β π )) β (π₯ β (β‘πΉ β π) β§ π₯ β (β‘πΊ β π ))) |
31 | | opelxp 5713 |
. . . . . . . . 9
β’
(β¨(πΉβπ₯), (πΊβπ₯)β© β (π Γ π ) β ((πΉβπ₯) β π β§ (πΊβπ₯) β π )) |
32 | 29, 30, 31 | 3bitr4g 314 |
. . . . . . . 8
β’ ((((πΉ β (π Cn π
) β§ πΊ β (π Cn π)) β§ (π β π
β§ π β π)) β§ π₯ β π) β (π₯ β ((β‘πΉ β π) β© (β‘πΊ β π )) β β¨(πΉβπ₯), (πΊβπ₯)β© β (π Γ π ))) |
33 | 32 | rabbi2dva 4218 |
. . . . . . 7
β’ (((πΉ β (π Cn π
) β§ πΊ β (π Cn π)) β§ (π β π
β§ π β π)) β (π β© ((β‘πΉ β π) β© (β‘πΊ β π ))) = {π₯ β π β£ β¨(πΉβπ₯), (πΊβπ₯)β© β (π Γ π )}) |
34 | | inss1 4229 |
. . . . . . . . . 10
β’ ((β‘πΉ β π) β© (β‘πΊ β π )) β (β‘πΉ β π) |
35 | | cnvimass 6081 |
. . . . . . . . . 10
β’ (β‘πΉ β π) β dom πΉ |
36 | 34, 35 | sstri 3992 |
. . . . . . . . 9
β’ ((β‘πΉ β π) β© (β‘πΊ β π )) β dom πΉ |
37 | 36, 14 | fssdm 6738 |
. . . . . . . 8
β’ (((πΉ β (π Cn π
) β§ πΊ β (π Cn π)) β§ (π β π
β§ π β π)) β ((β‘πΉ β π) β© (β‘πΊ β π )) β π) |
38 | | sseqin2 4216 |
. . . . . . . 8
β’ (((β‘πΉ β π) β© (β‘πΊ β π )) β π β (π β© ((β‘πΉ β π) β© (β‘πΊ β π ))) = ((β‘πΉ β π) β© (β‘πΊ β π ))) |
39 | 37, 38 | sylib 217 |
. . . . . . 7
β’ (((πΉ β (π Cn π
) β§ πΊ β (π Cn π)) β§ (π β π
β§ π β π)) β (π β© ((β‘πΉ β π) β© (β‘πΊ β π ))) = ((β‘πΉ β π) β© (β‘πΊ β π ))) |
40 | 33, 39 | eqtr3d 2775 |
. . . . . 6
β’ (((πΉ β (π Cn π
) β§ πΊ β (π Cn π)) β§ (π β π
β§ π β π)) β {π₯ β π β£ β¨(πΉβπ₯), (πΊβπ₯)β© β (π Γ π )} = ((β‘πΉ β π) β© (β‘πΊ β π ))) |
41 | 13, 40 | eqtrid 2785 |
. . . . 5
β’ (((πΉ β (π Cn π
) β§ πΊ β (π Cn π)) β§ (π β π
β§ π β π)) β (β‘π» β (π Γ π )) = ((β‘πΉ β π) β© (β‘πΊ β π ))) |
42 | | cntop1 22744 |
. . . . . . . 8
β’ (πΊ β (π Cn π) β π β Top) |
43 | 42 | adantl 483 |
. . . . . . 7
β’ ((πΉ β (π Cn π
) β§ πΊ β (π Cn π)) β π β Top) |
44 | 43 | adantr 482 |
. . . . . 6
β’ (((πΉ β (π Cn π
) β§ πΊ β (π Cn π)) β§ (π β π
β§ π β π)) β π β Top) |
45 | | cnima 22769 |
. . . . . . 7
β’ ((πΉ β (π Cn π
) β§ π β π
) β (β‘πΉ β π) β π) |
46 | 45 | ad2ant2r 746 |
. . . . . 6
β’ (((πΉ β (π Cn π
) β§ πΊ β (π Cn π)) β§ (π β π
β§ π β π)) β (β‘πΉ β π) β π) |
47 | | cnima 22769 |
. . . . . . 7
β’ ((πΊ β (π Cn π) β§ π β π) β (β‘πΊ β π ) β π) |
48 | 47 | ad2ant2l 745 |
. . . . . 6
β’ (((πΉ β (π Cn π
) β§ πΊ β (π Cn π)) β§ (π β π
β§ π β π)) β (β‘πΊ β π ) β π) |
49 | | inopn 22401 |
. . . . . 6
β’ ((π β Top β§ (β‘πΉ β π) β π β§ (β‘πΊ β π ) β π) β ((β‘πΉ β π) β© (β‘πΊ β π )) β π) |
50 | 44, 46, 48, 49 | syl3anc 1372 |
. . . . 5
β’ (((πΉ β (π Cn π
) β§ πΊ β (π Cn π)) β§ (π β π
β§ π β π)) β ((β‘πΉ β π) β© (β‘πΊ β π )) β π) |
51 | 41, 50 | eqeltrd 2834 |
. . . 4
β’ (((πΉ β (π Cn π
) β§ πΊ β (π Cn π)) β§ (π β π
β§ π β π)) β (β‘π» β (π Γ π )) β π) |
52 | 51 | ralrimivva 3201 |
. . 3
β’ ((πΉ β (π Cn π
) β§ πΊ β (π Cn π)) β βπ β π
βπ β π (β‘π» β (π Γ π )) β π) |
53 | | vex 3479 |
. . . . . 6
β’ π β V |
54 | | vex 3479 |
. . . . . 6
β’ π β V |
55 | 53, 54 | xpex 7740 |
. . . . 5
β’ (π Γ π ) β V |
56 | 55 | rgen2w 3067 |
. . . 4
β’
βπ β
π
βπ β π (π Γ π ) β V |
57 | | eqid 2733 |
. . . . 5
β’ (π β π
, π β π β¦ (π Γ π )) = (π β π
, π β π β¦ (π Γ π )) |
58 | | imaeq2 6056 |
. . . . . 6
β’ (π§ = (π Γ π ) β (β‘π» β π§) = (β‘π» β (π Γ π ))) |
59 | 58 | eleq1d 2819 |
. . . . 5
β’ (π§ = (π Γ π ) β ((β‘π» β π§) β π β (β‘π» β (π Γ π )) β π)) |
60 | 57, 59 | ralrnmpo 7547 |
. . . 4
β’
(βπ β
π
βπ β π (π Γ π ) β V β (βπ§ β ran (π β π
, π β π β¦ (π Γ π ))(β‘π» β π§) β π β βπ β π
βπ β π (β‘π» β (π Γ π )) β π)) |
61 | 56, 60 | ax-mp 5 |
. . 3
β’
(βπ§ β
ran (π β π
, π β π β¦ (π Γ π ))(β‘π» β π§) β π β βπ β π
βπ β π (β‘π» β (π Γ π )) β π) |
62 | 52, 61 | sylibr 233 |
. 2
β’ ((πΉ β (π Cn π
) β§ πΊ β (π Cn π)) β βπ§ β ran (π β π
, π β π β¦ (π Γ π ))(β‘π» β π§) β π) |
63 | 1 | toptopon 22419 |
. . . 4
β’ (π β Top β π β (TopOnβπ)) |
64 | 43, 63 | sylib 217 |
. . 3
β’ ((πΉ β (π Cn π
) β§ πΊ β (π Cn π)) β π β (TopOnβπ)) |
65 | | cntop2 22745 |
. . . 4
β’ (πΉ β (π Cn π
) β π
β Top) |
66 | | cntop2 22745 |
. . . 4
β’ (πΊ β (π Cn π) β π β Top) |
67 | | eqid 2733 |
. . . . 5
β’ ran
(π β π
, π β π β¦ (π Γ π )) = ran (π β π
, π β π β¦ (π Γ π )) |
68 | 67 | txval 23068 |
. . . 4
β’ ((π
β Top β§ π β Top) β (π
Γt π) = (topGenβran (π β π
, π β π β¦ (π Γ π )))) |
69 | 65, 66, 68 | syl2an 597 |
. . 3
β’ ((πΉ β (π Cn π
) β§ πΊ β (π Cn π)) β (π
Γt π) = (topGenβran (π β π
, π β π β¦ (π Γ π )))) |
70 | | toptopon2 22420 |
. . . . 5
β’ (π
β Top β π
β (TopOnββͺ π
)) |
71 | 65, 70 | sylib 217 |
. . . 4
β’ (πΉ β (π Cn π
) β π
β (TopOnββͺ π
)) |
72 | | toptopon2 22420 |
. . . . 5
β’ (π β Top β π β (TopOnββͺ π)) |
73 | 66, 72 | sylib 217 |
. . . 4
β’ (πΊ β (π Cn π) β π β (TopOnββͺ π)) |
74 | | txtopon 23095 |
. . . 4
β’ ((π
β (TopOnββͺ π
)
β§ π β
(TopOnββͺ π)) β (π
Γt π) β (TopOnβ(βͺ π
Γ βͺ π))) |
75 | 71, 73, 74 | syl2an 597 |
. . 3
β’ ((πΉ β (π Cn π
) β§ πΊ β (π Cn π)) β (π
Γt π) β (TopOnβ(βͺ π
Γ βͺ π))) |
76 | 64, 69, 75 | tgcn 22756 |
. 2
β’ ((πΉ β (π Cn π
) β§ πΊ β (π Cn π)) β (π» β (π Cn (π
Γt π)) β (π»:πβΆ(βͺ π
Γ βͺ π)
β§ βπ§ β ran
(π β π
, π β π β¦ (π Γ π ))(β‘π» β π§) β π))) |
77 | 12, 62, 76 | mpbir2and 712 |
1
β’ ((πΉ β (π Cn π
) β§ πΊ β (π Cn π)) β π» β (π Cn (π
Γt π))) |