Theorem slelss

Description: If two surreals A and B share a birthday, then A <_s B if and only if the left set of A is a non-strict subset of the left set of B . (Contributed by Scott Fenton, 21-Mar-2025)

	Ref	Expression
Assertion	slelss	Could not format assertion : No typesetting found for |- ( ( A e. No /\ B e. No /\ ( bday ` A ) = ( bday ` B ) ) -> ( A <_s B <-> ( _Left ` A ) C_ ( _Left ` B ) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		sltlpss	Could not format ( ( A e. No /\ B e. No /\ ( bday ` A ) = ( bday ` B ) ) -> ( A ( _Left ` A ) C. ( _Left ` B ) ) ) : No typesetting found for |- ( ( A e. No /\ B e. No /\ ( bday ` A ) = ( bday ` B ) ) -> ( A ( _Left ` A ) C. ( _Left ` B ) ) ) with typecode |-
2		fveq2	Could not format ( A = B -> ( _Left ` A ) = ( _Left ` B ) ) : No typesetting found for |- ( A = B -> ( _Left ` A ) = ( _Left ` B ) ) with typecode |-
3		simpr	Could not format ( ( ( A e. No /\ B e. No /\ ( bday ` A ) = ( bday ` B ) ) /\ ( _Left ` A ) = ( _Left ` B ) ) -> ( _Left ` A ) = ( _Left ` B ) ) : No typesetting found for |- ( ( ( A e. No /\ B e. No /\ ( bday ` A ) = ( bday ` B ) ) /\ ( _Left ` A ) = ( _Left ` B ) ) -> ( _Left ` A ) = ( _Left ` B ) ) with typecode |-
4		lruneq	Could not format ( ( A e. No /\ B e. No /\ ( bday ` A ) = ( bday ` B ) ) -> ( ( _Left ` A ) u. ( _Right ` A ) ) = ( ( _Left ` B ) u. ( _Right ` B ) ) ) : No typesetting found for |- ( ( A e. No /\ B e. No /\ ( bday ` A ) = ( bday ` B ) ) -> ( ( _Left ` A ) u. ( _Right ` A ) ) = ( ( _Left ` B ) u. ( _Right ` B ) ) ) with typecode |-
5	4	adantr	Could not format ( ( ( A e. No /\ B e. No /\ ( bday ` A ) = ( bday ` B ) ) /\ ( _Left ` A ) = ( _Left ` B ) ) -> ( ( _Left ` A ) u. ( _Right ` A ) ) = ( ( _Left ` B ) u. ( _Right ` B ) ) ) : No typesetting found for |- ( ( ( A e. No /\ B e. No /\ ( bday ` A ) = ( bday ` B ) ) /\ ( _Left ` A ) = ( _Left ` B ) ) -> ( ( _Left ` A ) u. ( _Right ` A ) ) = ( ( _Left ` B ) u. ( _Right ` B ) ) ) with typecode |-
6	5 3	difeq12d	Could not format ( ( ( A e. No /\ B e. No /\ ( bday ` A ) = ( bday ` B ) ) /\ ( _Left ` A ) = ( _Left ` B ) ) -> ( ( ( _Left ` A ) u. ( _Right ` A ) ) \ ( _Left ` A ) ) = ( ( ( _Left ` B ) u. ( _Right ` B ) ) \ ( _Left ` B ) ) ) : No typesetting found for |- ( ( ( A e. No /\ B e. No /\ ( bday ` A ) = ( bday ` B ) ) /\ ( _Left ` A ) = ( _Left ` B ) ) -> ( ( ( _Left ` A ) u. ( _Right ` A ) ) \ ( _Left ` A ) ) = ( ( ( _Left ` B ) u. ( _Right ` B ) ) \ ( _Left ` B ) ) ) with typecode |-
7		difundir	Could not format ( ( ( _Left ` A ) u. ( _Right ` A ) ) \ ( _Left ` A ) ) = ( ( ( _Left ` A ) \ ( _Left ` A ) ) u. ( ( _Right ` A ) \ ( _Left ` A ) ) ) : No typesetting found for |- ( ( ( _Left ` A ) u. ( _Right ` A ) ) \ ( _Left ` A ) ) = ( ( ( _Left ` A ) \ ( _Left ` A ) ) u. ( ( _Right ` A ) \ ( _Left ` A ) ) ) with typecode |-
8		difid	Could not format ( ( _Left ` A ) \ ( _Left ` A ) ) = (/) : No typesetting found for |- ( ( _Left ` A ) \ ( _Left ` A ) ) = (/) with typecode |-
9	8	uneq1i	Could not format ( ( ( _Left ` A ) \ ( _Left ` A ) ) u. ( ( _Right ` A ) \ ( _Left ` A ) ) ) = ( (/) u. ( ( _Right ` A ) \ ( _Left ` A ) ) ) : No typesetting found for |- ( ( ( _Left ` A ) \ ( _Left ` A ) ) u. ( ( _Right ` A ) \ ( _Left ` A ) ) ) = ( (/) u. ( ( _Right ` A ) \ ( _Left ` A ) ) ) with typecode |-
10		0un	Could not format ( (/) u. ( ( _Right ` A ) \ ( _Left ` A ) ) ) = ( ( _Right ` A ) \ ( _Left ` A ) ) : No typesetting found for |- ( (/) u. ( ( _Right ` A ) \ ( _Left ` A ) ) ) = ( ( _Right ` A ) \ ( _Left ` A ) ) with typecode |-
11	7 9 10	3eqtri	Could not format ( ( ( _Left ` A ) u. ( _Right ` A ) ) \ ( _Left ` A ) ) = ( ( _Right ` A ) \ ( _Left ` A ) ) : No typesetting found for |- ( ( ( _Left ` A ) u. ( _Right ` A ) ) \ ( _Left ` A ) ) = ( ( _Right ` A ) \ ( _Left ` A ) ) with typecode |-
12		incom	Could not format ( ( _Left ` A ) i^i ( _Right ` A ) ) = ( ( _Right ` A ) i^i ( _Left ` A ) ) : No typesetting found for |- ( ( _Left ` A ) i^i ( _Right ` A ) ) = ( ( _Right ` A ) i^i ( _Left ` A ) ) with typecode |-
13		lltropt	Could not format ( _Left ` A ) <
14		ssltdisj	Could not format ( ( _Left ` A ) < ( ( _Left ` A ) i^i ( _Right ` A ) ) = (/) ) : No typesetting found for |- ( ( _Left ` A ) < ( ( _Left ` A ) i^i ( _Right ` A ) ) = (/) ) with typecode |-
15	13 14	mp1i	Could not format ( ( ( A e. No /\ B e. No /\ ( bday ` A ) = ( bday ` B ) ) /\ ( _Left ` A ) = ( _Left ` B ) ) -> ( ( _Left ` A ) i^i ( _Right ` A ) ) = (/) ) : No typesetting found for |- ( ( ( A e. No /\ B e. No /\ ( bday ` A ) = ( bday ` B ) ) /\ ( _Left ` A ) = ( _Left ` B ) ) -> ( ( _Left ` A ) i^i ( _Right ` A ) ) = (/) ) with typecode |-
16	12 15	eqtr3id	Could not format ( ( ( A e. No /\ B e. No /\ ( bday ` A ) = ( bday ` B ) ) /\ ( _Left ` A ) = ( _Left ` B ) ) -> ( ( _Right ` A ) i^i ( _Left ` A ) ) = (/) ) : No typesetting found for |- ( ( ( A e. No /\ B e. No /\ ( bday ` A ) = ( bday ` B ) ) /\ ( _Left ` A ) = ( _Left ` B ) ) -> ( ( _Right ` A ) i^i ( _Left ` A ) ) = (/) ) with typecode |-
17		disjdif2	Could not format ( ( ( _Right ` A ) i^i ( _Left ` A ) ) = (/) -> ( ( _Right ` A ) \ ( _Left ` A ) ) = ( _Right ` A ) ) : No typesetting found for |- ( ( ( _Right ` A ) i^i ( _Left ` A ) ) = (/) -> ( ( _Right ` A ) \ ( _Left ` A ) ) = ( _Right ` A ) ) with typecode |-
18	16 17	syl	Could not format ( ( ( A e. No /\ B e. No /\ ( bday ` A ) = ( bday ` B ) ) /\ ( _Left ` A ) = ( _Left ` B ) ) -> ( ( _Right ` A ) \ ( _Left ` A ) ) = ( _Right ` A ) ) : No typesetting found for |- ( ( ( A e. No /\ B e. No /\ ( bday ` A ) = ( bday ` B ) ) /\ ( _Left ` A ) = ( _Left ` B ) ) -> ( ( _Right ` A ) \ ( _Left ` A ) ) = ( _Right ` A ) ) with typecode |-
19	11 18	eqtrid	Could not format ( ( ( A e. No /\ B e. No /\ ( bday ` A ) = ( bday ` B ) ) /\ ( _Left ` A ) = ( _Left ` B ) ) -> ( ( ( _Left ` A ) u. ( _Right ` A ) ) \ ( _Left ` A ) ) = ( _Right ` A ) ) : No typesetting found for |- ( ( ( A e. No /\ B e. No /\ ( bday ` A ) = ( bday ` B ) ) /\ ( _Left ` A ) = ( _Left ` B ) ) -> ( ( ( _Left ` A ) u. ( _Right ` A ) ) \ ( _Left ` A ) ) = ( _Right ` A ) ) with typecode |-
20		difundir	Could not format ( ( ( _Left ` B ) u. ( _Right ` B ) ) \ ( _Left ` B ) ) = ( ( ( _Left ` B ) \ ( _Left ` B ) ) u. ( ( _Right ` B ) \ ( _Left ` B ) ) ) : No typesetting found for |- ( ( ( _Left ` B ) u. ( _Right ` B ) ) \ ( _Left ` B ) ) = ( ( ( _Left ` B ) \ ( _Left ` B ) ) u. ( ( _Right ` B ) \ ( _Left ` B ) ) ) with typecode |-
21		difid	Could not format ( ( _Left ` B ) \ ( _Left ` B ) ) = (/) : No typesetting found for |- ( ( _Left ` B ) \ ( _Left ` B ) ) = (/) with typecode |-
22	21	uneq1i	Could not format ( ( ( _Left ` B ) \ ( _Left ` B ) ) u. ( ( _Right ` B ) \ ( _Left ` B ) ) ) = ( (/) u. ( ( _Right ` B ) \ ( _Left ` B ) ) ) : No typesetting found for |- ( ( ( _Left ` B ) \ ( _Left ` B ) ) u. ( ( _Right ` B ) \ ( _Left ` B ) ) ) = ( (/) u. ( ( _Right ` B ) \ ( _Left ` B ) ) ) with typecode |-
23		0un	Could not format ( (/) u. ( ( _Right ` B ) \ ( _Left ` B ) ) ) = ( ( _Right ` B ) \ ( _Left ` B ) ) : No typesetting found for |- ( (/) u. ( ( _Right ` B ) \ ( _Left ` B ) ) ) = ( ( _Right ` B ) \ ( _Left ` B ) ) with typecode |-
24	20 22 23	3eqtri	Could not format ( ( ( _Left ` B ) u. ( _Right ` B ) ) \ ( _Left ` B ) ) = ( ( _Right ` B ) \ ( _Left ` B ) ) : No typesetting found for |- ( ( ( _Left ` B ) u. ( _Right ` B ) ) \ ( _Left ` B ) ) = ( ( _Right ` B ) \ ( _Left ` B ) ) with typecode |-
25		incom	Could not format ( ( _Left ` B ) i^i ( _Right ` B ) ) = ( ( _Right ` B ) i^i ( _Left ` B ) ) : No typesetting found for |- ( ( _Left ` B ) i^i ( _Right ` B ) ) = ( ( _Right ` B ) i^i ( _Left ` B ) ) with typecode |-
26		lltropt	Could not format ( _Left ` B ) <
27		ssltdisj	Could not format ( ( _Left ` B ) < ( ( _Left ` B ) i^i ( _Right ` B ) ) = (/) ) : No typesetting found for |- ( ( _Left ` B ) < ( ( _Left ` B ) i^i ( _Right ` B ) ) = (/) ) with typecode |-
28	26 27	mp1i	Could not format ( ( ( A e. No /\ B e. No /\ ( bday ` A ) = ( bday ` B ) ) /\ ( _Left ` A ) = ( _Left ` B ) ) -> ( ( _Left ` B ) i^i ( _Right ` B ) ) = (/) ) : No typesetting found for |- ( ( ( A e. No /\ B e. No /\ ( bday ` A ) = ( bday ` B ) ) /\ ( _Left ` A ) = ( _Left ` B ) ) -> ( ( _Left ` B ) i^i ( _Right ` B ) ) = (/) ) with typecode |-
29	25 28	eqtr3id	Could not format ( ( ( A e. No /\ B e. No /\ ( bday ` A ) = ( bday ` B ) ) /\ ( _Left ` A ) = ( _Left ` B ) ) -> ( ( _Right ` B ) i^i ( _Left ` B ) ) = (/) ) : No typesetting found for |- ( ( ( A e. No /\ B e. No /\ ( bday ` A ) = ( bday ` B ) ) /\ ( _Left ` A ) = ( _Left ` B ) ) -> ( ( _Right ` B ) i^i ( _Left ` B ) ) = (/) ) with typecode |-
30		disjdif2	Could not format ( ( ( _Right ` B ) i^i ( _Left ` B ) ) = (/) -> ( ( _Right ` B ) \ ( _Left ` B ) ) = ( _Right ` B ) ) : No typesetting found for |- ( ( ( _Right ` B ) i^i ( _Left ` B ) ) = (/) -> ( ( _Right ` B ) \ ( _Left ` B ) ) = ( _Right ` B ) ) with typecode |-
31	29 30	syl	Could not format ( ( ( A e. No /\ B e. No /\ ( bday ` A ) = ( bday ` B ) ) /\ ( _Left ` A ) = ( _Left ` B ) ) -> ( ( _Right ` B ) \ ( _Left ` B ) ) = ( _Right ` B ) ) : No typesetting found for |- ( ( ( A e. No /\ B e. No /\ ( bday ` A ) = ( bday ` B ) ) /\ ( _Left ` A ) = ( _Left ` B ) ) -> ( ( _Right ` B ) \ ( _Left ` B ) ) = ( _Right ` B ) ) with typecode |-
32	24 31	eqtrid	Could not format ( ( ( A e. No /\ B e. No /\ ( bday ` A ) = ( bday ` B ) ) /\ ( _Left ` A ) = ( _Left ` B ) ) -> ( ( ( _Left ` B ) u. ( _Right ` B ) ) \ ( _Left ` B ) ) = ( _Right ` B ) ) : No typesetting found for |- ( ( ( A e. No /\ B e. No /\ ( bday ` A ) = ( bday ` B ) ) /\ ( _Left ` A ) = ( _Left ` B ) ) -> ( ( ( _Left ` B ) u. ( _Right ` B ) ) \ ( _Left ` B ) ) = ( _Right ` B ) ) with typecode |-
33	6 19 32	3eqtr3d	Could not format ( ( ( A e. No /\ B e. No /\ ( bday ` A ) = ( bday ` B ) ) /\ ( _Left ` A ) = ( _Left ` B ) ) -> ( _Right ` A ) = ( _Right ` B ) ) : No typesetting found for |- ( ( ( A e. No /\ B e. No /\ ( bday ` A ) = ( bday ` B ) ) /\ ( _Left ` A ) = ( _Left ` B ) ) -> ( _Right ` A ) = ( _Right ` B ) ) with typecode |-
34	3 33	oveq12d	Could not format ( ( ( A e. No /\ B e. No /\ ( bday ` A ) = ( bday ` B ) ) /\ ( _Left ` A ) = ( _Left ` B ) ) -> ( ( _Left ` A ) |s ( _Right ` A ) ) = ( ( _Left ` B ) |s ( _Right ` B ) ) ) : No typesetting found for |- ( ( ( A e. No /\ B e. No /\ ( bday ` A ) = ( bday ` B ) ) /\ ( _Left ` A ) = ( _Left ` B ) ) -> ( ( _Left ` A ) |s ( _Right ` A ) ) = ( ( _Left ` B ) |s ( _Right ` B ) ) ) with typecode |-
35		simpl1	Could not format ( ( ( A e. No /\ B e. No /\ ( bday ` A ) = ( bday ` B ) ) /\ ( _Left ` A ) = ( _Left ` B ) ) -> A e. No ) : No typesetting found for |- ( ( ( A e. No /\ B e. No /\ ( bday ` A ) = ( bday ` B ) ) /\ ( _Left ` A ) = ( _Left ` B ) ) -> A e. No ) with typecode |-
36		lrcut	Could not format ( A e. No -> ( ( _Left ` A ) |s ( _Right ` A ) ) = A ) : No typesetting found for |- ( A e. No -> ( ( _Left ` A ) |s ( _Right ` A ) ) = A ) with typecode |-
37	35 36	syl	Could not format ( ( ( A e. No /\ B e. No /\ ( bday ` A ) = ( bday ` B ) ) /\ ( _Left ` A ) = ( _Left ` B ) ) -> ( ( _Left ` A ) |s ( _Right ` A ) ) = A ) : No typesetting found for |- ( ( ( A e. No /\ B e. No /\ ( bday ` A ) = ( bday ` B ) ) /\ ( _Left ` A ) = ( _Left ` B ) ) -> ( ( _Left ` A ) |s ( _Right ` A ) ) = A ) with typecode |-
38		simpl2	Could not format ( ( ( A e. No /\ B e. No /\ ( bday ` A ) = ( bday ` B ) ) /\ ( _Left ` A ) = ( _Left ` B ) ) -> B e. No ) : No typesetting found for |- ( ( ( A e. No /\ B e. No /\ ( bday ` A ) = ( bday ` B ) ) /\ ( _Left ` A ) = ( _Left ` B ) ) -> B e. No ) with typecode |-
39		lrcut	Could not format ( B e. No -> ( ( _Left ` B ) |s ( _Right ` B ) ) = B ) : No typesetting found for |- ( B e. No -> ( ( _Left ` B ) |s ( _Right ` B ) ) = B ) with typecode |-
40	38 39	syl	Could not format ( ( ( A e. No /\ B e. No /\ ( bday ` A ) = ( bday ` B ) ) /\ ( _Left ` A ) = ( _Left ` B ) ) -> ( ( _Left ` B ) |s ( _Right ` B ) ) = B ) : No typesetting found for |- ( ( ( A e. No /\ B e. No /\ ( bday ` A ) = ( bday ` B ) ) /\ ( _Left ` A ) = ( _Left ` B ) ) -> ( ( _Left ` B ) |s ( _Right ` B ) ) = B ) with typecode |-
41	34 37 40	3eqtr3d	Could not format ( ( ( A e. No /\ B e. No /\ ( bday ` A ) = ( bday ` B ) ) /\ ( _Left ` A ) = ( _Left ` B ) ) -> A = B ) : No typesetting found for |- ( ( ( A e. No /\ B e. No /\ ( bday ` A ) = ( bday ` B ) ) /\ ( _Left ` A ) = ( _Left ` B ) ) -> A = B ) with typecode |-
42	41	ex	Could not format ( ( A e. No /\ B e. No /\ ( bday ` A ) = ( bday ` B ) ) -> ( ( _Left ` A ) = ( _Left ` B ) -> A = B ) ) : No typesetting found for |- ( ( A e. No /\ B e. No /\ ( bday ` A ) = ( bday ` B ) ) -> ( ( _Left ` A ) = ( _Left ` B ) -> A = B ) ) with typecode |-
43	2 42	impbid2	Could not format ( ( A e. No /\ B e. No /\ ( bday ` A ) = ( bday ` B ) ) -> ( A = B <-> ( _Left ` A ) = ( _Left ` B ) ) ) : No typesetting found for |- ( ( A e. No /\ B e. No /\ ( bday ` A ) = ( bday ` B ) ) -> ( A = B <-> ( _Left ` A ) = ( _Left ` B ) ) ) with typecode |-
44	1 43	orbi12d	Could not format ( ( A e. No /\ B e. No /\ ( bday ` A ) = ( bday ` B ) ) -> ( ( A ( ( _Left ` A ) C. ( _Left ` B ) \/ ( _Left ` A ) = ( _Left ` B ) ) ) ) : No typesetting found for |- ( ( A e. No /\ B e. No /\ ( bday ` A ) = ( bday ` B ) ) -> ( ( A ( ( _Left ` A ) C. ( _Left ` B ) \/ ( _Left ` A ) = ( _Left ` B ) ) ) ) with typecode |-
45		sleloe	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\to \left(A{\le }_{s}B\leftrightarrow \left(A{<}_{s}B\vee A=B\right)\right)$$
46	45	3adant3	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\wedge \mathrm{bday}\left(A\right)=\mathrm{bday}\left(B\right)\right)\to \left(A{\le }_{s}B\leftrightarrow \left(A{<}_{s}B\vee A=B\right)\right)$$
47		sspss	Could not format ( ( _Left ` A ) C_ ( _Left ` B ) <-> ( ( _Left ` A ) C. ( _Left ` B ) \/ ( _Left ` A ) = ( _Left ` B ) ) ) : No typesetting found for |- ( ( _Left ` A ) C_ ( _Left ` B ) <-> ( ( _Left ` A ) C. ( _Left ` B ) \/ ( _Left ` A ) = ( _Left ` B ) ) ) with typecode |-
48	47	a1i	Could not format ( ( A e. No /\ B e. No /\ ( bday ` A ) = ( bday ` B ) ) -> ( ( _Left ` A ) C_ ( _Left ` B ) <-> ( ( _Left ` A ) C. ( _Left ` B ) \/ ( _Left ` A ) = ( _Left ` B ) ) ) ) : No typesetting found for |- ( ( A e. No /\ B e. No /\ ( bday ` A ) = ( bday ` B ) ) -> ( ( _Left ` A ) C_ ( _Left ` B ) <-> ( ( _Left ` A ) C. ( _Left ` B ) \/ ( _Left ` A ) = ( _Left ` B ) ) ) ) with typecode |-
49	44 46 48	3bitr4d	Could not format ( ( A e. No /\ B e. No /\ ( bday ` A ) = ( bday ` B ) ) -> ( A <_s B <-> ( _Left ` A ) C_ ( _Left ` B ) ) ) : No typesetting found for |- ( ( A e. No /\ B e. No /\ ( bday ` A ) = ( bday ` B ) ) -> ( A <_s B <-> ( _Left ` A ) C_ ( _Left ` B ) ) ) with typecode |-