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 
|- ( ( A e. Fin /\ A ~~ B /\ B ~~ C ) -> A ~~ C )

Proof

Step Hyp Ref Expression
1 bren 
 |-  ( B ~~ C <-> E. f f : B -1-1-onto-> C )
2 bren 
 |-  ( A ~~ B <-> E. g g : A -1-1-onto-> B )
3 exdistrv 
 |-  ( E. g E. f ( g : A -1-1-onto-> B /\ f : B -1-1-onto-> C ) <-> ( E. g g : A -1-1-onto-> B /\ E. f f : B -1-1-onto-> C ) )
4 19.42vv 
 |-  ( E. g E. f ( A e. Fin /\ ( g : A -1-1-onto-> B /\ f : B -1-1-onto-> C ) ) <-> ( A e. Fin /\ E. g E. f ( g : A -1-1-onto-> B /\ f : B -1-1-onto-> C ) ) )
5 f1oco 
 |-  ( ( f : B -1-1-onto-> C /\ g : A -1-1-onto-> B ) -> ( f o. g ) : A -1-1-onto-> C )
6 5 ancoms 
 |-  ( ( g : A -1-1-onto-> B /\ f : B -1-1-onto-> C ) -> ( f o. g ) : A -1-1-onto-> C )
7 f1oenfi 
 |-  ( ( A e. Fin /\ ( f o. g ) : A -1-1-onto-> C ) -> A ~~ C )
8 6 7 sylan2 
 |-  ( ( A e. Fin /\ ( g : A -1-1-onto-> B /\ f : B -1-1-onto-> C ) ) -> A ~~ C )
9 8 exlimivv 
 |-  ( E. g E. f ( A e. Fin /\ ( g : A -1-1-onto-> B /\ f : B -1-1-onto-> C ) ) -> A ~~ C )
10 4 9 sylbir 
 |-  ( ( A e. Fin /\ E. g E. f ( g : A -1-1-onto-> B /\ f : B -1-1-onto-> C ) ) -> A ~~ C )
11 3 10 sylan2br 
 |-  ( ( A e. Fin /\ ( E. g g : A -1-1-onto-> B /\ E. f f : B -1-1-onto-> C ) ) -> A ~~ C )
12 11 3impb 
 |-  ( ( A e. Fin /\ E. g g : A -1-1-onto-> B /\ E. f f : B -1-1-onto-> C ) -> A ~~ C )
13 2 12 syl3an2b 
 |-  ( ( A e. Fin /\ A ~~ B /\ E. f f : B -1-1-onto-> C ) -> A ~~ C )
14 1 13 syl3an3b 
 |-  ( ( A e. Fin /\ A ~~ B /\ B ~~ C ) -> A ~~ C )