Theorem pwfir

Description: If the power set of a set is finite, then the set itself is finite. (Contributed by BTernaryTau, 7-Sep-2024)

	Ref	Expression
Assertion	pwfir	⊢ ( 𝒫 𝐵 ∈ Fin → 𝐵 ∈ Fin )

Proof

Step	Hyp	Ref	Expression
1		df-ima	⊢ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝒫 𝐵 ∧ { 𝑦 } = 𝑥 ) } “ 𝒫 𝐵 ) = ran ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝒫 𝐵 ∧ { 𝑦 } = 𝑥 ) } ↾ 𝒫 𝐵 )
2		relopab	⊢ Rel { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝒫 𝐵 ∧ { 𝑦 } = 𝑥 ) }
3		dmopabss	⊢ dom { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝒫 𝐵 ∧ { 𝑦 } = 𝑥 ) } ⊆ 𝒫 𝐵
4		relssres	⊢ ( ( Rel { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝒫 𝐵 ∧ { 𝑦 } = 𝑥 ) } ∧ dom { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝒫 𝐵 ∧ { 𝑦 } = 𝑥 ) } ⊆ 𝒫 𝐵 ) → ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝒫 𝐵 ∧ { 𝑦 } = 𝑥 ) } ↾ 𝒫 𝐵 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝒫 𝐵 ∧ { 𝑦 } = 𝑥 ) } )
5	2 3 4	mp2an	⊢ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝒫 𝐵 ∧ { 𝑦 } = 𝑥 ) } ↾ 𝒫 𝐵 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝒫 𝐵 ∧ { 𝑦 } = 𝑥 ) }
6	5	rneqi	⊢ ran ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝒫 𝐵 ∧ { 𝑦 } = 𝑥 ) } ↾ 𝒫 𝐵 ) = ran { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝒫 𝐵 ∧ { 𝑦 } = 𝑥 ) }
7		rnopab	⊢ ran { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝒫 𝐵 ∧ { 𝑦 } = 𝑥 ) } = { 𝑦 ∣ ∃ 𝑥 ( 𝑥 ∈ 𝒫 𝐵 ∧ { 𝑦 } = 𝑥 ) }
8		eleq1	⊢ ( { 𝑦 } = 𝑥 → ( { 𝑦 } ∈ 𝒫 𝐵 ↔ 𝑥 ∈ 𝒫 𝐵 ) )
9	8	biimparc	⊢ ( ( 𝑥 ∈ 𝒫 𝐵 ∧ { 𝑦 } = 𝑥 ) → { 𝑦 } ∈ 𝒫 𝐵 )
10		vex	⊢ 𝑦 ∈ V
11	10	snelpw	⊢ ( 𝑦 ∈ 𝐵 ↔ { 𝑦 } ∈ 𝒫 𝐵 )
12	9 11	sylibr	⊢ ( ( 𝑥 ∈ 𝒫 𝐵 ∧ { 𝑦 } = 𝑥 ) → 𝑦 ∈ 𝐵 )
13	12	exlimiv	⊢ ( ∃ 𝑥 ( 𝑥 ∈ 𝒫 𝐵 ∧ { 𝑦 } = 𝑥 ) → 𝑦 ∈ 𝐵 )
14		snelpwi	⊢ ( 𝑦 ∈ 𝐵 → { 𝑦 } ∈ 𝒫 𝐵 )
15		eqid	⊢ { 𝑦 } = { 𝑦 }
16		eqeq2	⊢ ( 𝑥 = { 𝑦 } → ( { 𝑦 } = 𝑥 ↔ { 𝑦 } = { 𝑦 } ) )
17	16	rspcev	⊢ ( ( { 𝑦 } ∈ 𝒫 𝐵 ∧ { 𝑦 } = { 𝑦 } ) → ∃ 𝑥 ∈ 𝒫 𝐵 { 𝑦 } = 𝑥 )
18	14 15 17	sylancl	⊢ ( 𝑦 ∈ 𝐵 → ∃ 𝑥 ∈ 𝒫 𝐵 { 𝑦 } = 𝑥 )
19		df-rex	⊢ ( ∃ 𝑥 ∈ 𝒫 𝐵 { 𝑦 } = 𝑥 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝒫 𝐵 ∧ { 𝑦 } = 𝑥 ) )
20	18 19	sylib	⊢ ( 𝑦 ∈ 𝐵 → ∃ 𝑥 ( 𝑥 ∈ 𝒫 𝐵 ∧ { 𝑦 } = 𝑥 ) )
21	13 20	impbii	⊢ ( ∃ 𝑥 ( 𝑥 ∈ 𝒫 𝐵 ∧ { 𝑦 } = 𝑥 ) ↔ 𝑦 ∈ 𝐵 )
22	21	abbii	⊢ { 𝑦 ∣ ∃ 𝑥 ( 𝑥 ∈ 𝒫 𝐵 ∧ { 𝑦 } = 𝑥 ) } = { 𝑦 ∣ 𝑦 ∈ 𝐵 }
23		abid2	⊢ { 𝑦 ∣ 𝑦 ∈ 𝐵 } = 𝐵
24	7 22 23	3eqtri	⊢ ran { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝒫 𝐵 ∧ { 𝑦 } = 𝑥 ) } = 𝐵
25	1 6 24	3eqtri	⊢ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝒫 𝐵 ∧ { 𝑦 } = 𝑥 ) } “ 𝒫 𝐵 ) = 𝐵
26		funopab	⊢ ( Fun { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝒫 𝐵 ∧ { 𝑦 } = 𝑥 ) } ↔ ∀ 𝑥 ∃* 𝑦 ( 𝑥 ∈ 𝒫 𝐵 ∧ { 𝑦 } = 𝑥 ) )
27		mosneq	⊢ ∃* 𝑦 { 𝑦 } = 𝑥
28	27	moani	⊢ ∃* 𝑦 ( 𝑥 ∈ 𝒫 𝐵 ∧ { 𝑦 } = 𝑥 )
29	26 28	mpgbir	⊢ Fun { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝒫 𝐵 ∧ { 𝑦 } = 𝑥 ) }
30		imafi	⊢ ( ( Fun { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝒫 𝐵 ∧ { 𝑦 } = 𝑥 ) } ∧ 𝒫 𝐵 ∈ Fin ) → ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝒫 𝐵 ∧ { 𝑦 } = 𝑥 ) } “ 𝒫 𝐵 ) ∈ Fin )
31	29 30	mpan	⊢ ( 𝒫 𝐵 ∈ Fin → ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝒫 𝐵 ∧ { 𝑦 } = 𝑥 ) } “ 𝒫 𝐵 ) ∈ Fin )
32	25 31	eqeltrrid	⊢ ( 𝒫 𝐵 ∈ Fin → 𝐵 ∈ Fin )