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 Could not format assertion : No typesetting found for |- ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) -> ( X ( _Left ` X ) C. ( _Left ` Y ) ) ) with typecode |-

Proof

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