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

Metamath Proof Explorer

Theorem ensymfib

Description: Symmetry of equinumerosity for finite sets, proved without using the Axiom of Power Sets (unlike ensymb ). (Contributed by BTernaryTau, 9-Sep-2024)

Ref Expression
Assertion ensymfib ( 𝐴 ∈ Fin → ( 𝐴 ≈ 𝐵 ↔ 𝐵 ≈ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 bren ⊢ ( 𝐴 ≈ 𝐵 ↔ ∃ 𝑓 𝑓 : 𝐴 –1-1-onto→ 𝐵 )
2 19.42v ⊢ ( ∃ 𝑓 ( 𝐴 ∈ Fin ∧ 𝑓 : 𝐴 –1-1-onto→ 𝐵 ) ↔ ( 𝐴 ∈ Fin ∧ ∃ 𝑓 𝑓 : 𝐴 –1-1-onto→ 𝐵 ) )
3 f1ocnv ⊢ ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 → ◡ 𝑓 : 𝐵 –1-1-onto→ 𝐴 )
4 f1oenfirn ⊢ ( ( 𝐴 ∈ Fin ∧ ◡ 𝑓 : 𝐵 –1-1-onto→ 𝐴 ) → 𝐵 ≈ 𝐴 )
5 3 4 sylan2 ⊢ ( ( 𝐴 ∈ Fin ∧ 𝑓 : 𝐴 –1-1-onto→ 𝐵 ) → 𝐵 ≈ 𝐴 )
6 5 exlimiv ⊢ ( ∃ 𝑓 ( 𝐴 ∈ Fin ∧ 𝑓 : 𝐴 –1-1-onto→ 𝐵 ) → 𝐵 ≈ 𝐴 )
7 2 6 sylbir ⊢ ( ( 𝐴 ∈ Fin ∧ ∃ 𝑓 𝑓 : 𝐴 –1-1-onto→ 𝐵 ) → 𝐵 ≈ 𝐴 )
8 1 7 sylan2b ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ≈ 𝐵 ) → 𝐵 ≈ 𝐴 )
9 bren ⊢ ( 𝐵 ≈ 𝐴 ↔ ∃ 𝑔 𝑔 : 𝐵 –1-1-onto→ 𝐴 )
10 19.42v ⊢ ( ∃ 𝑔 ( 𝐴 ∈ Fin ∧ 𝑔 : 𝐵 –1-1-onto→ 𝐴 ) ↔ ( 𝐴 ∈ Fin ∧ ∃ 𝑔 𝑔 : 𝐵 –1-1-onto→ 𝐴 ) )
11 f1ocnv ⊢ ( 𝑔 : 𝐵 –1-1-onto→ 𝐴 → ◡ 𝑔 : 𝐴 –1-1-onto→ 𝐵 )
12 f1oenfi ⊢ ( ( 𝐴 ∈ Fin ∧ ◡ 𝑔 : 𝐴 –1-1-onto→ 𝐵 ) → 𝐴 ≈ 𝐵 )
13 11 12 sylan2 ⊢ ( ( 𝐴 ∈ Fin ∧ 𝑔 : 𝐵 –1-1-onto→ 𝐴 ) → 𝐴 ≈ 𝐵 )
14 13 exlimiv ⊢ ( ∃ 𝑔 ( 𝐴 ∈ Fin ∧ 𝑔 : 𝐵 –1-1-onto→ 𝐴 ) → 𝐴 ≈ 𝐵 )
15 10 14 sylbir ⊢ ( ( 𝐴 ∈ Fin ∧ ∃ 𝑔 𝑔 : 𝐵 –1-1-onto→ 𝐴 ) → 𝐴 ≈ 𝐵 )
16 9 15 sylan2b ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ≈ 𝐴 ) → 𝐴 ≈ 𝐵 )
17 8 16 impbida ⊢ ( 𝐴 ∈ Fin → ( 𝐴 ≈ 𝐵 ↔ 𝐵 ≈ 𝐴 ) )