This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem djudom1

Description: Ordering law for cardinal addition. Exercise 4.56(f) of Mendelson p. 258. (Contributed by NM, 28-Sep-2004) (Revised by Mario Carneiro, 29-Apr-2015) (Revised by Jim Kingdon, 1-Sep-2023)

		Ref	Expression
	Assertion	djudom1	$⊢ (A ≼ B \land C \in V) \to (A ⊔︀ C) ≼ (B ⊔︀ C)$

Proof

Step	Hyp	Ref	Expression
1		snex	$⊢ \{\emptyset\} \in V$
2	1	xpdom2	$⊢ A ≼ B \to (\{\emptyset\} \times A) ≼ (\{\emptyset\} \times B)$
3		snex	$⊢ \{1_{𝑜}\} \in V$
4		xpexg	$⊢ (\{1_{𝑜}\} \in V \land C \in V) \to \{1_{𝑜}\} \times C \in V$
5	3 4	mpan	$⊢ C \in V \to \{1_{𝑜}\} \times C \in V$
6		domrefg	$⊢ \{1_{𝑜}\} \times C \in V \to (\{1_{𝑜}\} \times C) ≼ (\{1_{𝑜}\} \times C)$
7	5 6	syl	$⊢ C \in V \to (\{1_{𝑜}\} \times C) ≼ (\{1_{𝑜}\} \times C)$
8		xp01disjl	$⊢ (\{\emptyset\} \times B) \cap (\{1_{𝑜}\} \times C) = \emptyset$
9		undom	$⊢ (((\{\emptyset\} \times A) ≼ (\{\emptyset\} \times B) \land (\{1_{𝑜}\} \times C) ≼ (\{1_{𝑜}\} \times C)) \land (\{\emptyset\} \times B) \cap (\{1_{𝑜}\} \times C) = \emptyset) \to ((\{\emptyset\} \times A) \cup (\{1_{𝑜}\} \times C)) ≼ ((\{\emptyset\} \times B) \cup (\{1_{𝑜}\} \times C))$
10	8 9	mpan2	$⊢ ((\{\emptyset\} \times A) ≼ (\{\emptyset\} \times B) \land (\{1_{𝑜}\} \times C) ≼ (\{1_{𝑜}\} \times C)) \to ((\{\emptyset\} \times A) \cup (\{1_{𝑜}\} \times C)) ≼ ((\{\emptyset\} \times B) \cup (\{1_{𝑜}\} \times C))$
11	2 7 10	syl2an	$⊢ (A ≼ B \land C \in V) \to ((\{\emptyset\} \times A) \cup (\{1_{𝑜}\} \times C)) ≼ ((\{\emptyset\} \times B) \cup (\{1_{𝑜}\} \times C))$
12		df-dju	$⊢ (A ⊔︀ C) = (\{\emptyset\} \times A) \cup (\{1_{𝑜}\} \times C)$
13		df-dju	$⊢ (B ⊔︀ C) = (\{\emptyset\} \times B) \cup (\{1_{𝑜}\} \times C)$
14	11 12 13	3brtr4g	$⊢ (A ≼ B \land C \in V) \to (A ⊔︀ C) ≼ (B ⊔︀ C)$