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 𝑆 ∪ { 𝑋 } ) ) ) ) )