ltsrec

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

		Ref	Expression
	Assertion	ltsrec	$⊢ ((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	1 2 3 4	lesrecd	$⊢ ((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))$
6		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)$
7	5 6	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))$
8		cutcuts	$⊢ C ≪_{s} D \to (C \|_{s} D \in No \land C ≪_{s} \{C \|_{s} D\} \land \{C \|_{s} D\} ≪_{s} D)$
9	8	simp1d	$⊢ C ≪_{s} D \to C \|_{s} D \in No$
10	9	ad2antlr	$⊢ ((A ≪_{s} B \land C ≪_{s} D) \land (X = A \|_{s} B \land Y = C \|_{s} D)) \to C \|_{s} D \in No$
11	3 10	eqeltrd	$⊢ ((A ≪_{s} B \land C ≪_{s} D) \land (X = A \|_{s} B \land Y = C \|_{s} D)) \to Y \in No$
12		cutcuts	$⊢ A ≪_{s} B \to (A \|_{s} B \in No \land A ≪_{s} \{A \|_{s} B\} \land \{A \|_{s} B\} ≪_{s} B)$
13	12	simp1d	$⊢ A ≪_{s} B \to A \|_{s} B \in No$
14	13	ad2antrr	$⊢ ((A ≪_{s} B \land C ≪_{s} D) \land (X = A \|_{s} B \land Y = C \|_{s} D)) \to A \|_{s} B \in No$
15	4 14	eqeltrd	$⊢ ((A ≪_{s} B \land C ≪_{s} D) \land (X = A \|_{s} B \land Y = C \|_{s} D)) \to X \in No$
16		lenlts	$⊢ (Y \in No \land X \in No) \to (Y \leq_{s} X \leftrightarrow \neg X <_{s} Y)$
17	11 15 16	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)$
18		sltsss1	$⊢ C ≪_{s} D \to C \subseteq No$
19	18	ad2antlr	$⊢ ((A ≪_{s} B \land C ≪_{s} D) \land (X = A \|_{s} B \land Y = C \|_{s} D)) \to C \subseteq No$
20	19	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$
21	15	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$
22		ltnles	$⊢ (c \in No \land X \in No) \to (c <_{s} X \leftrightarrow \neg X \leq_{s} c)$
23	20 21 22	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)$
24	23	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)$
25	11	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$
26		sltsss2	$⊢ A ≪_{s} B \to B \subseteq No$
27	26	ad2antrr	$⊢ ((A ≪_{s} B \land C ≪_{s} D) \land (X = A \|_{s} B \land Y = C \|_{s} D)) \to B \subseteq No$
28	27	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$
29		ltnles	$⊢ (Y \in No \land b \in No) \to (Y <_{s} b \leftrightarrow \neg b \leq_{s} Y)$
30	25 28 29	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)$
31	30	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)$
32	24 31	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))$
33		ralnex	$⊢ \forall c \in C \neg X \leq_{s} c \leftrightarrow \neg \exists c \in C X \leq_{s} c$
34		ralnex	$⊢ \forall b \in B \neg b \leq_{s} Y \leftrightarrow \neg \exists b \in B b \leq_{s} Y$
35	33 34	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)$
36		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)$
37	35 36	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)$
38	32 37	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))$
39	7 17 38	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))$
40	39	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 ltsrec

Proof