Metamath Proof Explorer

Theorem noextenddif

Description: Calculate the place where a surreal and its extension differ. (Contributed by Scott Fenton, 22-Nov-2021)

Ref Expression
Hypothesis noextend.1 
|- X e. { 1o , 2o }
Assertion noextenddif 
|- ( A e. No -> |^| { x e. On | ( A ` x ) =/= ( ( A u. { <. dom A , X >. } ) ` x ) } = dom A )

Proof

Step Hyp Ref Expression
1 noextend.1 
 |-  X e. { 1o , 2o }
2 nodmon 
 |-  ( A e. No -> dom A e. On )
3 1 nosgnn0i 
 |-  (/) =/= X
4 3 a1i 
 |-  ( A e. No -> (/) =/= X )
5 nodmord 
 |-  ( A e. No -> Ord dom A )
6 ordirr 
 |-  ( Ord dom A -> -. dom A e. dom A )
7 5 6 syl 
 |-  ( A e. No -> -. dom A e. dom A )
8 ndmfv 
 |-  ( -. dom A e. dom A -> ( A ` dom A ) = (/) )
9 7 8 syl 
 |-  ( A e. No -> ( A ` dom A ) = (/) )
10 nofun 
 |-  ( A e. No -> Fun A )
11 funfn 
 |-  ( Fun A <-> A Fn dom A )
12 10 11 sylib 
 |-  ( A e. No -> A Fn dom A )
13 fnsng 
 |-  ( ( dom A e. On /\ X e. { 1o , 2o } ) -> { <. dom A , X >. } Fn { dom A } )
14 2 1 13 sylancl 
 |-  ( A e. No -> { <. dom A , X >. } Fn { dom A } )
15 disjsn 
 |-  ( ( dom A i^i { dom A } ) = (/) <-> -. dom A e. dom A )
16 7 15 sylibr 
 |-  ( A e. No -> ( dom A i^i { dom A } ) = (/) )
17 snidg 
 |-  ( dom A e. On -> dom A e. { dom A } )
18 2 17 syl 
 |-  ( A e. No -> dom A e. { dom A } )
19 fvun2 
 |-  ( ( A Fn dom A /\ { <. dom A , X >. } Fn { dom A } /\ ( ( dom A i^i { dom A } ) = (/) /\ dom A e. { dom A } ) ) -> ( ( A u. { <. dom A , X >. } ) ` dom A ) = ( { <. dom A , X >. } ` dom A ) )
20 12 14 16 18 19 syl112anc 
 |-  ( A e. No -> ( ( A u. { <. dom A , X >. } ) ` dom A ) = ( { <. dom A , X >. } ` dom A ) )
21 fvsng 
 |-  ( ( dom A e. On /\ X e. { 1o , 2o } ) -> ( { <. dom A , X >. } ` dom A ) = X )
22 2 1 21 sylancl 
 |-  ( A e. No -> ( { <. dom A , X >. } ` dom A ) = X )
