Metamath Proof Explorer


Theorem ptcmplem1

Description: Lemma for ptcmp . (Contributed by Mario Carneiro, 26-Aug-2015)

Ref Expression
Hypotheses ptcmp.1 S = k A , u F k w X w k -1 u
ptcmp.2 X = n A F n
ptcmp.3 φ A V
ptcmp.4 φ F : A Comp
ptcmp.5 φ X UFL dom card
Assertion ptcmplem1 φ X = ran S X 𝑡 F = topGen fi ran S X

Proof

Step Hyp Ref Expression
1 ptcmp.1 S = k A , u F k w X w k -1 u
2 ptcmp.2 X = n A F n
3 ptcmp.3 φ A V
4 ptcmp.4 φ F : A Comp
5 ptcmp.5 φ X UFL dom card
6 4 ffnd φ F Fn A
7 eqid x | g g Fn A y A g y F y z Fin y A z g y = F y x = y A g y = x | g g Fn A y A g y F y z Fin y A z g y = F y x = y A g y
8 7 ptval A V F Fn A 𝑡 F = topGen x | g g Fn A y A g y F y z Fin y A z g y = F y x = y A g y
9 3 6 8 syl2anc φ 𝑡 F = topGen x | g g Fn A y A g y F y z Fin y A z g y = F y x = y A g y
10 cmptop x Comp x Top
11 10 ssriv Comp Top
12 fss F : A Comp Comp Top F : A Top
13 4 11 12 sylancl φ F : A Top
14 7 2 ptbasfi A V F : A Top x | g g Fn A y A g y F y z Fin y A z g y = F y x = y A g y = fi X ran k A , u F k w X w k -1 u
15 3 13 14 syl2anc φ x | g g Fn A y A g y F y z Fin y A z g y = F y x = y A g y = fi X ran k A , u F k w X w k -1 u
16 uncom ran S X = X ran S
17 1 rneqi ran S = ran k A , u F k w X w k -1 u
18 17 uneq2i X ran S = X ran k A , u F k w X w k -1 u
19 16 18 eqtri ran S X = X ran k A , u F k w X w k -1 u
20 19 fveq2i fi ran S X = fi X ran k A , u F k w X w k -1 u
21 15 20 eqtr4di φ x | g g Fn A y A g y F y z Fin y A z g y = F y x = y A g y = fi ran S X
22 21 fveq2d φ topGen x | g g Fn A y A g y F y z Fin y A z g y = F y x = y A g y = topGen fi ran S X
23 9 22 eqtrd φ 𝑡 F = topGen fi ran S X
24 23 unieqd φ 𝑡 F = topGen fi ran S X
25 fibas fi ran S X TopBases
26 unitg fi ran S X TopBases topGen fi ran S X = fi ran S X
27 25 26 ax-mp topGen fi ran S X = fi ran S X
28 24 27 eqtrdi φ 𝑡 F = fi ran S X
29 eqid 𝑡 F = 𝑡 F
30 29 ptuni A V F : A Top n A F n = 𝑡 F
31 3 13 30 syl2anc φ n A F n = 𝑡 F
32 2 31 syl5eq φ X = 𝑡 F
33 5 pwexd φ 𝒫 X V
34 eqid w X w k = w X w k
35 34 mptpreima w X w k -1 u = w X | w k u
36 35 ssrab3 w X w k -1 u X
37 5 adantr φ k A u F k X UFL dom card
38 elpw2g X UFL dom card w X w k -1 u 𝒫 X w X w k -1 u X
39 37 38 syl φ k A u F k w X w k -1 u 𝒫 X w X w k -1 u X
40 36 39 mpbiri φ k A u F k w X w k -1 u 𝒫 X
41 40 ralrimivva φ k A u F k w X w k -1 u 𝒫 X
42 1 fmpox k A u F k w X w k -1 u 𝒫 X S : k A k × F k 𝒫 X
43 41 42 sylib φ S : k A k × F k 𝒫 X
44 43 frnd φ ran S 𝒫 X
45 33 44 ssexd φ ran S V
46 snex X V
47 unexg ran S V X V ran S X V
48 45 46 47 sylancl φ ran S X V
49 fiuni ran S X V ran S X = fi ran S X
50 48 49 syl φ ran S X = fi ran S X
51 28 32 50 3eqtr4d φ X = ran S X
52 51 23 jca φ X = ran S X 𝑡 F = topGen fi ran S X