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

Metamath Proof Explorer

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 )