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