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

Metamath Proof Explorer

Theorem en3d

Description: Equinumerosity inference from an implicit one-to-one onto function. (Contributed by NM, 27-Jul-2004) (Revised by Mario Carneiro, 12-May-2014) (Revised by AV, 4-Aug-2024)

Ref Expression
Hypotheses en3d.1 
|- ( ph -> A e. V )
en3d.2 
|- ( ph -> B e. W )
en3d.3 
|- ( ph -> ( x e. A -> C e. B ) )
en3d.4 
|- ( ph -> ( y e. B -> D e. A ) )
en3d.5 
|- ( ph -> ( ( x e. A /\ y e. B ) -> ( x = D <-> y = C ) ) )
Assertion en3d 
|- ( ph -> A ~~ B )

Proof

Step Hyp Ref Expression
1 en3d.1 
 |-  ( ph -> A e. V )
2 en3d.2 
 |-  ( ph -> B e. W )
3 en3d.3 
 |-  ( ph -> ( x e. A -> C e. B ) )
4 en3d.4 
 |-  ( ph -> ( y e. B -> D e. A ) )
5 en3d.5 
 |-  ( ph -> ( ( x e. A /\ y e. B ) -> ( x = D <-> y = C ) ) )
6 eqid 
 |-  ( x e. A |-> C ) = ( x e. A |-> C )
7 3 imp 
 |-  ( ( ph /\ x e. A ) -> C e. B )
8 4 imp 
 |-  ( ( ph /\ y e. B ) -> D e. A )
9 5 imp 
 |-  ( ( ph /\ ( x e. A /\ y e. B ) ) -> ( x = D <-> y = C ) )
10 6 7 8 9 f1o2d 
 |-  ( ph -> ( x e. A |-> C ) : A -1-1-onto-> B )
11 f1oen2g 
 |-  ( ( A e. V /\ B e. W /\ ( x e. A |-> C ) : A -1-1-onto-> B ) -> A ~~ B )
12 1 2 10 11 syl3anc 
 |-  ( ph -> A ~~ B )