Metamath Proof Explorer

Theorem nosepon

Description: Given two unequal surreals, the minimal ordinal at which they differ is an ordinal. (Contributed by Scott Fenton, 21-Sep-2020)

Ref Expression
Assertion nosepon 
|- ( ( A e. No /\ B e. No /\ A =/= B ) -> |^| { x e. On | ( A ` x ) =/= ( B ` x ) } e. On )

Proof

Step Hyp Ref Expression
1 df-ne 
 |-  ( ( A ` x ) =/= ( B ` x ) <-> -. ( A ` x ) = ( B ` x ) )
2 1 rexbii 
 |-  ( E. x e. On ( A ` x ) =/= ( B ` x ) <-> E. x e. On -. ( A ` x ) = ( B ` x ) )
3 2 notbii 
 |-  ( -. E. x e. On ( A ` x ) =/= ( B ` x ) <-> -. E. x e. On -. ( A ` x ) = ( B ` x ) )
4 dfral2 
 |-  ( A. x e. On ( A ` x ) = ( B ` x ) <-> -. E. x e. On -. ( A ` x ) = ( B ` x ) )
5 3 4 bitr4i 
 |-  ( -. E. x e. On ( A ` x ) =/= ( B ` x ) <-> A. x e. On ( A ` x ) = ( B ` x ) )
6 nodmord 
 |-  ( A e. No -> Ord dom A )
7 nodmord 
 |-  ( B e. No -> Ord dom B )
8 ordtri3or 
 |-  ( ( Ord dom A /\ Ord dom B ) -> ( dom A e. dom B \/ dom A = dom B \/ dom B e. dom A ) )
9 6 7 8 syl2an 
 |-  ( ( A e. No /\ B e. No ) -> ( dom A e. dom B \/ dom A = dom B \/ dom B e. dom A ) )
10 3orass 
 |-  ( ( dom A e. dom B \/ dom A = dom B \/ dom B e. dom A ) <-> ( dom A e. dom B \/ ( dom A = dom B \/ dom B e. dom A ) ) )
11 or12 
 |-  ( ( dom A e. dom B \/ ( dom A = dom B \/ dom B e. dom A ) ) <-> ( dom A = dom B \/ ( dom A e. dom B \/ dom B e. dom A ) ) )
12 10 11 bitri 
 |-  ( ( dom A e. dom B \/ dom A = dom B \/ dom B e. dom A ) <-> ( dom A = dom B \/ ( dom A e. dom B \/ dom B e. dom A ) ) )
13 9 12 sylib 
 |-  ( ( A e. No /\ B e. No ) -> ( dom A = dom B \/ ( dom A e. dom B \/ dom B e. dom A ) ) )
14 13 ord 
 |-  ( ( A e. No /\ B e. No ) -> ( -. dom A = dom B -> ( dom A e. dom B \/ dom B e. dom A ) ) )
15 noseponlem 
 |-  ( ( A e. No /\ B e. No /\ dom A e. dom B ) -> -. A. x e. On ( A ` x ) = ( B ` x ) )
16 15 3expia 
 |-  ( ( A e. No /\ B e. No ) -> ( dom A e. dom B -> -. A. x e. On ( A ` x ) = ( B ` x ) ) )
17 noseponlem 
 |-  ( ( B e. No /\ A e. No /\ dom B e. dom A ) -> -. A. x e. On ( B ` x ) = ( A ` x ) )
18 eqcom 
 |-  ( ( A ` x ) = ( B ` x ) <-> ( B ` x ) = ( A ` x ) )
19 18 ralbii 
 |-  ( A. x e. On ( A ` x ) = ( B ` x ) <-> A. x e. On ( B ` x ) = ( A ` x ) )
20 17 19 sylnibr 
 |-  ( ( B e. No /\ A e. No /\ dom B e. dom A ) -> -. A. x e. On ( A ` x ) = ( B ` x ) )
21 20 3expia 
 |-  ( ( B e. No /\ A e. No ) -> ( dom B e. dom A -> -. A. x e. On ( A ` x ) = ( B ` x ) ) )
