Metamath Proof Explorer

Theorem om2noseqf1o

Description: G is a bijection. (Contributed by Scott Fenton, 18-Apr-2025)

Ref Expression
Hypotheses om2noseq.1 
|- ( ph -> C e. No )
om2noseq.2 
|- ( ph -> G = ( rec ( ( x e. _V |-> ( x +s 1s ) ) , C ) |` _om ) )
om2noseq.3 
|- ( ph -> Z = ( rec ( ( x e. _V |-> ( x +s 1s ) ) , C ) " _om ) )
Assertion om2noseqf1o 
|- ( ph -> G : _om -1-1-onto-> Z )

Proof

Step Hyp Ref Expression
1 om2noseq.1 
 |-  ( ph -> C e. No )
2 om2noseq.2 
 |-  ( ph -> G = ( rec ( ( x e. _V |-> ( x +s 1s ) ) , C ) |` _om ) )
3 om2noseq.3 
 |-  ( ph -> Z = ( rec ( ( x e. _V |-> ( x +s 1s ) ) , C ) " _om ) )
4 1 2 3 om2noseqfo 
 |-  ( ph -> G : _om -onto-> Z )
5 fof 
 |-  ( G : _om -onto-> Z -> G : _om --> Z )
6 4 5 syl 
 |-  ( ph -> G : _om --> Z )
7 1 2 3 om2noseqlt 
 |-  ( ( ph /\ ( y e. _om /\ z e. _om ) ) -> ( y e. z -> ( G ` y )
8 1 2 3 om2noseqlt 
 |-  ( ( ph /\ ( z e. _om /\ y e. _om ) ) -> ( z e. y -> ( G ` z )
9 8 ancom2s 
 |-  ( ( ph /\ ( y e. _om /\ z e. _om ) ) -> ( z e. y -> ( G ` z )
10 7 9 orim12d 
 |-  ( ( ph /\ ( y e. _om /\ z e. _om ) ) -> ( ( y e. z \/ z e. y ) -> ( ( G ` y )
11 10 con3d 
 |-  ( ( ph /\ ( y e. _om /\ z e. _om ) ) -> ( -. ( ( G ` y )  -. ( y e. z \/ z e. y ) ) )
12 3 1 noseqssno 
 |-  ( ph -> Z C_ No )
13 6 12 fssd 
 |-  ( ph -> G : _om --> No )
14 13 ffvelcdmda 
 |-  ( ( ph /\ y e. _om ) -> ( G ` y ) e. No )
15 14 adantrr 
 |-  ( ( ph /\ ( y e. _om /\ z e. _om ) ) -> ( G ` y ) e. No )
16 13 ffvelcdmda 
 |-  ( ( ph /\ z e. _om ) -> ( G ` z ) e. No )
17 16 adantrl 
 |-  ( ( ph /\ ( y e. _om /\ z e. _om ) ) -> ( G ` z ) e. No )
18 slttrieq2 
 |-  ( ( ( G ` y ) e. No /\ ( G ` z ) e. No ) -> ( ( G ` y ) = ( G ` z ) <-> ( -. ( G ` y )
19 ioran 
 |-  ( -. ( ( G ` y )  ( -. ( G ` y )
20 18 19 bitr4di 
 |-  ( ( ( G ` y ) e. No /\ ( G ` z ) e. No ) -> ( ( G ` y ) = ( G ` z ) <-> -. ( ( G ` y )
21 15 17 20 syl2anc 
 |-  ( ( ph /\ ( y e. _om /\ z e. _om ) ) -> ( ( G ` y ) = ( G ` z ) <-> -. ( ( G ` y )
22 nnord 
 |-  ( y e. _om -> Ord y )
23 nnord 
 |-  ( z e. _om -> Ord z )
24 ordtri3 
 |-  ( ( Ord y /\ Ord z ) -> ( y = z <-> -. ( y e. z \/ z e. y ) ) )
25 22 23 24 syl2an 
 |-  ( ( y e. _om /\ z e. _om ) -> ( y = z <-> -. ( y e. z \/ z e. y ) ) )
26 25 adantl 
 |-  ( ( ph /\ ( y e. _om /\ z e. _om ) ) -> ( y = z <-> -. ( y e. z \/ z e. y ) ) )
27 11 21 26 3imtr4d 
 |-  ( ( ph /\ ( y e. _om /\ z e. _om ) ) -> ( ( G ` y ) = ( G ` z ) -> y = z ) )
28 27 ralrimivva 
 |-  ( ph -> A. y e. _om A. z e. _om ( ( G ` y ) = ( G ` z ) -> y = z ) )
29 dff13 
 |-  ( G : _om -1-1-> Z <-> ( G : _om --> Z /\ A. y e. _om A. z e. _om ( ( G ` y ) = ( G ` z ) -> y = z ) ) )
30 6 28 29 sylanbrc 
 |-  ( ph -> G : _om -1-1-> Z )
31 df-f1o 
 |-  ( G : _om -1-1-onto-> Z <-> ( G : _om -1-1-> Z /\ G : _om -onto-> Z ) )
32 30 4 31 sylanbrc 
 |-  ( ph -> G : _om -1-1-onto-> Z )