infunsdom

Description: The union of two sets that are strictly dominated by the infinite set X is also strictly dominated by X . (Contributed by Mario Carneiro, 3-May-2015)

		Ref	Expression
	Assertion	infunsdom	$⊢ ((X \in dom card \land ω ≼ X) \land (A ≺ X \land B ≺ X)) \to (A \cup B) ≺ X$

Proof

Step	Hyp	Ref	Expression
1		sdomdom	$⊢ A ≺ B \to A ≼ B$
2		infunsdom1	$⊢ ((X \in dom card \land ω ≼ X) \land (A ≼ B \land B ≺ X)) \to (A \cup B) ≺ X$
3	2	anass1rs	$⊢ (((X \in dom card \land ω ≼ X) \land B ≺ X) \land A ≼ B) \to (A \cup B) ≺ X$
4	3	adantlrl	$⊢ (((X \in dom card \land ω ≼ X) \land (A ≺ X \land B ≺ X)) \land A ≼ B) \to (A \cup B) ≺ X$
5	1 4	sylan2	$⊢ (((X \in dom card \land ω ≼ X) \land (A ≺ X \land B ≺ X)) \land A ≺ B) \to (A \cup B) ≺ X$
6		simpll	$⊢ ((X \in dom card \land ω ≼ X) \land (A ≺ X \land B ≺ X)) \to X \in dom card$
7		sdomdom	$⊢ B ≺ X \to B ≼ X$
8	7	ad2antll	$⊢ ((X \in dom card \land ω ≼ X) \land (A ≺ X \land B ≺ X)) \to B ≼ X$
9		numdom	$⊢ (X \in dom card \land B ≼ X) \to B \in dom card$
10	6 8 9	syl2anc	$⊢ ((X \in dom card \land ω ≼ X) \land (A ≺ X \land B ≺ X)) \to B \in dom card$
11		sdomdom	$⊢ A ≺ X \to A ≼ X$
12	11	ad2antrl	$⊢ ((X \in dom card \land ω ≼ X) \land (A ≺ X \land B ≺ X)) \to A ≼ X$
13		numdom	$⊢ (X \in dom card \land A ≼ X) \to A \in dom card$
14	6 12 13	syl2anc	$⊢ ((X \in dom card \land ω ≼ X) \land (A ≺ X \land B ≺ X)) \to A \in dom card$
15		domtri2	$⊢ (B \in dom card \land A \in dom card) \to (B ≼ A \leftrightarrow \neg A ≺ B)$
16	10 14 15	syl2anc	$⊢ ((X \in dom card \land ω ≼ X) \land (A ≺ X \land B ≺ X)) \to (B ≼ A \leftrightarrow \neg A ≺ B)$
17	16	biimpar	$⊢ (((X \in dom card \land ω ≼ X) \land (A ≺ X \land B ≺ X)) \land \neg A ≺ B) \to B ≼ A$
18		uncom	$⊢ A \cup B = B \cup A$
19		infunsdom1	$⊢ ((X \in dom card \land ω ≼ X) \land (B ≼ A \land A ≺ X)) \to (B \cup A) ≺ X$
20	18 19	eqbrtrid	$⊢ ((X \in dom card \land ω ≼ X) \land (B ≼ A \land A ≺ X)) \to (A \cup B) ≺ X$
21	20	anass1rs	$⊢ (((X \in dom card \land ω ≼ X) \land A ≺ X) \land B ≼ A) \to (A \cup B) ≺ X$
22	21	adantlrr	$⊢ (((X \in dom card \land ω ≼ X) \land (A ≺ X \land B ≺ X)) \land B ≼ A) \to (A \cup B) ≺ X$
23	17 22	syldan	$⊢ (((X \in dom card \land ω ≼ X) \land (A ≺ X \land B ≺ X)) \land \neg A ≺ B) \to (A \cup B) ≺ X$
24	5 23	pm2.61dan	$⊢ ((X \in dom card \land ω ≼ X) \land (A ≺ X \land B ≺ X)) \to (A \cup B) ≺ X$

Metamath Proof Explorer

Theorem infunsdom

Proof