Theorem entrfil

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

	Ref	Expression
Assertion	entrfil	⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ≈ 𝐵 ∧ 𝐵 ≈ 𝐶 ) → 𝐴 ≈ 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		bren	⊢ ( 𝐵 ≈ 𝐶 ↔ ∃ 𝑓 𝑓 : 𝐵 –1-1-onto→ 𝐶 )
2		bren	⊢ ( 𝐴 ≈ 𝐵 ↔ ∃ 𝑔 𝑔 : 𝐴 –1-1-onto→ 𝐵 )
3		exdistrv	⊢ ( ∃ 𝑔 ∃ 𝑓 ( 𝑔 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑓 : 𝐵 –1-1-onto→ 𝐶 ) ↔ ( ∃ 𝑔 𝑔 : 𝐴 –1-1-onto→ 𝐵 ∧ ∃ 𝑓 𝑓 : 𝐵 –1-1-onto→ 𝐶 ) )
4		19.42vv	⊢ ( ∃ 𝑔 ∃ 𝑓 ( 𝐴 ∈ Fin ∧ ( 𝑔 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑓 : 𝐵 –1-1-onto→ 𝐶 ) ) ↔ ( 𝐴 ∈ Fin ∧ ∃ 𝑔 ∃ 𝑓 ( 𝑔 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑓 : 𝐵 –1-1-onto→ 𝐶 ) ) )
5		f1oco	⊢ ( ( 𝑓 : 𝐵 –1-1-onto→ 𝐶 ∧ 𝑔 : 𝐴 –1-1-onto→ 𝐵 ) → ( 𝑓 ∘ 𝑔 ) : 𝐴 –1-1-onto→ 𝐶 )
6	5	ancoms	⊢ ( ( 𝑔 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑓 : 𝐵 –1-1-onto→ 𝐶 ) → ( 𝑓 ∘ 𝑔 ) : 𝐴 –1-1-onto→ 𝐶 )
7		f1oenfi	⊢ ( ( 𝐴 ∈ Fin ∧ ( 𝑓 ∘ 𝑔 ) : 𝐴 –1-1-onto→ 𝐶 ) → 𝐴 ≈ 𝐶 )
8	6 7	sylan2	⊢ ( ( 𝐴 ∈ Fin ∧ ( 𝑔 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑓 : 𝐵 –1-1-onto→ 𝐶 ) ) → 𝐴 ≈ 𝐶 )
9	8	exlimivv	⊢ ( ∃ 𝑔 ∃ 𝑓 ( 𝐴 ∈ Fin ∧ ( 𝑔 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑓 : 𝐵 –1-1-onto→ 𝐶 ) ) → 𝐴 ≈ 𝐶 )
10	4 9	sylbir	⊢ ( ( 𝐴 ∈ Fin ∧ ∃ 𝑔 ∃ 𝑓 ( 𝑔 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑓 : 𝐵 –1-1-onto→ 𝐶 ) ) → 𝐴 ≈ 𝐶 )
11	3 10	sylan2br	⊢ ( ( 𝐴 ∈ Fin ∧ ( ∃ 𝑔 𝑔 : 𝐴 –1-1-onto→ 𝐵 ∧ ∃ 𝑓 𝑓 : 𝐵 –1-1-onto→ 𝐶 ) ) → 𝐴 ≈ 𝐶 )
12	11	3impb	⊢ ( ( 𝐴 ∈ Fin ∧ ∃ 𝑔 𝑔 : 𝐴 –1-1-onto→ 𝐵 ∧ ∃ 𝑓 𝑓 : 𝐵 –1-1-onto→ 𝐶 ) → 𝐴 ≈ 𝐶 )
13	2 12	syl3an2b	⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ≈ 𝐵 ∧ ∃ 𝑓 𝑓 : 𝐵 –1-1-onto→ 𝐶 ) → 𝐴 ≈ 𝐶 )
14	1 13	syl3an3b	⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ≈ 𝐵 ∧ 𝐵 ≈ 𝐶 ) → 𝐴 ≈ 𝐶 )