ssltun2

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

		Ref	Expression
	Assertion	ssltun2	$⊢ (A ≪_{s} B \land A ≪_{s} C) \to A ≪_{s} (B \cup C)$

Proof

Step	Hyp	Ref	Expression
1		ssltex1	$⊢ A ≪_{s} B \to A \in V$
2	1	adantr	$⊢ (A ≪_{s} B \land A ≪_{s} C) \to A \in V$
3		ssltex2	$⊢ A ≪_{s} B \to B \in V$
4	3	adantr	$⊢ (A ≪_{s} B \land A ≪_{s} C) \to B \in V$
5		ssltex2	$⊢ A ≪_{s} C \to C \in V$
6	5	adantl	$⊢ (A ≪_{s} B \land A ≪_{s} C) \to C \in V$
7	4 6	unexd	$⊢ (A ≪_{s} B \land A ≪_{s} C) \to B \cup C \in V$
8		ssltss1	$⊢ A ≪_{s} B \to A \subseteq No$
9	8	adantr	$⊢ (A ≪_{s} B \land A ≪_{s} C) \to A \subseteq No$
10		ssltss2	$⊢ A ≪_{s} B \to B \subseteq No$
11	10	adantr	$⊢ (A ≪_{s} B \land A ≪_{s} C) \to B \subseteq No$
12		ssltss2	$⊢ A ≪_{s} C \to C \subseteq No$
13	12	adantl	$⊢ (A ≪_{s} B \land A ≪_{s} C) \to C \subseteq No$
14	11 13	unssd	$⊢ (A ≪_{s} B \land A ≪_{s} C) \to B \cup C \subseteq No$
15		elun	$⊢ y \in (B \cup C) \leftrightarrow (y \in B \lor y \in C)$
16		ssltsepc	$⊢ (A ≪_{s} B \land x \in A \land y \in B) \to x <_{s} y$
17	16	3exp	$⊢ A ≪_{s} B \to (x \in A \to (y \in B \to x <_{s} y))$
18	17	adantr	$⊢ (A ≪_{s} B \land A ≪_{s} C) \to (x \in A \to (y \in B \to x <_{s} y))$
19	18	com3r	$⊢ y \in B \to ((A ≪_{s} B \land A ≪_{s} C) \to (x \in A \to x <_{s} y))$
20		ssltsepc	$⊢ (A ≪_{s} C \land x \in A \land y \in C) \to x <_{s} y$
21	20	3exp	$⊢ A ≪_{s} C \to (x \in A \to (y \in C \to x <_{s} y))$
22	21	adantl	$⊢ (A ≪_{s} B \land A ≪_{s} C) \to (x \in A \to (y \in C \to x <_{s} y))$
23	22	com3r	$⊢ y \in C \to ((A ≪_{s} B \land A ≪_{s} C) \to (x \in A \to x <_{s} y))$
24	19 23	jaoi	$⊢ (y \in B \lor y \in C) \to ((A ≪_{s} B \land A ≪_{s} C) \to (x \in A \to x <_{s} y))$
25	15 24	sylbi	$⊢ y \in (B \cup C) \to ((A ≪_{s} B \land A ≪_{s} C) \to (x \in A \to x <_{s} y))$
26	25	3imp231	$⊢ ((A ≪_{s} B \land A ≪_{s} C) \land x \in A \land y \in (B \cup C)) \to x <_{s} y$
27	2 7 9 14 26	ssltd	$⊢ (A ≪_{s} B \land A ≪_{s} C) \to A ≪_{s} (B \cup C)$

Metamath Proof Explorer

Theorem ssltun2

Proof