sltstr

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

		Ref	Expression
	Assertion	sltstr	$⊢ (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		sltsex1	$⊢ A ≪_{s} B \to A \in V$
3	2	3ad2ant2	$⊢ (y \in B \land A ≪_{s} B \land B ≪_{s} C) \to A \in V$
4		sltsex2	$⊢ B ≪_{s} C \to C \in V$
5	4	3ad2ant3	$⊢ (y \in B \land A ≪_{s} B \land B ≪_{s} C) \to C \in V$
6		sltsss1	$⊢ A ≪_{s} B \to A \subseteq No$
7	6	3ad2ant2	$⊢ (y \in B \land A ≪_{s} B \land B ≪_{s} C) \to A \subseteq No$
8		sltsss2	$⊢ B ≪_{s} C \to C \subseteq No$
9	8	3ad2ant3	$⊢ (y \in B \land A ≪_{s} B \land B ≪_{s} C) \to C \subseteq No$
10	7	3ad2ant1	$⊢ ((y \in B \land A ≪_{s} B \land B ≪_{s} C) \land x \in A \land z \in C) \to A \subseteq No$
11		simp2	$⊢ ((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		sltsss2	$⊢ A ≪_{s} B \to B \subseteq No$
14	13	3ad2ant2	$⊢ (y \in B \land A ≪_{s} B \land B ≪_{s} C) \to B \subseteq No$
15	14	3ad2ant1	$⊢ ((y \in B \land A ≪_{s} B \land B ≪_{s} C) \land x \in A \land z \in C) \to B \subseteq No$
16		simp11	$⊢ ((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	3ad2ant1	$⊢ ((y \in B \land A ≪_{s} B \land B ≪_{s} C) \land x \in A \land z \in C) \to C \subseteq No$
19		simp3	$⊢ ((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		simp12	$⊢ ((y \in B \land A ≪_{s} B \land B ≪_{s} C) \land x \in A \land z \in C) \to A ≪_{s} B$
22	21 11 16	sltssepcd	$⊢ ((y \in B \land A ≪_{s} B \land B ≪_{s} C) \land x \in A \land z \in C) \to x <_{s} y$
23		simp13	$⊢ ((y \in B \land A ≪_{s} B \land B ≪_{s} C) \land x \in A \land z \in C) \to B ≪_{s} C$
24	23 16 19	sltssepcd	$⊢ ((y \in B \land A ≪_{s} B \land B ≪_{s} C) \land x \in A \land z \in C) \to y <_{s} z$
25	12 17 20 22 24	ltstrd	$⊢ ((y \in B \land A ≪_{s} B \land B ≪_{s} C) \land x \in A \land z \in C) \to x <_{s} z$
26	3 5 7 9 25	sltsd	$⊢ (y \in B \land A ≪_{s} B \land B ≪_{s} C) \to A ≪_{s} C$
27	26	3exp	$⊢ y \in B \to (A ≪_{s} B \to (B ≪_{s} C \to A ≪_{s} C))$
28	27	exlimiv	$⊢ \exists y y \in B \to (A ≪_{s} B \to (B ≪_{s} C \to A ≪_{s} C))$
29	1 28	sylbi	$⊢ B \neq \emptyset \to (A ≪_{s} B \to (B ≪_{s} C \to A ≪_{s} C))$
30	29	3imp231	$⊢ (A ≪_{s} B \land B ≪_{s} C \land B \neq \emptyset) \to A ≪_{s} C$

Metamath Proof Explorer

Theorem sltstr

Proof