Step | Hyp | Ref
| Expression |
1 | | cfilufbas 23657 |
. . 3
β’ ((π β (UnifOnβπ) β§ πΉ β (CauFiluβπ)) β πΉ β (fBasβπ)) |
2 | | fgcl 23245 |
. . 3
β’ (πΉ β (fBasβπ) β (πfilGenπΉ) β (Filβπ)) |
3 | | filfbas 23215 |
. . 3
β’ ((πfilGenπΉ) β (Filβπ) β (πfilGenπΉ) β (fBasβπ)) |
4 | 1, 2, 3 | 3syl 18 |
. 2
β’ ((π β (UnifOnβπ) β§ πΉ β (CauFiluβπ)) β (πfilGenπΉ) β (fBasβπ)) |
5 | 1 | ad3antrrr 729 |
. . . . . . 7
β’
(((((π β
(UnifOnβπ) β§
πΉ β
(CauFiluβπ)) β§ π£ β π) β§ π β πΉ) β§ (π Γ π) β π£) β πΉ β (fBasβπ)) |
6 | | ssfg 23239 |
. . . . . . 7
β’ (πΉ β (fBasβπ) β πΉ β (πfilGenπΉ)) |
7 | 5, 6 | syl 17 |
. . . . . 6
β’
(((((π β
(UnifOnβπ) β§
πΉ β
(CauFiluβπ)) β§ π£ β π) β§ π β πΉ) β§ (π Γ π) β π£) β πΉ β (πfilGenπΉ)) |
8 | | simplr 768 |
. . . . . 6
β’
(((((π β
(UnifOnβπ) β§
πΉ β
(CauFiluβπ)) β§ π£ β π) β§ π β πΉ) β§ (π Γ π) β π£) β π β πΉ) |
9 | 7, 8 | sseldd 3950 |
. . . . 5
β’
(((((π β
(UnifOnβπ) β§
πΉ β
(CauFiluβπ)) β§ π£ β π) β§ π β πΉ) β§ (π Γ π) β π£) β π β (πfilGenπΉ)) |
10 | | id 22 |
. . . . . . . 8
β’ (π = π β π = π) |
11 | 10 | sqxpeqd 5670 |
. . . . . . 7
β’ (π = π β (π Γ π) = (π Γ π)) |
12 | 11 | sseq1d 3980 |
. . . . . 6
β’ (π = π β ((π Γ π) β π£ β (π Γ π) β π£)) |
13 | 12 | rspcev 3584 |
. . . . 5
β’ ((π β (πfilGenπΉ) β§ (π Γ π) β π£) β βπ β (πfilGenπΉ)(π Γ π) β π£) |
14 | 9, 13 | sylancom 589 |
. . . 4
β’
(((((π β
(UnifOnβπ) β§
πΉ β
(CauFiluβπ)) β§ π£ β π) β§ π β πΉ) β§ (π Γ π) β π£) β βπ β (πfilGenπΉ)(π Γ π) β π£) |
15 | | iscfilu 23656 |
. . . . . 6
β’ (π β (UnifOnβπ) β (πΉ β (CauFiluβπ) β (πΉ β (fBasβπ) β§ βπ£ β π βπ β πΉ (π Γ π) β π£))) |
16 | 15 | simplbda 501 |
. . . . 5
β’ ((π β (UnifOnβπ) β§ πΉ β (CauFiluβπ)) β βπ£ β π βπ β πΉ (π Γ π) β π£) |
17 | 16 | r19.21bi 3237 |
. . . 4
β’ (((π β (UnifOnβπ) β§ πΉ β (CauFiluβπ)) β§ π£ β π) β βπ β πΉ (π Γ π) β π£) |
18 | 14, 17 | r19.29a 3160 |
. . 3
β’ (((π β (UnifOnβπ) β§ πΉ β (CauFiluβπ)) β§ π£ β π) β βπ β (πfilGenπΉ)(π Γ π) β π£) |
19 | 18 | ralrimiva 3144 |
. 2
β’ ((π β (UnifOnβπ) β§ πΉ β (CauFiluβπ)) β βπ£ β π βπ β (πfilGenπΉ)(π Γ π) β π£) |
20 | | iscfilu 23656 |
. . 3
β’ (π β (UnifOnβπ) β ((πfilGenπΉ) β (CauFiluβπ) β ((πfilGenπΉ) β (fBasβπ) β§ βπ£ β π βπ β (πfilGenπΉ)(π Γ π) β π£))) |
21 | 20 | adantr 482 |
. 2
β’ ((π β (UnifOnβπ) β§ πΉ β (CauFiluβπ)) β ((πfilGenπΉ) β (CauFiluβπ) β ((πfilGenπΉ) β (fBasβπ) β§ βπ£ β π βπ β (πfilGenπΉ)(π Γ π) β π£))) |
22 | 4, 19, 21 | mpbir2and 712 |
1
β’ ((π β (UnifOnβπ) β§ πΉ β (CauFiluβπ)) β (πfilGenπΉ) β (CauFiluβπ)) |