23 20 22 eqtrd 
 |-  ( A e. No -> ( ( A u. { <. dom A , X >. } ) ` dom A ) = X )
24 4 9 23 3netr4d 
 |-  ( A e. No -> ( A ` dom A ) =/= ( ( A u. { <. dom A , X >. } ) ` dom A ) )
25 fveq2 
 |-  ( x = dom A -> ( A ` x ) = ( A ` dom A ) )
26 fveq2 
 |-  ( x = dom A -> ( ( A u. { <. dom A , X >. } ) ` x ) = ( ( A u. { <. dom A , X >. } ) ` dom A ) )
27 25 26 neeq12d 
 |-  ( x = dom A -> ( ( A ` x ) =/= ( ( A u. { <. dom A , X >. } ) ` x ) <-> ( A ` dom A ) =/= ( ( A u. { <. dom A , X >. } ) ` dom A ) ) )
28 27 onintss 
 |-  ( dom A e. On -> ( ( A ` dom A ) =/= ( ( A u. { <. dom A , X >. } ) ` dom A ) -> |^| { x e. On | ( A ` x ) =/= ( ( A u. { <. dom A , X >. } ) ` x ) } C_ dom A ) )
29 2 24 28 sylc 
 |-  ( A e. No -> |^| { x e. On | ( A ` x ) =/= ( ( A u. { <. dom A , X >. } ) ` x ) } C_ dom A )
30 eloni 
 |-  ( y e. On -> Ord y )
31 ordtri2 
 |-  ( ( Ord y /\ Ord dom A ) -> ( y e. dom A <-> -. ( y = dom A \/ dom A e. y ) ) )
32 eqcom 
 |-  ( y = dom A <-> dom A = y )
33 32 orbi1i 
 |-  ( ( y = dom A \/ dom A e. y ) <-> ( dom A = y \/ dom A e. y ) )
34 orcom 
 |-  ( ( dom A = y \/ dom A e. y ) <-> ( dom A e. y \/ dom A = y ) )
35 33 34 bitri 
 |-  ( ( y = dom A \/ dom A e. y ) <-> ( dom A e. y \/ dom A = y ) )
36 35 notbii 
 |-  ( -. ( y = dom A \/ dom A e. y ) <-> -. ( dom A e. y \/ dom A = y ) )
37 31 36 bitrdi 
 |-  ( ( Ord y /\ Ord dom A ) -> ( y e. dom A <-> -. ( dom A e. y \/ dom A = y ) ) )
38 ordsseleq 
 |-  ( ( Ord dom A /\ Ord y ) -> ( dom A C_ y <-> ( dom A e. y \/ dom A = y ) ) )
39 38 notbid 
 |-  ( ( Ord dom A /\ Ord y ) -> ( -. dom A C_ y <-> -. ( dom A e. y \/ dom A = y ) ) )
40 39 ancoms 
 |-  ( ( Ord y /\ Ord dom A ) -> ( -. dom A C_ y <-> -. ( dom A e. y \/ dom A = y ) ) )
41 37 40 bitr4d 
 |-  ( ( Ord y /\ Ord dom A ) -> ( y e. dom A <-> -. dom A C_ y ) )
42 30 5 41 syl2anr 
 |-  ( ( A e. No /\ y e. On ) -> ( y e. dom A <-> -. dom A C_ y ) )
43 12 3ad2ant1 
 |-  ( ( A e. No /\ y e. On /\ y e. dom A ) -> A Fn dom A )
44 14 3ad2ant1 
 |-  ( ( A e. No /\ y e. On /\ y e. dom A ) -> { <. dom A , X >. } Fn { dom A } )
45 16 3ad2ant1 
 |-  ( ( A e. No /\ y e. On /\ y e. dom A ) -> ( dom A i^i { dom A } ) = (/) )
46 simp3 
 |-  ( ( A e. No /\ y e. On /\ y e. dom A ) -> y e. dom A )
47 fvun1 
 |-  ( ( A Fn dom A /\ { <. dom A , X >. } Fn { dom A } /\ ( ( dom A i^i { dom A } ) = (/) /\ y e. dom A ) ) -> ( ( A u. { <. dom A , X >. } ) ` y ) = ( A ` y ) )
48 43 44 45 46 47 syl112anc 
 |-  ( ( A e. No /\ y e. On /\ y e. dom A ) -> ( ( A u. { <. dom A , X >. } ) ` y ) = ( A ` y ) )
49 48 eqcomd 
 |-  ( ( A e. No /\ y e. On /\ y e. dom A ) -> ( A ` y ) = ( ( A u. { <. dom A , X >. } ) ` y ) )
50 49 3expia 
 |-  ( ( A e. No /\ y e. On ) -> ( y e. dom A -> ( A ` y ) = ( ( A u. { <. dom A , X >. } ) ` y ) ) )
51 42 50 sylbird 
 |-  ( ( A e. No /\ y e. On ) -> ( -. dom A C_ y -> ( A ` y ) = ( ( A u. { <. dom A , X >. } ) ` y ) ) )
52 51 necon1ad 
 |-  ( ( A e. No /\ y e. On ) -> ( ( A ` y ) =/= ( ( A u. { <. dom A , X >. } ) ` y ) -> dom A C_ y ) )
53 52 ralrimiva 
 |-  ( A e. No -> A. y e. On ( ( A ` y ) =/= ( ( A u. { <. dom A , X >. } ) ` y ) -> dom A C_ y ) )
54 fveq2 
 |-  ( x = y -> ( A ` x ) = ( A ` y ) )
55 fveq2 
 |-  ( x = y -> ( ( A u. { <. dom A , X >. } ) ` x ) = ( ( A u. { <. dom A , X >. } ) ` y ) )
56 54 55 neeq12d 
 |-  ( x = y -> ( ( A ` x ) =/= ( ( A u. { <. dom A , X >. } ) ` x ) <-> ( A ` y ) =/= ( ( A u. { <. dom A , X >. } ) ` y ) ) )
57 56 ralrab 
 |-  ( A. y e. { x e. On | ( A ` x ) =/= ( ( A u. { <. dom A , X >. } ) ` x ) } dom A C_ y <-> A. y e. On ( ( A ` y ) =/= ( ( A u. { <. dom A , X >. } ) ` y ) -> dom A C_ y ) )
58 53 57 sylibr 
 |-  ( A e. No -> A. y e. { x e. On | ( A ` x ) =/= ( ( A u. { <. dom A , X >. } ) ` x ) } dom A C_ y )
59 ssint 
 |-  ( dom A C_ |^| { x e. On | ( A ` x ) =/= ( ( A u. { <. dom A , X >. } ) ` x ) } <-> A. y e. { x e. On | ( A ` x ) =/= ( ( A u. { <. dom A , X >. } ) ` x ) } dom A C_ y )
60 58 59 sylibr 
 |-  ( A e. No -> dom A C_ |^| { x e. On | ( A ` x ) =/= ( ( A u. { <. dom A , X >. } ) ` x ) } )
61 29 60 eqssd 
 |-  ( A e. No -> |^| { x e. On | ( A ` x ) =/= ( ( A u. { <. dom A , X >. } ) ` x ) } = dom A )