22 21 ancoms 
 |-  ( ( A e. No /\ B e. No ) -> ( dom B e. dom A -> -. A. x e. On ( A ` x ) = ( B ` x ) ) )
23 16 22 jaod 
 |-  ( ( A e. No /\ B e. No ) -> ( ( dom A e. dom B \/ dom B e. dom A ) -> -. A. x e. On ( A ` x ) = ( B ` x ) ) )
24 14 23 syld 
 |-  ( ( A e. No /\ B e. No ) -> ( -. dom A = dom B -> -. A. x e. On ( A ` x ) = ( B ` x ) ) )
25 24 con4d 
 |-  ( ( A e. No /\ B e. No ) -> ( A. x e. On ( A ` x ) = ( B ` x ) -> dom A = dom B ) )
26 25 3impia 
 |-  ( ( A e. No /\ B e. No /\ A. x e. On ( A ` x ) = ( B ` x ) ) -> dom A = dom B )
27 ordsson 
 |-  ( Ord dom A -> dom A C_ On )
28 ssralv 
 |-  ( dom A C_ On -> ( A. x e. On ( A ` x ) = ( B ` x ) -> A. x e. dom A ( A ` x ) = ( B ` x ) ) )
29 6 27 28 3syl 
 |-  ( A e. No -> ( A. x e. On ( A ` x ) = ( B ` x ) -> A. x e. dom A ( A ` x ) = ( B ` x ) ) )
30 29 adantr 
 |-  ( ( A e. No /\ B e. No ) -> ( A. x e. On ( A ` x ) = ( B ` x ) -> A. x e. dom A ( A ` x ) = ( B ` x ) ) )
31 30 3impia 
 |-  ( ( A e. No /\ B e. No /\ A. x e. On ( A ` x ) = ( B ` x ) ) -> A. x e. dom A ( A ` x ) = ( B ` x ) )
32 nofun 
 |-  ( A e. No -> Fun A )
33 32 3ad2ant1 
 |-  ( ( A e. No /\ B e. No /\ A. x e. On ( A ` x ) = ( B ` x ) ) -> Fun A )
34 nofun 
 |-  ( B e. No -> Fun B )
35 34 3ad2ant2 
 |-  ( ( A e. No /\ B e. No /\ A. x e. On ( A ` x ) = ( B ` x ) ) -> Fun B )
36 eqfunfv 
 |-  ( ( Fun A /\ Fun B ) -> ( A = B <-> ( dom A = dom B /\ A. x e. dom A ( A ` x ) = ( B ` x ) ) ) )
37 33 35 36 syl2anc 
 |-  ( ( A e. No /\ B e. No /\ A. x e. On ( A ` x ) = ( B ` x ) ) -> ( A = B <-> ( dom A = dom B /\ A. x e. dom A ( A ` x ) = ( B ` x ) ) ) )
38 26 31 37 mpbir2and 
 |-  ( ( A e. No /\ B e. No /\ A. x e. On ( A ` x ) = ( B ` x ) ) -> A = B )
39 38 3expia 
 |-  ( ( A e. No /\ B e. No ) -> ( A. x e. On ( A ` x ) = ( B ` x ) -> A = B ) )
40 5 39 syl5bi 
 |-  ( ( A e. No /\ B e. No ) -> ( -. E. x e. On ( A ` x ) =/= ( B ` x ) -> A = B ) )
41 40 necon1ad 
 |-  ( ( A e. No /\ B e. No ) -> ( A =/= B -> E. x e. On ( A ` x ) =/= ( B ` x ) ) )
42 41 3impia 
 |-  ( ( A e. No /\ B e. No /\ A =/= B ) -> E. x e. On ( A ` x ) =/= ( B ` x ) )
43 onintrab2 
 |-  ( E. x e. On ( A ` x ) =/= ( B ` x ) <-> |^| { x e. On | ( A ` x ) =/= ( B ` x ) } e. On )
44 42 43 sylib 
 |-  ( ( A e. No /\ B e. No /\ A =/= B ) -> |^| { x e. On | ( A ` x ) =/= ( B ` x ) } e. On )