Metamath Proof Explorer

Theorem om2noseqlt2

Description: The mapping G preserves order. (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 om2noseqlt2 
|- ( ( ph /\ ( A e. _om /\ B e. _om ) ) -> ( A e. B <-> ( G ` A )

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 om2noseqlt 
 |-  ( ( ph /\ ( A e. _om /\ B e. _om ) ) -> ( A e. B -> ( G ` A )
5 1 2 3 om2noseqlt 
 |-  ( ( ph /\ ( B e. _om /\ A e. _om ) ) -> ( B e. A -> ( G ` B )
6 5 ancom2s 
 |-  ( ( ph /\ ( A e. _om /\ B e. _om ) ) -> ( B e. A -> ( G ` B )
7 fveq2 
 |-  ( B = A -> ( G ` B ) = ( G ` A ) )
8 7 a1i 
 |-  ( ( ph /\ ( A e. _om /\ B e. _om ) ) -> ( B = A -> ( G ` B ) = ( G ` A ) ) )
9 6 8 orim12d 
 |-  ( ( ph /\ ( A e. _om /\ B e. _om ) ) -> ( ( B e. A \/ B = A ) -> ( ( G ` B )
10 nnon 
 |-  ( B e. _om -> B e. On )
11 nnon 
 |-  ( A e. _om -> A e. On )
12 onsseleq 
 |-  ( ( B e. On /\ A e. On ) -> ( B C_ A <-> ( B e. A \/ B = A ) ) )
13 ontri1 
 |-  ( ( B e. On /\ A e. On ) -> ( B C_ A <-> -. A e. B ) )
14 12 13 bitr3d 
 |-  ( ( B e. On /\ A e. On ) -> ( ( B e. A \/ B = A ) <-> -. A e. B ) )
15 10 11 14 syl2anr 
 |-  ( ( A e. _om /\ B e. _om ) -> ( ( B e. A \/ B = A ) <-> -. A e. B ) )
16 15 adantl 
 |-  ( ( ph /\ ( A e. _om /\ B e. _om ) ) -> ( ( B e. A \/ B = A ) <-> -. A e. B ) )
17 1 2 3 om2noseqfo 
 |-  ( ph -> G : _om -onto-> Z )
18 fof 
 |-  ( G : _om -onto-> Z -> G : _om --> Z )
19 17 18 syl 
 |-  ( ph -> G : _om --> Z )
20 3 1 noseqssno 
 |-  ( ph -> Z C_ No )
21 19 20 fssd 
 |-  ( ph -> G : _om --> No )
22 21 ffvelcdmda 
 |-  ( ( ph /\ B e. _om ) -> ( G ` B ) e. No )
23 22 adantrl 
 |-  ( ( ph /\ ( A e. _om /\ B e. _om ) ) -> ( G ` B ) e. No )
24 21 ffvelcdmda 
 |-  ( ( ph /\ A e. _om ) -> ( G ` A ) e. No )
25 24 adantrr 
 |-  ( ( ph /\ ( A e. _om /\ B e. _om ) ) -> ( G ` A ) e. No )
26 sleloe 
 |-  ( ( ( G ` B ) e. No /\ ( G ` A ) e. No ) -> ( ( G ` B ) <_s ( G ` A ) <-> ( ( G ` B )
27 slenlt 
 |-  ( ( ( G ` B ) e. No /\ ( G ` A ) e. No ) -> ( ( G ` B ) <_s ( G ` A ) <-> -. ( G ` A )
28 26 27 bitr3d 
 |-  ( ( ( G ` B ) e. No /\ ( G ` A ) e. No ) -> ( ( ( G ` B )  -. ( G ` A )
29 23 25 28 syl2anc 
 |-  ( ( ph /\ ( A e. _om /\ B e. _om ) ) -> ( ( ( G ` B )  -. ( G ` A )
30 9 16 29 3imtr3d 
 |-  ( ( ph /\ ( A e. _om /\ B e. _om ) ) -> ( -. A e. B -> -. ( G ` A )
31 4 30 impcon4bid 
 |-  ( ( ph /\ ( A e. _om /\ B e. _om ) ) -> ( A e. B <-> ( G ` A )