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		snex	⊢ { 𝑥 } ∈ 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	syl5req	⊢ ( 𝑑 ∈ ( 𝒫 ( 𝑏 ∪ { 𝑥 } ) ∖ 𝒫 𝑏 ) → 𝑑 = ( ( 𝑑 ∖ { 𝑥 } ) ∪ { 𝑥 } ) )
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 )