Metamath Proof Explorer

Theorem sltlpss

Description: If two surreals share a birthday, then X iff the left set of X is a proper subset of the left set of Y . (Contributed by Scott Fenton, 17-Sep-2024)

Ref Expression
Assertion sltlpss 
|- ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) -> ( X  ( _Left ` X ) C. ( _Left ` Y ) ) )

Proof

Step Hyp Ref Expression
1 oldssno 
 |-  ( _Old ` ( bday ` X ) ) C_ No
2 1 sseli 
 |-  ( x e. ( _Old ` ( bday ` X ) ) -> x e. No )
3 2 3ad2ant2 
 |-  ( ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X  x e. No )
4 simp1l1 
 |-  ( ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X  X e. No )
5 simp1l2 
 |-  ( ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X  Y e. No )
6 simp3 
 |-  ( ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X  x
7 simp1r 
 |-  ( ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X  X
8 3 4 5 6 7 slttrd 
 |-  ( ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X  x
9 8 3exp 
 |-  ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X  ( x e. ( _Old ` ( bday ` X ) ) -> ( x  x
10 9 imdistand 
 |-  ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X  ( ( x e. ( _Old ` ( bday ` X ) ) /\ x  ( x e. ( _Old ` ( bday ` X ) ) /\ x
11 fveq2 
 |-  ( ( bday ` X ) = ( bday ` Y ) -> ( _Old ` ( bday ` X ) ) = ( _Old ` ( bday ` Y ) ) )
12 11 3ad2ant3 
 |-  ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) -> ( _Old ` ( bday ` X ) ) = ( _Old ` ( bday ` Y ) ) )
13 12 adantr 
 |-  ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X  ( _Old ` ( bday ` X ) ) = ( _Old ` ( bday ` Y ) ) )
14 13 eleq2d 
 |-  ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X  ( x e. ( _Old ` ( bday ` X ) ) <-> x e. ( _Old ` ( bday ` Y ) ) ) )
