sslttr

Description: Transitive law for surreal set less than. (Contributed by Scott Fenton, 9-Dec-2021)

		Ref	Expression
	Assertion	sslttr	$⊢ (A ≪_{s} B \land B ≪_{s} C \land B \neq \emptyset) \to A ≪_{s} C$

Proof

Step	Hyp	Ref	Expression
1		n0	$⊢ B \neq \emptyset \leftrightarrow \exists y y \in B$
2		ssltex1	$⊢ A ≪_{s} B \to A \in V$
3		ssltex2	$⊢ B ≪_{s} C \to C \in V$
4	2 3	anim12i	$⊢ (A ≪_{s} B \land B ≪_{s} C) \to (A \in V \land C \in V)$
5	4	adantl	$⊢ (y \in B \land (A ≪_{s} B \land B ≪_{s} C)) \to (A \in V \land C \in V)$
6		ssltss1	$⊢ A ≪_{s} B \to A \subseteq No$
7	6	ad2antrl	$⊢ (y \in B \land (A ≪_{s} B \land B ≪_{s} C)) \to A \subseteq No$
8		ssltss2	$⊢ B ≪_{s} C \to C \subseteq No$
9	8	ad2antll	$⊢ (y \in B \land (A ≪_{s} B \land B ≪_{s} C)) \to C \subseteq No$
10	7	adantr	$⊢ ((y \in B \land (A ≪_{s} B \land B ≪_{s} C)) \land (x \in A \land z \in C)) \to A \subseteq No$
11		simprl	$⊢ ((y \in B \land (A ≪_{s} B \land B ≪_{s} C)) \land (x \in A \land z \in C)) \to x \in A$
12	10 11	sseldd	$⊢ ((y \in B \land (A ≪_{s} B \land B ≪_{s} C)) \land (x \in A \land z \in C)) \to x \in No$
13		ssltss1	$⊢ B ≪_{s} C \to B \subseteq No$
14	13	ad2antll	$⊢ (y \in B \land (A ≪_{s} B \land B ≪_{s} C)) \to B \subseteq No$
15	14	adantr	$⊢ ((y \in B \land (A ≪_{s} B \land B ≪_{s} C)) \land (x \in A \land z \in C)) \to B \subseteq No$
16		simpll	$⊢ ((y \in B \land (A ≪_{s} B \land B ≪_{s} C)) \land (x \in A \land z \in C)) \to y \in B$
17	15 16	sseldd	$⊢ ((y \in B \land (A ≪_{s} B \land B ≪_{s} C)) \land (x \in A \land z \in C)) \to y \in No$
18	9	adantr	$⊢ ((y \in B \land (A ≪_{s} B \land B ≪_{s} C)) \land (x \in A \land z \in C)) \to C \subseteq No$
19		simprr	$⊢ ((y \in B \land (A ≪_{s} B \land B ≪_{s} C)) \land (x \in A \land z \in C)) \to z \in C$
20	18 19	sseldd	$⊢ ((y \in B \land (A ≪_{s} B \land B ≪_{s} C)) \land (x \in A \land z \in C)) \to z \in No$
21		ssltsep	$⊢ A ≪_{s} B \to \forall x \in A \forall y \in B x <_{s} y$
22	21	ad2antrl	$⊢ (y \in B \land (A ≪_{s} B \land B ≪_{s} C)) \to \forall x \in A \forall y \in B x <_{s} y$
23	22	adantr	$⊢ ((y \in B \land (A ≪_{s} B \land B ≪_{s} C)) \land (x \in A \land z \in C)) \to \forall x \in A \forall y \in B x <_{s} y$
24		rsp	$⊢ \forall x \in A \forall y \in B x <_{s} y \to (x \in A \to \forall y \in B x <_{s} y)$
25	23 11 24	sylc	$⊢ ((y \in B \land (A ≪_{s} B \land B ≪_{s} C)) \land (x \in A \land z \in C)) \to \forall y \in B x <_{s} y$
26		rsp	$⊢ \forall y \in B x <_{s} y \to (y \in B \to x <_{s} y)$
27	25 16 26	sylc	$⊢ ((y \in B \land (A ≪_{s} B \land B ≪_{s} C)) \land (x \in A \land z \in C)) \to x <_{s} y$
28		ssltsep	$⊢ B ≪_{s} C \to \forall y \in B \forall z \in C y <_{s} z$
29	28	ad2antll	$⊢ (y \in B \land (A ≪_{s} B \land B ≪_{s} C)) \to \forall y \in B \forall z \in C y <_{s} z$
30	29	adantr	$⊢ ((y \in B \land (A ≪_{s} B \land B ≪_{s} C)) \land (x \in A \land z \in C)) \to \forall y \in B \forall z \in C y <_{s} z$
31		rsp	$⊢ \forall y \in B \forall z \in C y <_{s} z \to (y \in B \to \forall z \in C y <_{s} z)$
32	30 16 31	sylc	$⊢ ((y \in B \land (A ≪_{s} B \land B ≪_{s} C)) \land (x \in A \land z \in C)) \to \forall z \in C y <_{s} z$
33		rsp	$⊢ \forall z \in C y <_{s} z \to (z \in C \to y <_{s} z)$
34	32 19 33	sylc	$⊢ ((y \in B \land (A ≪_{s} B \land B ≪_{s} C)) \land (x \in A \land z \in C)) \to y <_{s} z$
35	12 17 20 27 34	slttrd	$⊢ ((y \in B \land (A ≪_{s} B \land B ≪_{s} C)) \land (x \in A \land z \in C)) \to x <_{s} z$
36	35	ralrimivva	$⊢ (y \in B \land (A ≪_{s} B \land B ≪_{s} C)) \to \forall x \in A \forall z \in C x <_{s} z$
37	7 9 36	3jca	$⊢ (y \in B \land (A ≪_{s} B \land B ≪_{s} C)) \to (A \subseteq No \land C \subseteq No \land \forall x \in A \forall z \in C x <_{s} z)$
38		brsslt	$⊢ A ≪_{s} C \leftrightarrow ((A \in V \land C \in V) \land (A \subseteq No \land C \subseteq No \land \forall x \in A \forall z \in C x <_{s} z))$
39	5 37 38	sylanbrc	$⊢ (y \in B \land (A ≪_{s} B \land B ≪_{s} C)) \to A ≪_{s} C$
40	39	ex	$⊢ y \in B \to ((A ≪_{s} B \land B ≪_{s} C) \to A ≪_{s} C)$
41	40	exlimiv	$⊢ \exists y y \in B \to ((A ≪_{s} B \land B ≪_{s} C) \to A ≪_{s} C)$
42	1 41	sylbi	$⊢ B \neq \emptyset \to ((A ≪_{s} B \land B ≪_{s} C) \to A ≪_{s} C)$
43	42	com12	$⊢ (A ≪_{s} B \land B ≪_{s} C) \to (B \neq \emptyset \to A ≪_{s} C)$
44	43	3impia	$⊢ (A ≪_{s} B \land B ≪_{s} C \land B \neq \emptyset) \to A ≪_{s} C$

Metamath Proof Explorer

Theorem sslttr

Proof