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

Metamath Proof Explorer

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 ∧ 𝐴 ≈ 𝐵 ∧ 𝐵 ≈ 𝐶 ) → 𝐴 ≈ 𝐶 )