Step | Hyp | Ref
| Expression |
1 | | fmucnd.1 |
. . . 4
β’ (π β π β (UnifOnβπ)) |
2 | | fmucnd.4 |
. . . 4
β’ (π β πΆ β (CauFiluβπ)) |
3 | | cfilufbas 23776 |
. . . 4
β’ ((π β (UnifOnβπ) β§ πΆ β (CauFiluβπ)) β πΆ β (fBasβπ)) |
4 | 1, 2, 3 | syl2anc 585 |
. . 3
β’ (π β πΆ β (fBasβπ)) |
5 | | fmucnd.2 |
. . . 4
β’ (π β π β (UnifOnβπ)) |
6 | | fmucnd.3 |
. . . 4
β’ (π β πΉ β (π Cnuπ)) |
7 | | isucn 23765 |
. . . . 5
β’ ((π β (UnifOnβπ) β§ π β (UnifOnβπ)) β (πΉ β (π Cnuπ) β (πΉ:πβΆπ β§ βπ£ β π βπ β π βπ₯ β π βπ¦ β π (π₯ππ¦ β (πΉβπ₯)π£(πΉβπ¦))))) |
8 | 7 | simprbda 500 |
. . . 4
β’ (((π β (UnifOnβπ) β§ π β (UnifOnβπ)) β§ πΉ β (π Cnuπ)) β πΉ:πβΆπ) |
9 | 1, 5, 6, 8 | syl21anc 837 |
. . 3
β’ (π β πΉ:πβΆπ) |
10 | 5 | elfvexd 6927 |
. . 3
β’ (π β π β V) |
11 | | fmucnd.5 |
. . . 4
β’ π· = ran (π β πΆ β¦ (πΉ β π)) |
12 | 11 | fbasrn 23370 |
. . 3
β’ ((πΆ β (fBasβπ) β§ πΉ:πβΆπ β§ π β V) β π· β (fBasβπ)) |
13 | 4, 9, 10, 12 | syl3anc 1372 |
. 2
β’ (π β π· β (fBasβπ)) |
14 | | simplr 768 |
. . . . . . . 8
β’ ((((π β§ π£ β π) β§ π β πΆ) β§ (π Γ π) β (β‘(π₯ β π, π¦ β π β¦ β¨(πΉβπ₯), (πΉβπ¦)β©) β π£)) β π β πΆ) |
15 | | eqid 2733 |
. . . . . . . 8
β’ (πΉ β π) = (πΉ β π) |
16 | | imaeq2 6053 |
. . . . . . . . 9
β’ (π = π β (πΉ β π) = (πΉ β π)) |
17 | 16 | rspceeqv 3632 |
. . . . . . . 8
β’ ((π β πΆ β§ (πΉ β π) = (πΉ β π)) β βπ β πΆ (πΉ β π) = (πΉ β π)) |
18 | 14, 15, 17 | sylancl 587 |
. . . . . . 7
β’ ((((π β§ π£ β π) β§ π β πΆ) β§ (π Γ π) β (β‘(π₯ β π, π¦ β π β¦ β¨(πΉβπ₯), (πΉβπ¦)β©) β π£)) β βπ β πΆ (πΉ β π) = (πΉ β π)) |
19 | | imaexg 7901 |
. . . . . . . . 9
β’ (πΉ β (π Cnuπ) β (πΉ β π) β V) |
20 | | eqid 2733 |
. . . . . . . . . 10
β’ (π β πΆ β¦ (πΉ β π)) = (π β πΆ β¦ (πΉ β π)) |
21 | 20 | elrnmpt 5953 |
. . . . . . . . 9
β’ ((πΉ β π) β V β ((πΉ β π) β ran (π β πΆ β¦ (πΉ β π)) β βπ β πΆ (πΉ β π) = (πΉ β π))) |
22 | 6, 19, 21 | 3syl 18 |
. . . . . . . 8
β’ (π β ((πΉ β π) β ran (π β πΆ β¦ (πΉ β π)) β βπ β πΆ (πΉ β π) = (πΉ β π))) |
23 | 22 | ad3antrrr 729 |
. . . . . . 7
β’ ((((π β§ π£ β π) β§ π β πΆ) β§ (π Γ π) β (β‘(π₯ β π, π¦ β π β¦ β¨(πΉβπ₯), (πΉβπ¦)β©) β π£)) β ((πΉ β π) β ran (π β πΆ β¦ (πΉ β π)) β βπ β πΆ (πΉ β π) = (πΉ β π))) |
24 | 18, 23 | mpbird 257 |
. . . . . 6
β’ ((((π β§ π£ β π) β§ π β πΆ) β§ (π Γ π) β (β‘(π₯ β π, π¦ β π β¦ β¨(πΉβπ₯), (πΉβπ¦)β©) β π£)) β (πΉ β π) β ran (π β πΆ β¦ (πΉ β π))) |
25 | | imaeq2 6053 |
. . . . . . . . 9
β’ (π = π β (πΉ β π) = (πΉ β π)) |
26 | 25 | cbvmptv 5260 |
. . . . . . . 8
β’ (π β πΆ β¦ (πΉ β π)) = (π β πΆ β¦ (πΉ β π)) |
27 | 26 | rneqi 5934 |
. . . . . . 7
β’ ran
(π β πΆ β¦ (πΉ β π)) = ran (π β πΆ β¦ (πΉ β π)) |
28 | 11, 27 | eqtri 2761 |
. . . . . 6
β’ π· = ran (π β πΆ β¦ (πΉ β π)) |
29 | 24, 28 | eleqtrrdi 2845 |
. . . . 5
β’ ((((π β§ π£ β π) β§ π β πΆ) β§ (π Γ π) β (β‘(π₯ β π, π¦ β π β¦ β¨(πΉβπ₯), (πΉβπ¦)β©) β π£)) β (πΉ β π) β π·) |
30 | 9 | ffnd 6715 |
. . . . . . . 8
β’ (π β πΉ Fn π) |
31 | 30 | ad3antrrr 729 |
. . . . . . 7
β’ ((((π β§ π£ β π) β§ π β πΆ) β§ (π Γ π) β (β‘(π₯ β π, π¦ β π β¦ β¨(πΉβπ₯), (πΉβπ¦)β©) β π£)) β πΉ Fn π) |
32 | | fbelss 23319 |
. . . . . . . . 9
β’ ((πΆ β (fBasβπ) β§ π β πΆ) β π β π) |
33 | 4, 32 | sylan 581 |
. . . . . . . 8
β’ ((π β§ π β πΆ) β π β π) |
34 | 33 | ad4ant13 750 |
. . . . . . 7
β’ ((((π β§ π£ β π) β§ π β πΆ) β§ (π Γ π) β (β‘(π₯ β π, π¦ β π β¦ β¨(πΉβπ₯), (πΉβπ¦)β©) β π£)) β π β π) |
35 | | fmucndlem 23778 |
. . . . . . 7
β’ ((πΉ Fn π β§ π β π) β ((π₯ β π, π¦ β π β¦ β¨(πΉβπ₯), (πΉβπ¦)β©) β (π Γ π)) = ((πΉ β π) Γ (πΉ β π))) |
36 | 31, 34, 35 | syl2anc 585 |
. . . . . 6
β’ ((((π β§ π£ β π) β§ π β πΆ) β§ (π Γ π) β (β‘(π₯ β π, π¦ β π β¦ β¨(πΉβπ₯), (πΉβπ¦)β©) β π£)) β ((π₯ β π, π¦ β π β¦ β¨(πΉβπ₯), (πΉβπ¦)β©) β (π Γ π)) = ((πΉ β π) Γ (πΉ β π))) |
37 | | eqid 2733 |
. . . . . . . . 9
β’ (π₯ β π, π¦ β π β¦ β¨(πΉβπ₯), (πΉβπ¦)β©) = (π₯ β π, π¦ β π β¦ β¨(πΉβπ₯), (πΉβπ¦)β©) |
38 | 37 | mpofun 7527 |
. . . . . . . 8
β’ Fun
(π₯ β π, π¦ β π β¦ β¨(πΉβπ₯), (πΉβπ¦)β©) |
39 | | funimass2 6628 |
. . . . . . . 8
β’ ((Fun
(π₯ β π, π¦ β π β¦ β¨(πΉβπ₯), (πΉβπ¦)β©) β§ (π Γ π) β (β‘(π₯ β π, π¦ β π β¦ β¨(πΉβπ₯), (πΉβπ¦)β©) β π£)) β ((π₯ β π, π¦ β π β¦ β¨(πΉβπ₯), (πΉβπ¦)β©) β (π Γ π)) β π£) |
40 | 38, 39 | mpan 689 |
. . . . . . 7
β’ ((π Γ π) β (β‘(π₯ β π, π¦ β π β¦ β¨(πΉβπ₯), (πΉβπ¦)β©) β π£) β ((π₯ β π, π¦ β π β¦ β¨(πΉβπ₯), (πΉβπ¦)β©) β (π Γ π)) β π£) |
41 | 40 | adantl 483 |
. . . . . 6
β’ ((((π β§ π£ β π) β§ π β πΆ) β§ (π Γ π) β (β‘(π₯ β π, π¦ β π β¦ β¨(πΉβπ₯), (πΉβπ¦)β©) β π£)) β ((π₯ β π, π¦ β π β¦ β¨(πΉβπ₯), (πΉβπ¦)β©) β (π Γ π)) β π£) |
42 | 36, 41 | eqsstrrd 4020 |
. . . . 5
β’ ((((π β§ π£ β π) β§ π β πΆ) β§ (π Γ π) β (β‘(π₯ β π, π¦ β π β¦ β¨(πΉβπ₯), (πΉβπ¦)β©) β π£)) β ((πΉ β π) Γ (πΉ β π)) β π£) |
43 | | id 22 |
. . . . . . . 8
β’ (π = (πΉ β π) β π = (πΉ β π)) |
44 | 43 | sqxpeqd 5707 |
. . . . . . 7
β’ (π = (πΉ β π) β (π Γ π) = ((πΉ β π) Γ (πΉ β π))) |
45 | 44 | sseq1d 4012 |
. . . . . 6
β’ (π = (πΉ β π) β ((π Γ π) β π£ β ((πΉ β π) Γ (πΉ β π)) β π£)) |
46 | 45 | rspcev 3612 |
. . . . 5
β’ (((πΉ β π) β π· β§ ((πΉ β π) Γ (πΉ β π)) β π£) β βπ β π· (π Γ π) β π£) |
47 | 29, 42, 46 | syl2anc 585 |
. . . 4
β’ ((((π β§ π£ β π) β§ π β πΆ) β§ (π Γ π) β (β‘(π₯ β π, π¦ β π β¦ β¨(πΉβπ₯), (πΉβπ¦)β©) β π£)) β βπ β π· (π Γ π) β π£) |
48 | 1 | adantr 482 |
. . . . 5
β’ ((π β§ π£ β π) β π β (UnifOnβπ)) |
49 | 2 | adantr 482 |
. . . . 5
β’ ((π β§ π£ β π) β πΆ β (CauFiluβπ)) |
50 | 5 | adantr 482 |
. . . . . 6
β’ ((π β§ π£ β π) β π β (UnifOnβπ)) |
51 | 6 | adantr 482 |
. . . . . 6
β’ ((π β§ π£ β π) β πΉ β (π Cnuπ)) |
52 | | simpr 486 |
. . . . . 6
β’ ((π β§ π£ β π) β π£ β π) |
53 | | nfcv 2904 |
. . . . . . 7
β’
β²π β¨(πΉβπ₯), (πΉβπ¦)β© |
54 | | nfcv 2904 |
. . . . . . 7
β’
β²π‘β¨(πΉβπ₯), (πΉβπ¦)β© |
55 | | nfcv 2904 |
. . . . . . 7
β’
β²π₯β¨(πΉβπ ), (πΉβπ‘)β© |
56 | | nfcv 2904 |
. . . . . . 7
β’
β²π¦β¨(πΉβπ ), (πΉβπ‘)β© |
57 | | simpl 484 |
. . . . . . . . 9
β’ ((π₯ = π β§ π¦ = π‘) β π₯ = π ) |
58 | 57 | fveq2d 6892 |
. . . . . . . 8
β’ ((π₯ = π β§ π¦ = π‘) β (πΉβπ₯) = (πΉβπ )) |
59 | | simpr 486 |
. . . . . . . . 9
β’ ((π₯ = π β§ π¦ = π‘) β π¦ = π‘) |
60 | 59 | fveq2d 6892 |
. . . . . . . 8
β’ ((π₯ = π β§ π¦ = π‘) β (πΉβπ¦) = (πΉβπ‘)) |
61 | 58, 60 | opeq12d 4880 |
. . . . . . 7
β’ ((π₯ = π β§ π¦ = π‘) β β¨(πΉβπ₯), (πΉβπ¦)β© = β¨(πΉβπ ), (πΉβπ‘)β©) |
62 | 53, 54, 55, 56, 61 | cbvmpo 7498 |
. . . . . 6
β’ (π₯ β π, π¦ β π β¦ β¨(πΉβπ₯), (πΉβπ¦)β©) = (π β π, π‘ β π β¦ β¨(πΉβπ ), (πΉβπ‘)β©) |
63 | 48, 50, 51, 52, 62 | ucnprima 23769 |
. . . . 5
β’ ((π β§ π£ β π) β (β‘(π₯ β π, π¦ β π β¦ β¨(πΉβπ₯), (πΉβπ¦)β©) β π£) β π) |
64 | | cfiluexsm 23777 |
. . . . 5
β’ ((π β (UnifOnβπ) β§ πΆ β (CauFiluβπ) β§ (β‘(π₯ β π, π¦ β π β¦ β¨(πΉβπ₯), (πΉβπ¦)β©) β π£) β π) β βπ β πΆ (π Γ π) β (β‘(π₯ β π, π¦ β π β¦ β¨(πΉβπ₯), (πΉβπ¦)β©) β π£)) |
65 | 48, 49, 63, 64 | syl3anc 1372 |
. . . 4
β’ ((π β§ π£ β π) β βπ β πΆ (π Γ π) β (β‘(π₯ β π, π¦ β π β¦ β¨(πΉβπ₯), (πΉβπ¦)β©) β π£)) |
66 | 47, 65 | r19.29a 3163 |
. . 3
β’ ((π β§ π£ β π) β βπ β π· (π Γ π) β π£) |
67 | 66 | ralrimiva 3147 |
. 2
β’ (π β βπ£ β π βπ β π· (π Γ π) β π£) |
68 | | iscfilu 23775 |
. . 3
β’ (π β (UnifOnβπ) β (π· β (CauFiluβπ) β (π· β (fBasβπ) β§ βπ£ β π βπ β π· (π Γ π) β π£))) |
69 | 5, 68 | syl 17 |
. 2
β’ (π β (π· β (CauFiluβπ) β (π· β (fBasβπ) β§ βπ£ β π βπ β π· (π Γ π) β π£))) |
70 | 13, 67, 69 | mpbir2and 712 |
1
β’ (π β π· β (CauFiluβπ)) |