sltrec

Description: A comparison law for surreals considered as cuts of sets of surreals. (Contributed by Scott Fenton, 11-Dec-2021)

		Ref	Expression
	Assertion	sltrec	$⊢ ((A ≪_{s} B \land C ≪_{s} D) \land (X = A \|_{s} B \land Y = C \|_{s} D)) \to (X <_{s} Y \leftrightarrow (\exists c \in C X \leq_{s} c \lor \exists b \in B b \leq_{s} Y))$

Proof

Step	Hyp	Ref	Expression
1		simplr	$⊢ ((A ≪_{s} B \land C ≪_{s} D) \land (X = A \|_{s} B \land Y = C \|_{s} D)) \to C ≪_{s} D$
2		simpll	$⊢ ((A ≪_{s} B \land C ≪_{s} D) \land (X = A \|_{s} B \land Y = C \|_{s} D)) \to A ≪_{s} B$
3		simprr	$⊢ ((A ≪_{s} B \land C ≪_{s} D) \land (X = A \|_{s} B \land Y = C \|_{s} D)) \to Y = C \|_{s} D$
4		simprl	$⊢ ((A ≪_{s} B \land C ≪_{s} D) \land (X = A \|_{s} B \land Y = C \|_{s} D)) \to X = A \|_{s} B$
5		slerec	$⊢ ((C ≪_{s} D \land A ≪_{s} B) \land (Y = C \|_{s} D \land X = A \|_{s} B)) \to (Y \leq_{s} X \leftrightarrow (\forall b \in B Y <_{s} b \land \forall c \in C c <_{s} X))$
6	1 2 3 4 5	syl22anc	$⊢ ((A ≪_{s} B \land C ≪_{s} D) \land (X = A \|_{s} B \land Y = C \|_{s} D)) \to (Y \leq_{s} X \leftrightarrow (\forall b \in B Y <_{s} b \land \forall c \in C c <_{s} X))$
7		ancom	$⊢ (\forall b \in B Y <_{s} b \land \forall c \in C c <_{s} X) \leftrightarrow (\forall c \in C c <_{s} X \land \forall b \in B Y <_{s} b)$
8	6 7	bitrdi	$⊢ ((A ≪_{s} B \land C ≪_{s} D) \land (X = A \|_{s} B \land Y = C \|_{s} D)) \to (Y \leq_{s} X \leftrightarrow (\forall c \in C c <_{s} X \land \forall b \in B Y <_{s} b))$
9		scutcut	$⊢ C ≪_{s} D \to (C \|_{s} D \in No \land C ≪_{s} \{C \|_{s} D\} \land \{C \|_{s} D\} ≪_{s} D)$
10	9	simp1d	$⊢ C ≪_{s} D \to C \|_{s} D \in No$
11	10	ad2antlr	$⊢ ((A ≪_{s} B \land C ≪_{s} D) \land (X = A \|_{s} B \land Y = C \|_{s} D)) \to C \|_{s} D \in No$
12	3 11	eqeltrd	$⊢ ((A ≪_{s} B \land C ≪_{s} D) \land (X = A \|_{s} B \land Y = C \|_{s} D)) \to Y \in No$
13		scutcut	$⊢ A ≪_{s} B \to (A \|_{s} B \in No \land A ≪_{s} \{A \|_{s} B\} \land \{A \|_{s} B\} ≪_{s} B)$
14	13	simp1d	$⊢ A ≪_{s} B \to A \|_{s} B \in No$
15	14	ad2antrr	$⊢ ((A ≪_{s} B \land C ≪_{s} D) \land (X = A \|_{s} B \land Y = C \|_{s} D)) \to A \|_{s} B \in No$
16	4 15	eqeltrd	$⊢ ((A ≪_{s} B \land C ≪_{s} D) \land (X = A \|_{s} B \land Y = C \|_{s} D)) \to X \in No$
17		slenlt	$⊢ (Y \in No \land X \in No) \to (Y \leq_{s} X \leftrightarrow \neg X <_{s} Y)$
18	12 16 17	syl2anc	$⊢ ((A ≪_{s} B \land C ≪_{s} D) \land (X = A \|_{s} B \land Y = C \|_{s} D)) \to (Y \leq_{s} X \leftrightarrow \neg X <_{s} Y)$
19		ssltss1	$⊢ C ≪_{s} D \to C \subseteq No$
20	19	ad2antlr	$⊢ ((A ≪_{s} B \land C ≪_{s} D) \land (X = A \|_{s} B \land Y = C \|_{s} D)) \to C \subseteq No$
21	20	sselda	$⊢ (((A ≪_{s} B \land C ≪_{s} D) \land (X = A \|_{s} B \land Y = C \|_{s} D)) \land c \in C) \to c \in No$
22	16	adantr	$⊢ (((A ≪_{s} B \land C ≪_{s} D) \land (X = A \|_{s} B \land Y = C \|_{s} D)) \land c \in C) \to X \in No$
23		sltnle	$⊢ (c \in No \land X \in No) \to (c <_{s} X \leftrightarrow \neg X \leq_{s} c)$
24	21 22 23	syl2anc	$⊢ (((A ≪_{s} B \land C ≪_{s} D) \land (X = A \|_{s} B \land Y = C \|_{s} D)) \land c \in C) \to (c <_{s} X \leftrightarrow \neg X \leq_{s} c)$
25	24	ralbidva	$⊢ ((A ≪_{s} B \land C ≪_{s} D) \land (X = A \|_{s} B \land Y = C \|_{s} D)) \to (\forall c \in C c <_{s} X \leftrightarrow \forall c \in C \neg X \leq_{s} c)$
26	12	adantr	$⊢ (((A ≪_{s} B \land C ≪_{s} D) \land (X = A \|_{s} B \land Y = C \|_{s} D)) \land b \in B) \to Y \in No$
27		ssltss2	$⊢ A ≪_{s} B \to B \subseteq No$
28	27	ad2antrr	$⊢ ((A ≪_{s} B \land C ≪_{s} D) \land (X = A \|_{s} B \land Y = C \|_{s} D)) \to B \subseteq No$
29	28	sselda	$⊢ (((A ≪_{s} B \land C ≪_{s} D) \land (X = A \|_{s} B \land Y = C \|_{s} D)) \land b \in B) \to b \in No$
30		sltnle	$⊢ (Y \in No \land b \in No) \to (Y <_{s} b \leftrightarrow \neg b \leq_{s} Y)$
31	26 29 30	syl2anc	$⊢ (((A ≪_{s} B \land C ≪_{s} D) \land (X = A \|_{s} B \land Y = C \|_{s} D)) \land b \in B) \to (Y <_{s} b \leftrightarrow \neg b \leq_{s} Y)$
32	31	ralbidva	$⊢ ((A ≪_{s} B \land C ≪_{s} D) \land (X = A \|_{s} B \land Y = C \|_{s} D)) \to (\forall b \in B Y <_{s} b \leftrightarrow \forall b \in B \neg b \leq_{s} Y)$
33	25 32	anbi12d	$⊢ ((A ≪_{s} B \land C ≪_{s} D) \land (X = A \|_{s} B \land Y = C \|_{s} D)) \to ((\forall c \in C c <_{s} X \land \forall b \in B Y <_{s} b) \leftrightarrow (\forall c \in C \neg X \leq_{s} c \land \forall b \in B \neg b \leq_{s} Y))$
34		ralnex	$⊢ \forall c \in C \neg X \leq_{s} c \leftrightarrow \neg \exists c \in C X \leq_{s} c$
35		ralnex	$⊢ \forall b \in B \neg b \leq_{s} Y \leftrightarrow \neg \exists b \in B b \leq_{s} Y$
36	34 35	anbi12i	$⊢ (\forall c \in C \neg X \leq_{s} c \land \forall b \in B \neg b \leq_{s} Y) \leftrightarrow (\neg \exists c \in C X \leq_{s} c \land \neg \exists b \in B b \leq_{s} Y)$
37		ioran	$⊢ \neg (\exists c \in C X \leq_{s} c \lor \exists b \in B b \leq_{s} Y) \leftrightarrow (\neg \exists c \in C X \leq_{s} c \land \neg \exists b \in B b \leq_{s} Y)$
38	36 37	bitr4i	$⊢ (\forall c \in C \neg X \leq_{s} c \land \forall b \in B \neg b \leq_{s} Y) \leftrightarrow \neg (\exists c \in C X \leq_{s} c \lor \exists b \in B b \leq_{s} Y)$
39	33 38	bitrdi	$⊢ ((A ≪_{s} B \land C ≪_{s} D) \land (X = A \|_{s} B \land Y = C \|_{s} D)) \to ((\forall c \in C c <_{s} X \land \forall b \in B Y <_{s} b) \leftrightarrow \neg (\exists c \in C X \leq_{s} c \lor \exists b \in B b \leq_{s} Y))$
40	8 18 39	3bitr3d	$⊢ ((A ≪_{s} B \land C ≪_{s} D) \land (X = A \|_{s} B \land Y = C \|_{s} D)) \to (\neg X <_{s} Y \leftrightarrow \neg (\exists c \in C X \leq_{s} c \lor \exists b \in B b \leq_{s} Y))$
41	40	con4bid	$⊢ ((A ≪_{s} B \land C ≪_{s} D) \land (X = A \|_{s} B \land Y = C \|_{s} D)) \to (X <_{s} Y \leftrightarrow (\exists c \in C X \leq_{s} c \lor \exists b \in B b \leq_{s} Y))$

Metamath Proof Explorer

Theorem sltrec

Proof