Metamath Proof Explorer

Theorem ptcmplem5

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 ptcmplem5 ( 𝜑 → ( ∏t ‘ 𝐹 ) ∈ Comp )

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 5 elin1d ⊢ ( 𝜑 → 𝑋 ∈ UFL )
7 1 2 3 4 5 ptcmplem1 ⊢ ( 𝜑 → ( 𝑋 = ∪ ( ran 𝑆 ∪ { 𝑋 } ) ∧ ( ∏t ‘ 𝐹 ) = ( topGen ‘ ( fi ‘ ( ran 𝑆 ∪ { 𝑋 } ) ) ) ) )
8 7 simpld ⊢ ( 𝜑 → 𝑋 = ∪ ( ran 𝑆 ∪ { 𝑋 } ) )
9 7 simprd ⊢ ( 𝜑 → ( ∏t ‘ 𝐹 ) = ( topGen ‘ ( fi ‘ ( ran 𝑆 ∪ { 𝑋 } ) ) ) )
10 elpwi ⊢ ( 𝑦 ∈ 𝒫 ran 𝑆 → 𝑦 ⊆ ran 𝑆 )
11 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ ran 𝑆 ∧ 𝑋 = ∪ 𝑦 ) ) ∧ ¬ ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) 𝑋 = ∪ 𝑧 ) → 𝐴 ∈ 𝑉 )
12 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ ran 𝑆 ∧ 𝑋 = ∪ 𝑦 ) ) ∧ ¬ ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) 𝑋 = ∪ 𝑧 ) → 𝐹 : 𝐴 ⟶ Comp )
13 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ ran 𝑆 ∧ 𝑋 = ∪ 𝑦 ) ) ∧ ¬ ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) 𝑋 = ∪ 𝑧 ) → 𝑋 ∈ ( UFL ∩ dom card ) )
14 simplrl ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ ran 𝑆 ∧ 𝑋 = ∪ 𝑦 ) ) ∧ ¬ ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) 𝑋 = ∪ 𝑧 ) → 𝑦 ⊆ ran 𝑆 )
15 simplrr ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ ran 𝑆 ∧ 𝑋 = ∪ 𝑦 ) ) ∧ ¬ ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) 𝑋 = ∪ 𝑧 ) → 𝑋 = ∪ 𝑦 )
16 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ ran 𝑆 ∧ 𝑋 = ∪ 𝑦 ) ) ∧ ¬ ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) 𝑋 = ∪ 𝑧 ) → ¬ ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) 𝑋 = ∪ 𝑧 )
17 imaeq2 ⊢ ( 𝑧 = 𝑢 → ( ◡ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑧 ) = ( ◡ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) )
18 17 eleq1d ⊢ ( 𝑧 = 𝑢 → ( ( ◡ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑧 ) ∈ 𝑦 ↔ ( ◡ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ∈ 𝑦 ) )
19 18 cbvrabv ⊢ { 𝑧 ∈ ( 𝐹 ‘ 𝑘 ) ∣ ( ◡ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑧 ) ∈ 𝑦 } = { 𝑢 ∈ ( 𝐹 ‘ 𝑘 ) ∣ ( ◡ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ∈ 𝑦 }
20 1 2 11 12 13 14 15 16 19 ptcmplem4 ⊢ ¬ ( ( 𝜑 ∧ ( 𝑦 ⊆ ran 𝑆 ∧ 𝑋 = ∪ 𝑦 ) ) ∧ ¬ ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) 𝑋 = ∪ 𝑧 )
21 iman ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ ran 𝑆 ∧ 𝑋 = ∪ 𝑦 ) ) → ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) 𝑋 = ∪ 𝑧 ) ↔ ¬ ( ( 𝜑 ∧ ( 𝑦 ⊆ ran 𝑆 ∧ 𝑋 = ∪ 𝑦 ) ) ∧ ¬ ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) 𝑋 = ∪ 𝑧 ) )
22 20 21 mpbir ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ ran 𝑆 ∧ 𝑋 = ∪ 𝑦 ) ) → ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) 𝑋 = ∪ 𝑧 )
23 22 expr ⊢ ( ( 𝜑 ∧ 𝑦 ⊆ ran 𝑆 ) → ( 𝑋 = ∪ 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) 𝑋 = ∪ 𝑧 ) )
24 10 23 sylan2 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝒫 ran 𝑆 ) → ( 𝑋 = ∪ 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) 𝑋 = ∪ 𝑧 ) )
25 24 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑦 ⊆ ( ran 𝑆 ∪ { 𝑋 } ) ) ∧ 𝑦 ∈ 𝒫 ran 𝑆 ) → ( 𝑋 = ∪ 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) 𝑋 = ∪ 𝑧 ) )
26 velpw ⊢ ( 𝑦 ∈ 𝒫 ( ran 𝑆 ∪ { 𝑋 } ) ↔ 𝑦 ⊆ ( ran 𝑆 ∪ { 𝑋 } ) )
27 eldif ⊢ ( 𝑦 ∈ ( 𝒫 ( ran 𝑆 ∪ { 𝑋 } ) ∖ 𝒫 ran 𝑆 ) ↔ ( 𝑦 ∈ 𝒫 ( ran 𝑆 ∪ { 𝑋 } ) ∧ ¬ 𝑦 ∈ 𝒫 ran 𝑆 ) )
28 elpwunsn ⊢ ( 𝑦 ∈ ( 𝒫 ( ran 𝑆 ∪ { 𝑋 } ) ∖ 𝒫 ran 𝑆 ) → 𝑋 ∈ 𝑦 )
29 27 28 sylbir ⊢ ( ( 𝑦 ∈ 𝒫 ( ran 𝑆 ∪ { 𝑋 } ) ∧ ¬ 𝑦 ∈ 𝒫 ran 𝑆 ) → 𝑋 ∈ 𝑦 )
30 26 29 sylanbr ⊢ ( ( 𝑦 ⊆ ( ran 𝑆 ∪ { 𝑋 } ) ∧ ¬ 𝑦 ∈ 𝒫 ran 𝑆 ) → 𝑋 ∈ 𝑦 )
31 30 adantll ⊢ ( ( ( 𝜑 ∧ 𝑦 ⊆ ( ran 𝑆 ∪ { 𝑋 } ) ) ∧ ¬ 𝑦 ∈ 𝒫 ran 𝑆 ) → 𝑋 ∈ 𝑦 )
32 snssi ⊢ ( 𝑋 ∈ 𝑦 → { 𝑋 } ⊆ 𝑦 )
33 32 adantl ⊢ ( ( ( 𝜑 ∧ 𝑦 ⊆ ( ran 𝑆 ∪ { 𝑋 } ) ) ∧ 𝑋 ∈ 𝑦 ) → { 𝑋 } ⊆ 𝑦 )
34 snfi ⊢ { 𝑋 } ∈ Fin
35 elfpw ⊢ ( { 𝑋 } ∈ ( 𝒫 𝑦 ∩ Fin ) ↔ ( { 𝑋 } ⊆ 𝑦 ∧ { 𝑋 } ∈ Fin ) )
36 33 34 35 sylanblrc ⊢ ( ( ( 𝜑 ∧ 𝑦 ⊆ ( ran 𝑆 ∪ { 𝑋 } ) ) ∧ 𝑋 ∈ 𝑦 ) → { 𝑋 } ∈ ( 𝒫 𝑦 ∩ Fin ) )
37 unisng ⊢ ( 𝑋 ∈ 𝑦 → ∪ { 𝑋 } = 𝑋 )
38 37 eqcomd ⊢ ( 𝑋 ∈ 𝑦 → 𝑋 = ∪ { 𝑋 } )
39 38 adantl ⊢ ( ( ( 𝜑 ∧ 𝑦 ⊆ ( ran 𝑆 ∪ { 𝑋 } ) ) ∧ 𝑋 ∈ 𝑦 ) → 𝑋 = ∪ { 𝑋 } )
40 unieq ⊢ ( 𝑧 = { 𝑋 } → ∪ 𝑧 = ∪ { 𝑋 } )
41 40 rspceeqv ⊢ ( ( { 𝑋 } ∈ ( 𝒫 𝑦 ∩ Fin ) ∧ 𝑋 = ∪ { 𝑋 } ) → ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) 𝑋 = ∪ 𝑧 )
42 36 39 41 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑦 ⊆ ( ran 𝑆 ∪ { 𝑋 } ) ) ∧ 𝑋 ∈ 𝑦 ) → ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) 𝑋 = ∪ 𝑧 )
43 42 a1d ⊢ ( ( ( 𝜑 ∧ 𝑦 ⊆ ( ran 𝑆 ∪ { 𝑋 } ) ) ∧ 𝑋 ∈ 𝑦 ) → ( 𝑋 = ∪ 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) 𝑋 = ∪ 𝑧 ) )
44 31 43 syldan ⊢ ( ( ( 𝜑 ∧ 𝑦 ⊆ ( ran 𝑆 ∪ { 𝑋 } ) ) ∧ ¬ 𝑦 ∈ 𝒫 ran 𝑆 ) → ( 𝑋 = ∪ 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) 𝑋 = ∪ 𝑧 ) )
45 25 44 pm2.61dan ⊢ ( ( 𝜑 ∧ 𝑦 ⊆ ( ran 𝑆 ∪ { 𝑋 } ) ) → ( 𝑋 = ∪ 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) 𝑋 = ∪ 𝑧 ) )
46 45 impr ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ ( ran 𝑆 ∪ { 𝑋 } ) ∧ 𝑋 = ∪ 𝑦 ) ) → ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) 𝑋 = ∪ 𝑧 )
47 6 8 9 46 alexsub ⊢ ( 𝜑 → ( ∏t ‘ 𝐹 ) ∈ Comp )