ssltun1

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

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

Proof

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

Metamath Proof Explorer

Theorem ssltun1

Proof