15 14 anbi1d 
 |-  ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X  ( ( x e. ( _Old ` ( bday ` X ) ) /\ x  ( x e. ( _Old ` ( bday ` Y ) ) /\ x
16 10 15 sylibd 
 |-  ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X  ( ( x e. ( _Old ` ( bday ` X ) ) /\ x  ( x e. ( _Old ` ( bday ` Y ) ) /\ x
17 leftval 
 |-  ( _Left ` X ) = { x e. ( _Old ` ( bday ` X ) ) | x
18 17 a1i 
 |-  ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X  ( _Left ` X ) = { x e. ( _Old ` ( bday ` X ) ) | x
19 18 eleq2d 
 |-  ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X  ( x e. ( _Left ` X ) <-> x e. { x e. ( _Old ` ( bday ` X ) ) | x
20 rabid 
 |-  ( x e. { x e. ( _Old ` ( bday ` X ) ) | x  ( x e. ( _Old ` ( bday ` X ) ) /\ x
21 19 20 bitrdi 
 |-  ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X  ( x e. ( _Left ` X ) <-> ( x e. ( _Old ` ( bday ` X ) ) /\ x
22 leftval 
 |-  ( _Left ` Y ) = { x e. ( _Old ` ( bday ` Y ) ) | x
23 22 a1i 
 |-  ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X  ( _Left ` Y ) = { x e. ( _Old ` ( bday ` Y ) ) | x
24 23 eleq2d 
 |-  ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X  ( x e. ( _Left ` Y ) <-> x e. { x e. ( _Old ` ( bday ` Y ) ) | x
25 rabid 
 |-  ( x e. { x e. ( _Old ` ( bday ` Y ) ) | x  ( x e. ( _Old ` ( bday ` Y ) ) /\ x
26 24 25 bitrdi 
 |-  ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X  ( x e. ( _Left ` Y ) <-> ( x e. ( _Old ` ( bday ` Y ) ) /\ x
27 16 21 26 3imtr4d 
 |-  ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X  ( x e. ( _Left ` X ) -> x e. ( _Left ` Y ) ) )
28 27 ssrdv 
 |-  ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X  ( _Left ` X ) C_ ( _Left ` Y ) )
29 sltirr 
 |-  ( Y e. No -> -. Y
30 29 3ad2ant2 
 |-  ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) -> -. Y
31 breq1 
 |-  ( X = Y -> ( X  Y
32 31 notbid 
 |-  ( X = Y -> ( -. X  -. Y
33 30 32 syl5ibrcom 
 |-  ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) -> ( X = Y -> -. X
34 33 con2d 
 |-  ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) -> ( X  -. X = Y ) )
35 34 imp 
 |-  ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X  -. X = Y )
36 simpr 
 |-  ( ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X  ( _Left ` X ) = ( _Left ` Y ) )
37 lruneq 
 |-  ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) -> ( ( _Left ` X ) u. ( _Right ` X ) ) = ( ( _Left ` Y ) u. ( _Right ` Y ) ) )
38 37 adantr 
 |-  ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X  ( ( _Left ` X ) u. ( _Right ` X ) ) = ( ( _Left ` Y ) u. ( _Right ` Y ) ) )
39 38 adantr 
 |-  ( ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X  ( ( _Left ` X ) u. ( _Right ` X ) ) = ( ( _Left ` Y ) u. ( _Right ` Y ) ) )
40 39 36 difeq12d 
 |-  ( ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X  ( ( ( _Left ` X ) u. ( _Right ` X ) ) \ ( _Left ` X ) ) = ( ( ( _Left ` Y ) u. ( _Right ` Y ) ) \ ( _Left ` Y ) ) )
41 difundir 
 |-  ( ( ( _Left ` X ) u. ( _Right ` X ) ) \ ( _Left ` X ) ) = ( ( ( _Left ` X ) \ ( _Left ` X ) ) u. ( ( _Right ` X ) \ ( _Left ` X ) ) )
42 difid 
 |-  ( ( _Left ` X ) \ ( _Left ` X ) ) = (/)
43 42 uneq1i 
 |-  ( ( ( _Left ` X ) \ ( _Left ` X ) ) u. ( ( _Right ` X ) \ ( _Left ` X ) ) ) = ( (/) u. ( ( _Right ` X ) \ ( _Left ` X ) ) )
44 0un 
 |-  ( (/) u. ( ( _Right ` X ) \ ( _Left ` X ) ) ) = ( ( _Right ` X ) \ ( _Left ` X ) )
45 41 43 44 3eqtri 
 |-  ( ( ( _Left ` X ) u. ( _Right ` X ) ) \ ( _Left ` X ) ) = ( ( _Right ` X ) \ ( _Left ` X ) )
46 incom 
 |-  ( ( _Left ` X ) i^i ( _Right ` X ) ) = ( ( _Right ` X ) i^i ( _Left ` X ) )
47 lltropt 
 |-  ( _Left ` X ) <
48 ssltdisj 
 |-  ( ( _Left ` X ) < ( ( _Left ` X ) i^i ( _Right ` X ) ) = (/) )
49 47 48 mp1i 
 |-  ( ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X  ( ( _Left ` X ) i^i ( _Right ` X ) ) = (/) )
50 46 49 eqtr3id 
 |-  ( ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X  ( ( _Right ` X ) i^i ( _Left ` X ) ) = (/) )
51 disjdif2 
 |-  ( ( ( _Right ` X ) i^i ( _Left ` X ) ) = (/) -> ( ( _Right ` X ) \ ( _Left ` X ) ) = ( _Right ` X ) )
52 50 51 syl 
 |-  ( ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X  ( ( _Right ` X ) \ ( _Left ` X ) ) = ( _Right ` X ) )
53 45 52 eqtrid 
 |-  ( ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X  ( ( ( _Left ` X ) u. ( _Right ` X ) ) \ ( _Left ` X ) ) = ( _Right ` X ) )
54 difundir 
 |-  ( ( ( _Left ` Y ) u. ( _Right ` Y ) ) \ ( _Left ` Y ) ) = ( ( ( _Left ` Y ) \ ( _Left ` Y ) ) u. ( ( _Right ` Y ) \ ( _Left ` Y ) ) )
55 difid 
 |-  ( ( _Left ` Y ) \ ( _Left ` Y ) ) = (/)
56 55 uneq1i 
 |-  ( ( ( _Left ` Y ) \ ( _Left ` Y ) ) u. ( ( _Right ` Y ) \ ( _Left ` Y ) ) ) = ( (/) u. ( ( _Right ` Y ) \ ( _Left ` Y ) ) )
57 0un 
 |-  ( (/) u. ( ( _Right ` Y ) \ ( _Left ` Y ) ) ) = ( ( _Right ` Y ) \ ( _Left ` Y ) )
58 54 56 57 3eqtri 
 |-  ( ( ( _Left ` Y ) u. ( _Right ` Y ) ) \ ( _Left ` Y ) ) = ( ( _Right ` Y ) \ ( _Left ` Y ) )
59 incom 
 |-  ( ( _Left ` Y ) i^i ( _Right ` Y ) ) = ( ( _Right ` Y ) i^i ( _Left ` Y ) )
60 lltropt 
 |-  ( _Left ` Y ) <
61 ssltdisj 
 |-  ( ( _Left ` Y ) < ( ( _Left ` Y ) i^i ( _Right ` Y ) ) = (/) )
62 60 61 mp1i 
 |-  ( ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X  ( ( _Left ` Y ) i^i ( _Right ` Y ) ) = (/) )
63 59 62 eqtr3id 
 |-  ( ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X  ( ( _Right ` Y ) i^i ( _Left ` Y ) ) = (/) )
64 disjdif2 
 |-  ( ( ( _Right ` Y ) i^i ( _Left ` Y ) ) = (/) -> ( ( _Right ` Y ) \ ( _Left ` Y ) ) = ( _Right ` Y ) )
65 63 64 syl 
 |-  ( ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X  ( ( _Right ` Y ) \ ( _Left ` Y ) ) = ( _Right ` Y ) )
66 58 65 eqtrid 
 |-  ( ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X  ( ( ( _Left ` Y ) u. ( _Right ` Y ) ) \ ( _Left ` Y ) ) = ( _Right ` Y ) )
67 40 53 66 3eqtr3d 
 |-  ( ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X  ( _Right ` X ) = ( _Right ` Y ) )
68 36 67 oveq12d 
 |-  ( ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X  ( ( _Left ` X ) |s ( _Right ` X ) ) = ( ( _Left ` Y ) |s ( _Right ` Y ) ) )
69 simpll1 
 |-  ( ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X  X e. No )
70 lrcut 
 |-  ( X e. No -> ( ( _Left ` X ) |s ( _Right ` X ) ) = X )
71 69 70 syl 
 |-  ( ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X  ( ( _Left ` X ) |s ( _Right ` X ) ) = X )
72 simpll2 
 |-  ( ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X  Y e. No )
73 lrcut 
 |-  ( Y e. No -> ( ( _Left ` Y ) |s ( _Right ` Y ) ) = Y )
74 72 73 syl 
 |-  ( ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X  ( ( _Left ` Y ) |s ( _Right ` Y ) ) = Y )
75 68 71 74 3eqtr3d 
 |-  ( ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X  X = Y )
76 35 75 mtand 
 |-  ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X  -. ( _Left ` X ) = ( _Left ` Y ) )
77 dfpss2 
 |-  ( ( _Left ` X ) C. ( _Left ` Y ) <-> ( ( _Left ` X ) C_ ( _Left ` Y ) /\ -. ( _Left ` X ) = ( _Left ` Y ) ) )
78 28 76 77 sylanbrc 
 |-  ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ X  ( _Left ` X ) C. ( _Left ` Y ) )
79 78 ex 
 |-  ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) -> ( X  ( _Left ` X ) C. ( _Left ` Y ) ) )
80 dfpss3 
 |-  ( ( _Left ` X ) C. ( _Left ` Y ) <-> ( ( _Left ` X ) C_ ( _Left ` Y ) /\ -. ( _Left ` Y ) C_ ( _Left ` X ) ) )
81 ssdif0 
 |-  ( ( _Left ` Y ) C_ ( _Left ` X ) <-> ( ( _Left ` Y ) \ ( _Left ` X ) ) = (/) )
82 81 necon3bbii 
 |-  ( -. ( _Left ` Y ) C_ ( _Left ` X ) <-> ( ( _Left ` Y ) \ ( _Left ` X ) ) =/= (/) )
83 n0 
 |-  ( ( ( _Left ` Y ) \ ( _Left ` X ) ) =/= (/) <-> E. x x e. ( ( _Left ` Y ) \ ( _Left ` X ) ) )
84 82 83 bitri 
 |-  ( -. ( _Left ` Y ) C_ ( _Left ` X ) <-> E. x x e. ( ( _Left ` Y ) \ ( _Left ` X ) ) )
85 eldif 
 |-  ( x e. ( ( _Left ` Y ) \ ( _Left ` X ) ) <-> ( x e. ( _Left ` Y ) /\ -. x e. ( _Left ` X ) ) )
86 22 a1i 
 |-  ( Y e. No -> ( _Left ` Y ) = { x e. ( _Old ` ( bday ` Y ) ) | x
87 86 eleq2d 
 |-  ( Y e. No -> ( x e. ( _Left ` Y ) <-> x e. { x e. ( _Old ` ( bday ` Y ) ) | x
88 87 25 bitrdi 
 |-  ( Y e. No -> ( x e. ( _Left ` Y ) <-> ( x e. ( _Old ` ( bday ` Y ) ) /\ x
89 17 a1i 
 |-  ( X e. No -> ( _Left ` X ) = { x e. ( _Old ` ( bday ` X ) ) | x
90 89 eleq2d 
 |-  ( X e. No -> ( x e. ( _Left ` X ) <-> x e. { x e. ( _Old ` ( bday ` X ) ) | x
91 90 20 bitrdi 
 |-  ( X e. No -> ( x e. ( _Left ` X ) <-> ( x e. ( _Old ` ( bday ` X ) ) /\ x
92 91 notbid 
 |-  ( X e. No -> ( -. x e. ( _Left ` X ) <-> -. ( x e. ( _Old ` ( bday ` X ) ) /\ x
93 ianor 
 |-  ( -. ( x e. ( _Old ` ( bday ` X ) ) /\ x  ( -. x e. ( _Old ` ( bday ` X ) ) \/ -. x
94 92 93 bitrdi 
 |-  ( X e. No -> ( -. x e. ( _Left ` X ) <-> ( -. x e. ( _Old ` ( bday ` X ) ) \/ -. x
95 88 94 bi2anan9r 
 |-  ( ( X e. No /\ Y e. No ) -> ( ( x e. ( _Left ` Y ) /\ -. x e. ( _Left ` X ) ) <-> ( ( x e. ( _Old ` ( bday ` Y ) ) /\ x
96 95 3adant3 
 |-  ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) -> ( ( x e. ( _Left ` Y ) /\ -. x e. ( _Left ` X ) ) <-> ( ( x e. ( _Old ` ( bday ` Y ) ) /\ x
97 simprl 
 |-  ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ ( x e. ( _Old ` ( bday ` Y ) ) /\ x  x e. ( _Old ` ( bday ` Y ) ) )
98 simpl3 
 |-  ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ ( x e. ( _Old ` ( bday ` Y ) ) /\ x  ( bday ` X ) = ( bday ` Y ) )
99 98 fveq2d 
 |-  ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ ( x e. ( _Old ` ( bday ` Y ) ) /\ x  ( _Old ` ( bday ` X ) ) = ( _Old ` ( bday ` Y ) ) )
100 97 99 eleqtrrd 
 |-  ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ ( x e. ( _Old ` ( bday ` Y ) ) /\ x  x e. ( _Old ` ( bday ` X ) ) )
101 100 pm2.24d 
 |-  ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ ( x e. ( _Old ` ( bday ` Y ) ) /\ x  ( -. x e. ( _Old ` ( bday ` X ) ) -> X
102 simpll1 
 |-  ( ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ ( x e. ( _Old ` ( bday ` Y ) ) /\ x  X e. No )
103 oldssno 
 |-  ( _Old ` ( bday ` Y ) ) C_ No
104 103 97 sselid 
 |-  ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ ( x e. ( _Old ` ( bday ` Y ) ) /\ x  x e. No )
105 104 adantr 
 |-  ( ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ ( x e. ( _Old ` ( bday ` Y ) ) /\ x  x e. No )
106 simpll2 
 |-  ( ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ ( x e. ( _Old ` ( bday ` Y ) ) /\ x  Y e. No )
107 simpl1 
 |-  ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ ( x e. ( _Old ` ( bday ` Y ) ) /\ x  X e. No )
108 slenlt 
 |-  ( ( X e. No /\ x e. No ) -> ( X <_s x <-> -. x
109 107 104 108 syl2anc 
 |-  ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ ( x e. ( _Old ` ( bday ` Y ) ) /\ x  ( X <_s x <-> -. x
110 109 biimpar 
 |-  ( ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ ( x e. ( _Old ` ( bday ` Y ) ) /\ x  X <_s x )
111 simplrr 
 |-  ( ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ ( x e. ( _Old ` ( bday ` Y ) ) /\ x  x
112 102 105 106 110 111 slelttrd 
 |-  ( ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ ( x e. ( _Old ` ( bday ` Y ) ) /\ x  X
113 112 ex 
 |-  ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ ( x e. ( _Old ` ( bday ` Y ) ) /\ x  ( -. x  X
114 101 113 jaod 
 |-  ( ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) /\ ( x e. ( _Old ` ( bday ` Y ) ) /\ x  ( ( -. x e. ( _Old ` ( bday ` X ) ) \/ -. x  X
115 114 expimpd 
 |-  ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) -> ( ( ( x e. ( _Old ` ( bday ` Y ) ) /\ x  X
116 96 115 sylbid 
 |-  ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) -> ( ( x e. ( _Left ` Y ) /\ -. x e. ( _Left ` X ) ) -> X
117 85 116 biimtrid 
 |-  ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) -> ( x e. ( ( _Left ` Y ) \ ( _Left ` X ) ) -> X
118 117 exlimdv 
 |-  ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) -> ( E. x x e. ( ( _Left ` Y ) \ ( _Left ` X ) ) -> X
119 84 118 biimtrid 
 |-  ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) -> ( -. ( _Left ` Y ) C_ ( _Left ` X ) -> X
120 119 adantld 
 |-  ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) -> ( ( ( _Left ` X ) C_ ( _Left ` Y ) /\ -. ( _Left ` Y ) C_ ( _Left ` X ) ) -> X
121 80 120 biimtrid 
 |-  ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) -> ( ( _Left ` X ) C. ( _Left ` Y ) -> X
122 79 121 impbid 
 |-  ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) -> ( X  ( _Left ` X ) C. ( _Left ` Y ) ) )