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	$⊢ (A \in No \land B \in No \land bday (A) = bday (B)) \to (A \leq_{s} B \leftrightarrow L (A) \subseteq L (B))$

Proof

Step	Hyp	Ref	Expression
1		sltlpss	$⊢ (A \in No \land B \in No \land bday (A) = bday (B)) \to (A <_{s} B \leftrightarrow L (A) \subset L (B))$
2		fveq2	$⊢ A = B \to L (A) = L (B)$
3		simpr	$⊢ ((A \in No \land B \in No \land bday (A) = bday (B)) \land L (A) = L (B)) \to L (A) = L (B)$
4		lruneq	$⊢ (A \in No \land B \in No \land bday (A) = bday (B)) \to L (A) \cup R (A) = L (B) \cup R (B)$
5	4	adantr	$⊢ ((A \in No \land B \in No \land bday (A) = bday (B)) \land L (A) = L (B)) \to L (A) \cup R (A) = L (B) \cup R (B)$
6	5 3	difeq12d	$⊢ ((A \in No \land B \in No \land bday (A) = bday (B)) \land L (A) = L (B)) \to (L (A) \cup R (A)) ∖ L (A) = (L (B) \cup R (B)) ∖ L (B)$
7		difundir	$⊢ (L (A) \cup R (A)) ∖ L (A) = (L (A) ∖ L (A)) \cup (R (A) ∖ L (A))$
8		difid	$⊢ L (A) ∖ L (A) = \emptyset$
9	8	uneq1i	$⊢ (L (A) ∖ L (A)) \cup (R (A) ∖ L (A)) = \emptyset \cup (R (A) ∖ L (A))$
10		0un	$⊢ \emptyset \cup (R (A) ∖ L (A)) = R (A) ∖ L (A)$
11	7 9 10	3eqtri	$⊢ (L (A) \cup R (A)) ∖ L (A) = R (A) ∖ L (A)$
12		incom	$⊢ L (A) \cap R (A) = R (A) \cap L (A)$
13		lltropt	$⊢ L (A) ≪_{s} R (A)$
14		ssltdisj	$⊢ L (A) ≪_{s} R (A) \to L (A) \cap R (A) = \emptyset$
15	13 14	mp1i	$⊢ ((A \in No \land B \in No \land bday (A) = bday (B)) \land L (A) = L (B)) \to L (A) \cap R (A) = \emptyset$
16	12 15	eqtr3id	$⊢ ((A \in No \land B \in No \land bday (A) = bday (B)) \land L (A) = L (B)) \to R (A) \cap L (A) = \emptyset$
17		disjdif2	$⊢ R (A) \cap L (A) = \emptyset \to R (A) ∖ L (A) = R (A)$
18	16 17	syl	$⊢ ((A \in No \land B \in No \land bday (A) = bday (B)) \land L (A) = L (B)) \to R (A) ∖ L (A) = R (A)$
19	11 18	eqtrid	$⊢ ((A \in No \land B \in No \land bday (A) = bday (B)) \land L (A) = L (B)) \to (L (A) \cup R (A)) ∖ L (A) = R (A)$
20		difundir	$⊢ (L (B) \cup R (B)) ∖ L (B) = (L (B) ∖ L (B)) \cup (R (B) ∖ L (B))$
21		difid	$⊢ L (B) ∖ L (B) = \emptyset$
22	21	uneq1i	$⊢ (L (B) ∖ L (B)) \cup (R (B) ∖ L (B)) = \emptyset \cup (R (B) ∖ L (B))$
23		0un	$⊢ \emptyset \cup (R (B) ∖ L (B)) = R (B) ∖ L (B)$
24	20 22 23	3eqtri	$⊢ (L (B) \cup R (B)) ∖ L (B) = R (B) ∖ L (B)$
25		incom	$⊢ L (B) \cap R (B) = R (B) \cap L (B)$
26		lltropt	$⊢ L (B) ≪_{s} R (B)$
27		ssltdisj	$⊢ L (B) ≪_{s} R (B) \to L (B) \cap R (B) = \emptyset$
28	26 27	mp1i	$⊢ ((A \in No \land B \in No \land bday (A) = bday (B)) \land L (A) = L (B)) \to L (B) \cap R (B) = \emptyset$
29	25 28	eqtr3id	$⊢ ((A \in No \land B \in No \land bday (A) = bday (B)) \land L (A) = L (B)) \to R (B) \cap L (B) = \emptyset$
30		disjdif2	$⊢ R (B) \cap L (B) = \emptyset \to R (B) ∖ L (B) = R (B)$
31	29 30	syl	$⊢ ((A \in No \land B \in No \land bday (A) = bday (B)) \land L (A) = L (B)) \to R (B) ∖ L (B) = R (B)$
32	24 31	eqtrid	$⊢ ((A \in No \land B \in No \land bday (A) = bday (B)) \land L (A) = L (B)) \to (L (B) \cup R (B)) ∖ L (B) = R (B)$
33	6 19 32	3eqtr3d	$⊢ ((A \in No \land B \in No \land bday (A) = bday (B)) \land L (A) = L (B)) \to R (A) = R (B)$
34	3 33	oveq12d	$⊢ ((A \in No \land B \in No \land bday (A) = bday (B)) \land L (A) = L (B)) \to L (A) \|_{s} R (A) = L (B) \|_{s} R (B)$
35		simpl1	$⊢ ((A \in No \land B \in No \land bday (A) = bday (B)) \land L (A) = L (B)) \to A \in No$
36		lrcut	$⊢ A \in No \to L (A) \|_{s} R (A) = A$
37	35 36	syl	$⊢ ((A \in No \land B \in No \land bday (A) = bday (B)) \land L (A) = L (B)) \to L (A) \|_{s} R (A) = A$
38		simpl2	$⊢ ((A \in No \land B \in No \land bday (A) = bday (B)) \land L (A) = L (B)) \to B \in No$
39		lrcut	$⊢ B \in No \to L (B) \|_{s} R (B) = B$
40	38 39	syl	$⊢ ((A \in No \land B \in No \land bday (A) = bday (B)) \land L (A) = L (B)) \to L (B) \|_{s} R (B) = B$
41	34 37 40	3eqtr3d	$⊢ ((A \in No \land B \in No \land bday (A) = bday (B)) \land L (A) = L (B)) \to A = B$
42	41	ex	$⊢ (A \in No \land B \in No \land bday (A) = bday (B)) \to (L (A) = L (B) \to A = B)$
43	2 42	impbid2	$⊢ (A \in No \land B \in No \land bday (A) = bday (B)) \to (A = B \leftrightarrow L (A) = L (B))$
44	1 43	orbi12d	$⊢ (A \in No \land B \in No \land bday (A) = bday (B)) \to ((A <_{s} B \lor A = B) \leftrightarrow (L (A) \subset L (B) \lor L (A) = L (B)))$
45		sleloe	$⊢ (A \in No \land B \in No) \to (A \leq_{s} B \leftrightarrow (A <_{s} B \lor A = B))$
46	45	3adant3	$⊢ (A \in No \land B \in No \land bday (A) = bday (B)) \to (A \leq_{s} B \leftrightarrow (A <_{s} B \lor A = B))$
47		sspss	$⊢ L (A) \subseteq L (B) \leftrightarrow (L (A) \subset L (B) \lor L (A) = L (B))$
48	47	a1i	$⊢ (A \in No \land B \in No \land bday (A) = bday (B)) \to (L (A) \subseteq L (B) \leftrightarrow (L (A) \subset L (B) \lor L (A) = L (B)))$
49	44 46 48	3bitr4d	$⊢ (A \in No \land B \in No \land bday (A) = bday (B)) \to (A \leq_{s} B \leftrightarrow L (A) \subseteq L (B))$

Metamath Proof Explorer

Theorem slelss

Proof