Metamath Proof Explorer

Theorem scutbdaylt

Description: If a surreal lies in a gap and is not equal to the cut, its birthday is greater than the cut's. (Contributed by Scott Fenton, 11-Dec-2021)

Ref Expression
Assertion scutbdaylt 
|- ( ( X e. No /\ ( A < ( bday ` ( A |s B ) ) e. ( bday ` X ) )

Proof

Step Hyp Ref Expression
1 simp2l 
 |-  ( ( X e. No /\ ( A < A <
2 simp2r 
 |-  ( ( X e. No /\ ( A < { X } <
3 snnzg 
 |-  ( X e. No -> { X } =/= (/) )
4 3 3ad2ant1 
 |-  ( ( X e. No /\ ( A < { X } =/= (/) )
5 sslttr 
 |-  ( ( A < A <
6 1 2 4 5 syl3anc 
 |-  ( ( X e. No /\ ( A < A <
7 scutbday 
 |-  ( A < ( bday ` ( A |s B ) ) = |^| ( bday " { y e. No | ( A <
8 6 7 syl 
 |-  ( ( X e. No /\ ( A < ( bday ` ( A |s B ) ) = |^| ( bday " { y e. No | ( A <
9 bdayfn 
 |-  bday Fn No
10 ssrab2 
 |-  { y e. No | ( A <
11 simp1 
 |-  ( ( X e. No /\ ( A < X e. No )
12 simp2 
 |-  ( ( X e. No /\ ( A < ( A <
13 sneq 
 |-  ( y = X -> { y } = { X } )
14 13 breq2d 
 |-  ( y = X -> ( A < A <
15 13 breq1d 
 |-  ( y = X -> ( { y } < { X } <
16 14 15 anbi12d 
 |-  ( y = X -> ( ( A < ( A <
17 16 elrab 
 |-  ( X e. { y e. No | ( A < ( X e. No /\ ( A <
18 11 12 17 sylanbrc 
 |-  ( ( X e. No /\ ( A < X e. { y e. No | ( A <
19 fnfvima 
 |-  ( ( bday Fn No /\ { y e. No | ( A < ( bday ` X ) e. ( bday " { y e. No | ( A <
20 9 10 18 19 mp3an12i 
 |-  ( ( X e. No /\ ( A < ( bday ` X ) e. ( bday " { y e. No | ( A <
21 intss1 
 |-  ( ( bday ` X ) e. ( bday " { y e. No | ( A < |^| ( bday " { y e. No | ( A <
22 20 21 syl 
 |-  ( ( X e. No /\ ( A < |^| ( bday " { y e. No | ( A <
23 8 22 eqsstrd 
 |-  ( ( X e. No /\ ( A < ( bday ` ( A |s B ) ) C_ ( bday ` X ) )
24 simprl 
 |-  ( ( X e. No /\ ( A < A <
25 simprr 
 |-  ( ( X e. No /\ ( A < { X } <
26 3 adantr 
 |-  ( ( X e. No /\ ( A < { X } =/= (/) )
27 24 25 26 5 syl3anc 
 |-  ( ( X e. No /\ ( A < A <
28 27 7 syl 
 |-  ( ( X e. No /\ ( A < ( bday ` ( A |s B ) ) = |^| ( bday " { y e. No | ( A <
29 28 eqeq1d 
 |-  ( ( X e. No /\ ( A < ( ( bday ` ( A |s B ) ) = ( bday ` X ) <-> |^| ( bday " { y e. No | ( A <
30 eqcom 
 |-  ( |^| ( bday " { y e. No | ( A < ( bday ` X ) = |^| ( bday " { y e. No | ( A <
31 29 30 bitrdi 
 |-  ( ( X e. No /\ ( A < ( ( bday ` ( A |s B ) ) = ( bday ` X ) <-> ( bday ` X ) = |^| ( bday " { y e. No | ( A <
32 31 biimpa 
 |-  ( ( ( X e. No /\ ( A < ( bday ` X ) = |^| ( bday " { y e. No | ( A <
33 17 biimpri 
 |-  ( ( X e. No /\ ( A < X e. { y e. No | ( A <
34 27 adantr 
 |-  ( ( ( X e. No /\ ( A < A <
35 conway 
 |-  ( A < E! x e. { y e. No | ( A <
36 34 35 syl 
 |-  ( ( ( X e. No /\ ( A < E! x e. { y e. No | ( A <
37 fveqeq2 
 |-  ( x = X -> ( ( bday ` x ) = |^| ( bday " { y e. No | ( A < ( bday ` X ) = |^| ( bday " { y e. No | ( A <
38 37 riota2 
 |-  ( ( X e. { y e. No | ( A < ( ( bday ` X ) = |^| ( bday " { y e. No | ( A < ( iota_ x e. { y e. No | ( A <
39 eqcom 
 |-  ( ( iota_ x e. { y e. No | ( A < X = ( iota_ x e. { y e. No | ( A <
40 38 39 bitrdi 
 |-  ( ( X e. { y e. No | ( A < ( ( bday ` X ) = |^| ( bday " { y e. No | ( A < X = ( iota_ x e. { y e. No | ( A <
41 33 36 40 syl2an2r 
 |-  ( ( ( X e. No /\ ( A < ( ( bday ` X ) = |^| ( bday " { y e. No | ( A < X = ( iota_ x e. { y e. No | ( A <
42 32 41 mpbid 
 |-  ( ( ( X e. No /\ ( A < X = ( iota_ x e. { y e. No | ( A <
43 scutval 
 |-  ( A < ( A |s B ) = ( iota_ x e. { y e. No | ( A <
44 34 43 syl 
 |-  ( ( ( X e. No /\ ( A < ( A |s B ) = ( iota_ x e. { y e. No | ( A <
45 42 44 eqtr4d 
 |-  ( ( ( X e. No /\ ( A < X = ( A |s B ) )
46 45 ex 
 |-  ( ( X e. No /\ ( A < ( ( bday ` ( A |s B ) ) = ( bday ` X ) -> X = ( A |s B ) ) )
47 46 necon3d 
 |-  ( ( X e. No /\ ( A < ( X =/= ( A |s B ) -> ( bday ` ( A |s B ) ) =/= ( bday ` X ) ) )
48 47 3impia 
 |-  ( ( X e. No /\ ( A < ( bday ` ( A |s B ) ) =/= ( bday ` X ) )
49 bdayelon 
 |-  ( bday ` ( A |s B ) ) e. On
50 bdayelon 
 |-  ( bday ` X ) e. On
51 onelpss 
 |-  ( ( ( bday ` ( A |s B ) ) e. On /\ ( bday ` X ) e. On ) -> ( ( bday ` ( A |s B ) ) e. ( bday ` X ) <-> ( ( bday ` ( A |s B ) ) C_ ( bday ` X ) /\ ( bday ` ( A |s B ) ) =/= ( bday ` X ) ) ) )
52 49 50 51 mp2an 
 |-  ( ( bday ` ( A |s B ) ) e. ( bday ` X ) <-> ( ( bday ` ( A |s B ) ) C_ ( bday ` X ) /\ ( bday ` ( A |s B ) ) =/= ( bday ` X ) ) )
53 23 48 52 sylanbrc 
 |-  ( ( X e. No /\ ( A < ( bday ` ( A |s B ) ) e. ( bday ` X ) )