This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem pwfilem

Description: Lemma for pwfi . (Contributed by NM, 26-Mar-2007) Avoid ax-pow . (Revised by BTernaryTau, 7-Sep-2024)

Ref Expression
Hypothesis pwfilem.1 ⊢ 𝐹 = ( 𝑐 ∈ 𝒫 𝑏 ↦ ( 𝑐 ∪ { 𝑥 } ) )
Assertion pwfilem ( 𝒫 𝑏 ∈ Fin → 𝒫 ( 𝑏 ∪ { 𝑥 } ) ∈ Fin )

Proof

Step Hyp Ref Expression
1 pwfilem.1 ⊢ 𝐹 = ( 𝑐 ∈ 𝒫 𝑏 ↦ ( 𝑐 ∪ { 𝑥 } ) )
2 pwundif ⊢ 𝒫 ( 𝑏 ∪ { 𝑥 } ) = ( ( 𝒫 ( 𝑏 ∪ { 𝑥 } ) ∖ 𝒫 𝑏 ) ∪ 𝒫 𝑏 )
3 1 funmpt2 ⊢ Fun 𝐹
4 vex ⊢ 𝑐 ∈ V
5 vsnex ⊢ { 𝑥 } ∈ V
6 4 5 unex ⊢ ( 𝑐 ∪ { 𝑥 } ) ∈ V
7 6 1 dmmpti ⊢ dom 𝐹 = 𝒫 𝑏
8 7 imaeq2i ⊢ ( 𝐹 “ dom 𝐹 ) = ( 𝐹 “ 𝒫 𝑏 )
9 imadmrn ⊢ ( 𝐹 “ dom 𝐹 ) = ran 𝐹
10 8 9 eqtr3i ⊢ ( 𝐹 “ 𝒫 𝑏 ) = ran 𝐹
11 imafi ⊢ ( ( Fun 𝐹 ∧ 𝒫 𝑏 ∈ Fin ) → ( 𝐹 “ 𝒫 𝑏 ) ∈ Fin )
12 10 11 eqeltrrid ⊢ ( ( Fun 𝐹 ∧ 𝒫 𝑏 ∈ Fin ) → ran 𝐹 ∈ Fin )
13 3 12 mpan ⊢ ( 𝒫 𝑏 ∈ Fin → ran 𝐹 ∈ Fin )
14 eldifi ⊢ ( 𝑑 ∈ ( 𝒫 ( 𝑏 ∪ { 𝑥 } ) ∖ 𝒫 𝑏 ) → 𝑑 ∈ 𝒫 ( 𝑏 ∪ { 𝑥 } ) )
15 5 elpwun ⊢ ( 𝑑 ∈ 𝒫 ( 𝑏 ∪ { 𝑥 } ) ↔ ( 𝑑 ∖ { 𝑥 } ) ∈ 𝒫 𝑏 )
16 14 15 sylib ⊢ ( 𝑑 ∈ ( 𝒫 ( 𝑏 ∪ { 𝑥 } ) ∖ 𝒫 𝑏 ) → ( 𝑑 ∖ { 𝑥 } ) ∈ 𝒫 𝑏 )
17 undif1 ⊢ ( ( 𝑑 ∖ { 𝑥 } ) ∪ { 𝑥 } ) = ( 𝑑 ∪ { 𝑥 } )
18 elpwunsn ⊢ ( 𝑑 ∈ ( 𝒫 ( 𝑏 ∪ { 𝑥 } ) ∖ 𝒫 𝑏 ) → 𝑥 ∈ 𝑑 )
19 18 snssd ⊢ ( 𝑑 ∈ ( 𝒫 ( 𝑏 ∪ { 𝑥 } ) ∖ 𝒫 𝑏 ) → { 𝑥 } ⊆ 𝑑 )
20 ssequn2 ⊢ ( { 𝑥 } ⊆ 𝑑 ↔ ( 𝑑 ∪ { 𝑥 } ) = 𝑑 )
21 19 20 sylib ⊢ ( 𝑑 ∈ ( 𝒫 ( 𝑏 ∪ { 𝑥 } ) ∖ 𝒫 𝑏 ) → ( 𝑑 ∪ { 𝑥 } ) = 𝑑 )
22 17 21 eqtr2id ⊢ ( 𝑑 ∈ ( 𝒫 ( 𝑏 ∪ { 𝑥 } ) ∖ 𝒫 𝑏 ) → 𝑑 = ( ( 𝑑 ∖ { 𝑥 } ) ∪ { 𝑥 } ) )
23 uneq1 ⊢ ( 𝑐 = ( 𝑑 ∖ { 𝑥 } ) → ( 𝑐 ∪ { 𝑥 } ) = ( ( 𝑑 ∖ { 𝑥 } ) ∪ { 𝑥 } ) )
24 23 rspceeqv ⊢ ( ( ( 𝑑 ∖ { 𝑥 } ) ∈ 𝒫 𝑏 ∧ 𝑑 = ( ( 𝑑 ∖ { 𝑥 } ) ∪ { 𝑥 } ) ) → ∃ 𝑐 ∈ 𝒫 𝑏 𝑑 = ( 𝑐 ∪ { 𝑥 } ) )
25 16 22 24 syl2anc ⊢ ( 𝑑 ∈ ( 𝒫 ( 𝑏 ∪ { 𝑥 } ) ∖ 𝒫 𝑏 ) → ∃ 𝑐 ∈ 𝒫 𝑏 𝑑 = ( 𝑐 ∪ { 𝑥 } ) )
26 1 25 14 elrnmptd ⊢ ( 𝑑 ∈ ( 𝒫 ( 𝑏 ∪ { 𝑥 } ) ∖ 𝒫 𝑏 ) → 𝑑 ∈ ran 𝐹 )
27 26 ssriv ⊢ ( 𝒫 ( 𝑏 ∪ { 𝑥 } ) ∖ 𝒫 𝑏 ) ⊆ ran 𝐹
28 ssfi ⊢ ( ( ran 𝐹 ∈ Fin ∧ ( 𝒫 ( 𝑏 ∪ { 𝑥 } ) ∖ 𝒫 𝑏 ) ⊆ ran 𝐹 ) → ( 𝒫 ( 𝑏 ∪ { 𝑥 } ) ∖ 𝒫 𝑏 ) ∈ Fin )
29 13 27 28 sylancl ⊢ ( 𝒫 𝑏 ∈ Fin → ( 𝒫 ( 𝑏 ∪ { 𝑥 } ) ∖ 𝒫 𝑏 ) ∈ Fin )
30 unfi ⊢ ( ( ( 𝒫 ( 𝑏 ∪ { 𝑥 } ) ∖ 𝒫 𝑏 ) ∈ Fin ∧ 𝒫 𝑏 ∈ Fin ) → ( ( 𝒫 ( 𝑏 ∪ { 𝑥 } ) ∖ 𝒫 𝑏 ) ∪ 𝒫 𝑏 ) ∈ Fin )
31 29 30 mpancom ⊢ ( 𝒫 𝑏 ∈ Fin → ( ( 𝒫 ( 𝑏 ∪ { 𝑥 } ) ∖ 𝒫 𝑏 ) ∪ 𝒫 𝑏 ) ∈ Fin )
32 2 31 eqeltrid ⊢ ( 𝒫 𝑏 ∈ Fin → 𝒫 ( 𝑏 ∪ { 𝑥 } ) ∈ Fin )