Metamath Proof Explorer

Theorem ptcmplem1

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

Ref Expression
Hypotheses ptcmp.1 ⊢ 𝑆 = ( 𝑘 ∈ 𝐴 , 𝑢 ∈ ( 𝐹 ‘ 𝑘 ) ↦ ( ◡ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) )
ptcmp.2 ⊢ 𝑋 = X 𝑛 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑛 )
ptcmp.3 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
ptcmp.4 ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ Comp )
ptcmp.5 ⊢ ( 𝜑 → 𝑋 ∈ ( UFL ∩ dom card ) )
Assertion ptcmplem1 ( 𝜑 → ( 𝑋 = ∪ ( ran 𝑆 ∪ { 𝑋 } ) ∧ ( ∏t ‘ 𝐹 ) = ( topGen ‘ ( fi ‘ ( ran 𝑆 ∪ { 𝑋 } ) ) ) ) )

Proof

Step Hyp Ref Expression
1 ptcmp.1 ⊢ 𝑆 = ( 𝑘 ∈ 𝐴 , 𝑢 ∈ ( 𝐹 ‘ 𝑘 ) ↦ ( ◡ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) )
2 ptcmp.2 ⊢ 𝑋 = X 𝑛 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑛 )
3 ptcmp.3 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
4 ptcmp.4 ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ Comp )
5 ptcmp.5 ⊢ ( 𝜑 → 𝑋 ∈ ( UFL ∩ dom card ) )
6 4 ffnd ⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
7 eqid ⊢ { 𝑥 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ∧ 𝑥 = X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ) } = { 𝑥 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ∧ 𝑥 = X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ) }
8 7 ptval ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ) → ( ∏t ‘ 𝐹 ) = ( topGen ‘ { 𝑥 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ∧ 𝑥 = X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ) } ) )
9 3 6 8 syl2anc ⊢ ( 𝜑 → ( ∏t ‘ 𝐹 ) = ( topGen ‘ { 𝑥 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ∧ 𝑥 = X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ) } ) )
10 cmptop ⊢ ( 𝑥 ∈ Comp → 𝑥 ∈ Top )
11 10 ssriv ⊢ Comp ⊆ Top
12 fss ⊢ ( ( 𝐹 : 𝐴 ⟶ Comp ∧ Comp ⊆ Top ) → 𝐹 : 𝐴 ⟶ Top )
13 4 11 12 sylancl ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ Top )
14 7 2 ptbasfi ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ) → { 𝑥 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ∧ 𝑥 = X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ) } = ( fi ‘ ( { 𝑋 } ∪ ran ( 𝑘 ∈ 𝐴 , 𝑢 ∈ ( 𝐹 ‘ 𝑘 ) ↦ ( ◡ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ) ) ) )
15 3 13 14 syl2anc ⊢ ( 𝜑 → { 𝑥 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ∧ 𝑥 = X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ) } = ( fi ‘ ( { 𝑋 } ∪ ran ( 𝑘 ∈ 𝐴 , 𝑢 ∈ ( 𝐹 ‘ 𝑘 ) ↦ ( ◡ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ) ) ) )
16 uncom ⊢ ( ran 𝑆 ∪ { 𝑋 } ) = ( { 𝑋 } ∪ ran 𝑆 )
17 1 rneqi ⊢ ran 𝑆 = ran ( 𝑘 ∈ 𝐴 , 𝑢 ∈ ( 𝐹 ‘ 𝑘 ) ↦ ( ◡ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) )
18 17 uneq2i ⊢ ( { 𝑋 } ∪ ran 𝑆 ) = ( { 𝑋 } ∪ ran ( 𝑘 ∈ 𝐴 , 𝑢 ∈ ( 𝐹 ‘ 𝑘 ) ↦ ( ◡ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ) )
19 16 18 eqtri ⊢ ( ran 𝑆 ∪ { 𝑋 } ) = ( { 𝑋 } ∪ ran ( 𝑘 ∈ 𝐴 , 𝑢 ∈ ( 𝐹 ‘ 𝑘 ) ↦ ( ◡ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ) )
20 19 fveq2i ⊢ ( fi ‘ ( ran 𝑆 ∪ { 𝑋 } ) ) = ( fi ‘ ( { 𝑋 } ∪ ran ( 𝑘 ∈ 𝐴 , 𝑢 ∈ ( 𝐹 ‘ 𝑘 ) ↦ ( ◡ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ) ) )
21 15 20 eqtr4di ⊢ ( 𝜑 → { 𝑥 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ∧ 𝑥 = X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ) } = ( fi ‘ ( ran 𝑆 ∪ { 𝑋 } ) ) )
22 21 fveq2d ⊢ ( 𝜑 → ( topGen ‘ { 𝑥 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ∧ 𝑥 = X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ) } ) = ( topGen ‘ ( fi ‘ ( ran 𝑆 ∪ { 𝑋 } ) ) ) )
23 9 22 eqtrd ⊢ ( 𝜑 → ( ∏t ‘ 𝐹 ) = ( topGen ‘ ( fi ‘ ( ran 𝑆 ∪ { 𝑋 } ) ) ) )
24 23 unieqd ⊢ ( 𝜑 → ∪ ( ∏t ‘ 𝐹 ) = ∪ ( topGen ‘ ( fi ‘ ( ran 𝑆 ∪ { 𝑋 } ) ) ) )
25 fibas ⊢ ( fi ‘ ( ran 𝑆 ∪ { 𝑋 } ) ) ∈ TopBases
26 unitg ⊢ ( ( fi ‘ ( ran 𝑆 ∪ { 𝑋 } ) ) ∈ TopBases → ∪ ( topGen ‘ ( fi ‘ ( ran 𝑆 ∪ { 𝑋 } ) ) ) = ∪ ( fi ‘ ( ran 𝑆 ∪ { 𝑋 } ) ) )
27 25 26 ax-mp ⊢ ∪ ( topGen ‘ ( fi ‘ ( ran 𝑆 ∪ { 𝑋 } ) ) ) = ∪ ( fi ‘ ( ran 𝑆 ∪ { 𝑋 } ) )
28 24 27 eqtrdi ⊢ ( 𝜑 → ∪ ( ∏t ‘ 𝐹 ) = ∪ ( fi ‘ ( ran 𝑆 ∪ { 𝑋 } ) ) )
29 eqid ⊢ ( ∏t ‘ 𝐹 ) = ( ∏t ‘ 𝐹 )
30 29 ptuni ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ) → X 𝑛 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑛 ) = ∪ ( ∏t ‘ 𝐹 ) )
31 3 13 30 syl2anc ⊢ ( 𝜑 → X 𝑛 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑛 ) = ∪ ( ∏t ‘ 𝐹 ) )
32 2 31 syl5eq ⊢ ( 𝜑 → 𝑋 = ∪ ( ∏t ‘ 𝐹 ) )
33 5 pwexd ⊢ ( 𝜑 → 𝒫 𝑋 ∈ V )
34 eqid ⊢ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝑘 ) ) = ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝑘 ) )
35 34 mptpreima ⊢ ( ◡ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) = { 𝑤 ∈ 𝑋 ∣ ( 𝑤 ‘ 𝑘 ) ∈ 𝑢 }
36 35 ssrab3 ⊢ ( ◡ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ⊆ 𝑋
37 5 adantr ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝐴 ∧ 𝑢 ∈ ( 𝐹 ‘ 𝑘 ) ) ) → 𝑋 ∈ ( UFL ∩ dom card ) )
38 elpw2g ⊢ ( 𝑋 ∈ ( UFL ∩ dom card ) → ( ( ◡ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ∈ 𝒫 𝑋 ↔ ( ◡ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ⊆ 𝑋 ) )
39 37 38 syl ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝐴 ∧ 𝑢 ∈ ( 𝐹 ‘ 𝑘 ) ) ) → ( ( ◡ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ∈ 𝒫 𝑋 ↔ ( ◡ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ⊆ 𝑋 ) )
40 36 39 mpbiri ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝐴 ∧ 𝑢 ∈ ( 𝐹 ‘ 𝑘 ) ) ) → ( ◡ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ∈ 𝒫 𝑋 )
41 40 ralrimivva ⊢ ( 𝜑 → ∀ 𝑘 ∈ 𝐴 ∀ 𝑢 ∈ ( 𝐹 ‘ 𝑘 ) ( ◡ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ∈ 𝒫 𝑋 )
42 1 fmpox ⊢ ( ∀ 𝑘 ∈ 𝐴 ∀ 𝑢 ∈ ( 𝐹 ‘ 𝑘 ) ( ◡ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ∈ 𝒫 𝑋 ↔ 𝑆 : ∪ 𝑘 ∈ 𝐴 ( { 𝑘 } × ( 𝐹 ‘ 𝑘 ) ) ⟶ 𝒫 𝑋 )
43 41 42 sylib ⊢ ( 𝜑 → 𝑆 : ∪ 𝑘 ∈ 𝐴 ( { 𝑘 } × ( 𝐹 ‘ 𝑘 ) ) ⟶ 𝒫 𝑋 )
44 43 frnd ⊢ ( 𝜑 → ran 𝑆 ⊆ 𝒫 𝑋 )
45 33 44 ssexd ⊢ ( 𝜑 → ran 𝑆 ∈ V )
46 snex ⊢ { 𝑋 } ∈ V
47 unexg ⊢ ( ( ran 𝑆 ∈ V ∧ { 𝑋 } ∈ V ) → ( ran 𝑆 ∪ { 𝑋 } ) ∈ V )
48 45 46 47 sylancl ⊢ ( 𝜑 → ( ran 𝑆 ∪ { 𝑋 } ) ∈ V )
49 fiuni ⊢ ( ( ran 𝑆 ∪ { 𝑋 } ) ∈ V → ∪ ( ran 𝑆 ∪ { 𝑋 } ) = ∪ ( fi ‘ ( ran 𝑆 ∪ { 𝑋 } ) ) )
50 48 49 syl ⊢ ( 𝜑 → ∪ ( ran 𝑆 ∪ { 𝑋 } ) = ∪ ( fi ‘ ( ran 𝑆 ∪ { 𝑋 } ) ) )
51 28 32 50 3eqtr4d ⊢ ( 𝜑 → 𝑋 = ∪ ( ran 𝑆 ∪ { 𝑋 } ) )
52 51 23 jca ⊢ ( 𝜑 → ( 𝑋 = ∪ ( ran 𝑆 ∪ { 𝑋 } ) ∧ ( ∏t ‘ 𝐹 ) = ( topGen ‘ ( fi ‘ ( ran 𝑆 ∪ { 𝑋 } ) ) ) ) )