Metamath Proof Explorer

Theorem pwfilem

Description: Lemma for pwfi . (Contributed by NM, 26-Mar-2007)

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

Proof

Step Hyp Ref Expression
1 pwfilem.1 ⊢ 𝐹 = ( 𝑐 ∈ 𝒫 𝑏 ↦ ( 𝑐 ∪ { 𝑥 } ) )
2 pwundif ⊢ 𝒫 ( 𝑏 ∪ { 𝑥 } ) = ( ( 𝒫 ( 𝑏 ∪ { 𝑥 } ) ∖ 𝒫 𝑏 ) ∪ 𝒫 𝑏 )
3 vex ⊢ 𝑐 ∈ V
4 snex ⊢ { 𝑥 } ∈ V
5 3 4 unex ⊢ ( 𝑐 ∪ { 𝑥 } ) ∈ V
6 5 1 fnmpti ⊢ 𝐹 Fn 𝒫 𝑏
7 dffn4 ⊢ ( 𝐹 Fn 𝒫 𝑏 ↔ 𝐹 : 𝒫 𝑏 –onto→ ran 𝐹 )
8 6 7 mpbi ⊢ 𝐹 : 𝒫 𝑏 –onto→ ran 𝐹
9 fodomfi ⊢ ( ( 𝒫 𝑏 ∈ Fin ∧ 𝐹 : 𝒫 𝑏 –onto→ ran 𝐹 ) → ran 𝐹 ≼ 𝒫 𝑏 )
10 8 9 mpan2 ⊢ ( 𝒫 𝑏 ∈ Fin → ran 𝐹 ≼ 𝒫 𝑏 )
11 domfi ⊢ ( ( 𝒫 𝑏 ∈ Fin ∧ ran 𝐹 ≼ 𝒫 𝑏 ) → ran 𝐹 ∈ Fin )
12 10 11 mpdan ⊢ ( 𝒫 𝑏 ∈ Fin → ran 𝐹 ∈ Fin )
13 eldifi ⊢ ( 𝑑 ∈ ( 𝒫 ( 𝑏 ∪ { 𝑥 } ) ∖ 𝒫 𝑏 ) → 𝑑 ∈ 𝒫 ( 𝑏 ∪ { 𝑥 } ) )
14 4 elpwun ⊢ ( 𝑑 ∈ 𝒫 ( 𝑏 ∪ { 𝑥 } ) ↔ ( 𝑑 ∖ { 𝑥 } ) ∈ 𝒫 𝑏 )
15 13 14 sylib ⊢ ( 𝑑 ∈ ( 𝒫 ( 𝑏 ∪ { 𝑥 } ) ∖ 𝒫 𝑏 ) → ( 𝑑 ∖ { 𝑥 } ) ∈ 𝒫 𝑏 )
16 undif1 ⊢ ( ( 𝑑 ∖ { 𝑥 } ) ∪ { 𝑥 } ) = ( 𝑑 ∪ { 𝑥 } )
17 elpwunsn ⊢ ( 𝑑 ∈ ( 𝒫 ( 𝑏 ∪ { 𝑥 } ) ∖ 𝒫 𝑏 ) → 𝑥 ∈ 𝑑 )
18 17 snssd ⊢ ( 𝑑 ∈ ( 𝒫 ( 𝑏 ∪ { 𝑥 } ) ∖ 𝒫 𝑏 ) → { 𝑥 } ⊆ 𝑑 )
19 ssequn2 ⊢ ( { 𝑥 } ⊆ 𝑑 ↔ ( 𝑑 ∪ { 𝑥 } ) = 𝑑 )
20 18 19 sylib ⊢ ( 𝑑 ∈ ( 𝒫 ( 𝑏 ∪ { 𝑥 } ) ∖ 𝒫 𝑏 ) → ( 𝑑 ∪ { 𝑥 } ) = 𝑑 )
21 16 20 syl5req ⊢ ( 𝑑 ∈ ( 𝒫 ( 𝑏 ∪ { 𝑥 } ) ∖ 𝒫 𝑏 ) → 𝑑 = ( ( 𝑑 ∖ { 𝑥 } ) ∪ { 𝑥 } ) )
22 uneq1 ⊢ ( 𝑐 = ( 𝑑 ∖ { 𝑥 } ) → ( 𝑐 ∪ { 𝑥 } ) = ( ( 𝑑 ∖ { 𝑥 } ) ∪ { 𝑥 } ) )
23 22 rspceeqv ⊢ ( ( ( 𝑑 ∖ { 𝑥 } ) ∈ 𝒫 𝑏 ∧ 𝑑 = ( ( 𝑑 ∖ { 𝑥 } ) ∪ { 𝑥 } ) ) → ∃ 𝑐 ∈ 𝒫 𝑏 𝑑 = ( 𝑐 ∪ { 𝑥 } ) )
24 15 21 23 syl2anc ⊢ ( 𝑑 ∈ ( 𝒫 ( 𝑏 ∪ { 𝑥 } ) ∖ 𝒫 𝑏 ) → ∃ 𝑐 ∈ 𝒫 𝑏 𝑑 = ( 𝑐 ∪ { 𝑥 } ) )
25 1 5 elrnmpti ⊢ ( 𝑑 ∈ ran 𝐹 ↔ ∃ 𝑐 ∈ 𝒫 𝑏 𝑑 = ( 𝑐 ∪ { 𝑥 } ) )
26 24 25 sylibr ⊢ ( 𝑑 ∈ ( 𝒫 ( 𝑏 ∪ { 𝑥 } ) ∖ 𝒫 𝑏 ) → 𝑑 ∈ ran 𝐹 )
27 26 ssriv ⊢ ( 𝒫 ( 𝑏 ∪ { 𝑥 } ) ∖ 𝒫 𝑏 ) ⊆ ran 𝐹
28 ssdomg ⊢ ( ran 𝐹 ∈ Fin → ( ( 𝒫 ( 𝑏 ∪ { 𝑥 } ) ∖ 𝒫 𝑏 ) ⊆ ran 𝐹 → ( 𝒫 ( 𝑏 ∪ { 𝑥 } ) ∖ 𝒫 𝑏 ) ≼ ran 𝐹 ) )
29 12 27 28 mpisyl ⊢ ( 𝒫 𝑏 ∈ Fin → ( 𝒫 ( 𝑏 ∪ { 𝑥 } ) ∖ 𝒫 𝑏 ) ≼ ran 𝐹 )
30 domfi ⊢ ( ( ran 𝐹 ∈ Fin ∧ ( 𝒫 ( 𝑏 ∪ { 𝑥 } ) ∖ 𝒫 𝑏 ) ≼ ran 𝐹 ) → ( 𝒫 ( 𝑏 ∪ { 𝑥 } ) ∖ 𝒫 𝑏 ) ∈ Fin )
31 12 29 30 syl2anc ⊢ ( 𝒫 𝑏 ∈ Fin → ( 𝒫 ( 𝑏 ∪ { 𝑥 } ) ∖ 𝒫 𝑏 ) ∈ Fin )
32 unfi ⊢ ( ( ( 𝒫 ( 𝑏 ∪ { 𝑥 } ) ∖ 𝒫 𝑏 ) ∈ Fin ∧ 𝒫 𝑏 ∈ Fin ) → ( ( 𝒫 ( 𝑏 ∪ { 𝑥 } ) ∖ 𝒫 𝑏 ) ∪ 𝒫 𝑏 ) ∈ Fin )
33 31 32 mpancom ⊢ ( 𝒫 𝑏 ∈ Fin → ( ( 𝒫 ( 𝑏 ∪ { 𝑥 } ) ∖ 𝒫 𝑏 ) ∪ 𝒫 𝑏 ) ∈ Fin )
34 2 33 eqeltrid ⊢ ( 𝒫 𝑏 ∈ Fin → 𝒫 ( 𝑏 ∪ { 𝑥 } ) ∈ Fin )