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 → ( 𝐴 ≈ 𝐵 ↔ 𝐵 ≈ 𝐴 ) )