infunsdom1

Description: The union of two sets that are strictly dominated by the infinite set X is also dominated by X . This version of infunsdom assumes additionally that A is the smaller of the two. (Contributed by Mario Carneiro, 14-Dec-2013) (Revised by Mario Carneiro, 3-May-2015)

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

Proof

Step	Hyp	Ref	Expression
1		simprl	$⊢ ((X \in dom card \land ω ≼ X) \land (A ≼ B \land B ≺ X)) \to A ≼ B$
2		domsdomtr	$⊢ (A ≼ B \land B ≺ ω) \to A ≺ ω$
3	1 2	sylan	$⊢ (((X \in dom card \land ω ≼ X) \land (A ≼ B \land B ≺ X)) \land B ≺ ω) \to A ≺ ω$
4		unfi2	$⊢ (A ≺ ω \land B ≺ ω) \to (A \cup B) ≺ ω$
5	3 4	sylancom	$⊢ (((X \in dom card \land ω ≼ X) \land (A ≼ B \land B ≺ X)) \land B ≺ ω) \to (A \cup B) ≺ ω$
6		simpllr	$⊢ (((X \in dom card \land ω ≼ X) \land (A ≼ B \land B ≺ X)) \land B ≺ ω) \to ω ≼ X$
7		sdomdomtr	$⊢ ((A \cup B) ≺ ω \land ω ≼ X) \to (A \cup B) ≺ X$
8	5 6 7	syl2anc	$⊢ (((X \in dom card \land ω ≼ X) \land (A ≼ B \land B ≺ X)) \land B ≺ ω) \to (A \cup B) ≺ X$
9		omelon	$⊢ ω \in On$
10		onenon	$⊢ ω \in On \to ω \in dom card$
11	9 10	ax-mp	$⊢ ω \in dom card$
12		simpll	$⊢ ((X \in dom card \land ω ≼ X) \land (A ≼ B \land B ≺ X)) \to X \in dom card$
13		sdomdom	$⊢ B ≺ X \to B ≼ X$
14	13	ad2antll	$⊢ ((X \in dom card \land ω ≼ X) \land (A ≼ B \land B ≺ X)) \to B ≼ X$
15		numdom	$⊢ (X \in dom card \land B ≼ X) \to B \in dom card$
16	12 14 15	syl2anc	$⊢ ((X \in dom card \land ω ≼ X) \land (A ≼ B \land B ≺ X)) \to B \in dom card$
17		domtri2	$⊢ (ω \in dom card \land B \in dom card) \to (ω ≼ B \leftrightarrow \neg B ≺ ω)$
18	11 16 17	sylancr	$⊢ ((X \in dom card \land ω ≼ X) \land (A ≼ B \land B ≺ X)) \to (ω ≼ B \leftrightarrow \neg B ≺ ω)$
19	18	biimpar	$⊢ (((X \in dom card \land ω ≼ X) \land (A ≼ B \land B ≺ X)) \land \neg B ≺ ω) \to ω ≼ B$
20		uncom	$⊢ A \cup B = B \cup A$
21	16	adantr	$⊢ (((X \in dom card \land ω ≼ X) \land (A ≼ B \land B ≺ X)) \land ω ≼ B) \to B \in dom card$
22		simpr	$⊢ (((X \in dom card \land ω ≼ X) \land (A ≼ B \land B ≺ X)) \land ω ≼ B) \to ω ≼ B$
23	1	adantr	$⊢ (((X \in dom card \land ω ≼ X) \land (A ≼ B \land B ≺ X)) \land ω ≼ B) \to A ≼ B$
24		infunabs	$⊢ (B \in dom card \land ω ≼ B \land A ≼ B) \to (B \cup A) \approx B$
25	21 22 23 24	syl3anc	$⊢ (((X \in dom card \land ω ≼ X) \land (A ≼ B \land B ≺ X)) \land ω ≼ B) \to (B \cup A) \approx B$
26	20 25	eqbrtrid	$⊢ (((X \in dom card \land ω ≼ X) \land (A ≼ B \land B ≺ X)) \land ω ≼ B) \to (A \cup B) \approx B$
27		simplrr	$⊢ (((X \in dom card \land ω ≼ X) \land (A ≼ B \land B ≺ X)) \land ω ≼ B) \to B ≺ X$
28		ensdomtr	$⊢ ((A \cup B) \approx B \land B ≺ X) \to (A \cup B) ≺ X$
29	26 27 28	syl2anc	$⊢ (((X \in dom card \land ω ≼ X) \land (A ≼ B \land B ≺ X)) \land ω ≼ B) \to (A \cup B) ≺ X$
30	19 29	syldan	$⊢ (((X \in dom card \land ω ≼ X) \land (A ≼ B \land B ≺ X)) \land \neg B ≺ ω) \to (A \cup B) ≺ X$
31	8 30	pm2.61dan	$⊢ ((X \in dom card \land ω ≼ X) \land (A ≼ B \land B ≺ X)) \to (A \cup B) ≺ X$

Metamath Proof Explorer

Theorem infunsdom1

Proof