Metamath Proof Explorer

Theorem eqscut2

Description: Condition for equality to a surreal cut. (Contributed by Scott Fenton, 8-Aug-2024)

Ref Expression
Assertion eqscut2 
|- ( ( L < ( ( L |s R ) = X <-> ( L < ( bday ` X ) C_ ( bday ` y ) ) ) ) )

Proof

Step Hyp Ref Expression
1 eqscut 
 |-  ( ( L < ( ( L |s R ) = X <-> ( L <
2 eqss 
 |-  ( ( bday ` X ) = |^| ( bday " { x e. No | ( L < ( ( bday ` X ) C_ |^| ( bday " { x e. No | ( L <
3 sneq 
 |-  ( x = X -> { x } = { X } )
4 3 breq2d 
 |-  ( x = X -> ( L < L <
5 3 breq1d 
 |-  ( x = X -> ( { x } < { X } <
6 4 5 anbi12d 
 |-  ( x = X -> ( ( L < ( L <
7 6 elrab3 
 |-  ( X e. No -> ( X e. { x e. No | ( L < ( L <
8 7 adantl 
 |-  ( ( L < ( X e. { x e. No | ( L < ( L <
9 8 biimpar 
 |-  ( ( ( L < X e. { x e. No | ( L <
10 bdayfn 
 |-  bday Fn No
11 ssrab2 
 |-  { x e. No | ( L <
12 fnfvima 
 |-  ( ( bday Fn No /\ { x e. No | ( L < ( bday ` X ) e. ( bday " { x e. No | ( L <
13 10 11 12 mp3an12 
 |-  ( X e. { x e. No | ( L < ( bday ` X ) e. ( bday " { x e. No | ( L <
14 intss1 
 |-  ( ( bday ` X ) e. ( bday " { x e. No | ( L < |^| ( bday " { x e. No | ( L <
15 9 13 14 3syl 
 |-  ( ( ( L < |^| ( bday " { x e. No | ( L <
16 15 biantrud 
 |-  ( ( ( L < ( ( bday ` X ) C_ |^| ( bday " { x e. No | ( L < ( ( bday ` X ) C_ |^| ( bday " { x e. No | ( L <
17 ssint 
 |-  ( ( bday ` X ) C_ |^| ( bday " { x e. No | ( L < A. z e. ( bday " { x e. No | ( L <
18 fvelimab 
 |-  ( ( bday Fn No /\ { x e. No | ( L < ( z e. ( bday " { x e. No | ( L < E. y e. { x e. No | ( L <
19 10 11 18 mp2an 
 |-  ( z e. ( bday " { x e. No | ( L < E. y e. { x e. No | ( L <
20 sneq 
 |-  ( x = y -> { x } = { y } )
21 20 breq2d 
 |-  ( x = y -> ( L < L <
22 20 breq1d 
 |-  ( x = y -> ( { x } < { y } <
23 21 22 anbi12d 
 |-  ( x = y -> ( ( L < ( L <
24 23 rexrab 
 |-  ( E. y e. { x e. No | ( L < E. y e. No ( ( L <
25 19 24 bitri 
 |-  ( z e. ( bday " { x e. No | ( L < E. y e. No ( ( L <
26 25 imbi1i 
 |-  ( ( z e. ( bday " { x e. No | ( L < ( bday ` X ) C_ z ) <-> ( E. y e. No ( ( L < ( bday ` X ) C_ z ) )
27 r19.23v 
 |-  ( A. y e. No ( ( ( L < ( bday ` X ) C_ z ) <-> ( E. y e. No ( ( L < ( bday ` X ) C_ z ) )
28 eqcom 
 |-  ( ( bday ` y ) = z <-> z = ( bday ` y ) )
29 28 anbi1ci 
 |-  ( ( ( L < ( z = ( bday ` y ) /\ ( L <
30 29 imbi1i 
 |-  ( ( ( ( L < ( bday ` X ) C_ z ) <-> ( ( z = ( bday ` y ) /\ ( L < ( bday ` X ) C_ z ) )
31 impexp 
 |-  ( ( ( z = ( bday ` y ) /\ ( L < ( bday ` X ) C_ z ) <-> ( z = ( bday ` y ) -> ( ( L < ( bday ` X ) C_ z ) ) )
32 30 31 bitri 
 |-  ( ( ( ( L < ( bday ` X ) C_ z ) <-> ( z = ( bday ` y ) -> ( ( L < ( bday ` X ) C_ z ) ) )
33 32 ralbii 
 |-  ( A. y e. No ( ( ( L < ( bday ` X ) C_ z ) <-> A. y e. No ( z = ( bday ` y ) -> ( ( L < ( bday ` X ) C_ z ) ) )
34 26 27 33 3bitr2i 
 |-  ( ( z e. ( bday " { x e. No | ( L < ( bday ` X ) C_ z ) <-> A. y e. No ( z = ( bday ` y ) -> ( ( L < ( bday ` X ) C_ z ) ) )
35 34 albii 
 |-  ( A. z ( z e. ( bday " { x e. No | ( L < ( bday ` X ) C_ z ) <-> A. z A. y e. No ( z = ( bday ` y ) -> ( ( L < ( bday ` X ) C_ z ) ) )
36 df-ral 
 |-  ( A. z e. ( bday " { x e. No | ( L < A. z ( z e. ( bday " { x e. No | ( L < ( bday ` X ) C_ z ) )
37 ralcom4 
 |-  ( A. y e. No A. z ( z = ( bday ` y ) -> ( ( L < ( bday ` X ) C_ z ) ) <-> A. z A. y e. No ( z = ( bday ` y ) -> ( ( L < ( bday ` X ) C_ z ) ) )
38 35 36 37 3bitr4i 
 |-  ( A. z e. ( bday " { x e. No | ( L < A. y e. No A. z ( z = ( bday ` y ) -> ( ( L < ( bday ` X ) C_ z ) ) )
39 fvex 
 |-  ( bday ` y ) e. _V
40 sseq2 
 |-  ( z = ( bday ` y ) -> ( ( bday ` X ) C_ z <-> ( bday ` X ) C_ ( bday ` y ) ) )
41 40 imbi2d 
 |-  ( z = ( bday ` y ) -> ( ( ( L < ( bday ` X ) C_ z ) <-> ( ( L < ( bday ` X ) C_ ( bday ` y ) ) ) )
42 39 41 ceqsalv 
 |-  ( A. z ( z = ( bday ` y ) -> ( ( L < ( bday ` X ) C_ z ) ) <-> ( ( L < ( bday ` X ) C_ ( bday ` y ) ) )
43 42 ralbii 
 |-  ( A. y e. No A. z ( z = ( bday ` y ) -> ( ( L < ( bday ` X ) C_ z ) ) <-> A. y e. No ( ( L < ( bday ` X ) C_ ( bday ` y ) ) )
44 38 43 bitri 
 |-  ( A. z e. ( bday " { x e. No | ( L < A. y e. No ( ( L < ( bday ` X ) C_ ( bday ` y ) ) )
45 17 44 bitri 
 |-  ( ( bday ` X ) C_ |^| ( bday " { x e. No | ( L < A. y e. No ( ( L < ( bday ` X ) C_ ( bday ` y ) ) )
46 16 45 bitr3di 
 |-  ( ( ( L < ( ( ( bday ` X ) C_ |^| ( bday " { x e. No | ( L < A. y e. No ( ( L < ( bday ` X ) C_ ( bday ` y ) ) ) )
47 2 46 syl5bb 
 |-  ( ( ( L < ( ( bday ` X ) = |^| ( bday " { x e. No | ( L < A. y e. No ( ( L < ( bday ` X ) C_ ( bday ` y ) ) ) )
48 47 pm5.32da 
 |-  ( ( L < ( ( ( L < ( ( L < ( bday ` X ) C_ ( bday ` y ) ) ) ) )
49 df-3an 
 |-  ( ( L < ( ( L <
50 df-3an 
 |-  ( ( L < ( bday ` X ) C_ ( bday ` y ) ) ) <-> ( ( L < ( bday ` X ) C_ ( bday ` y ) ) ) )
51 48 49 50 3bitr4g 
 |-  ( ( L < ( ( L < ( L < ( bday ` X ) C_ ( bday ` y ) ) ) ) )
52 1 51 bitrd 
 |-  ( ( L < ( ( L |s R ) = X <-> ( L < ( bday ` X ) C_ ( bday ` y ) ) ) ) )