unxpdom2

		Ref	Expression
	Assertion	unxpdom2	$⊢ (1_{𝑜} ≺ A \land B ≼ A) \to (A \cup B) ≼ (A \times A)$

Proof

Step	Hyp	Ref	Expression
1		relsdom	$⊢ Rel ≺$
2	1	brrelex2i	$⊢ 1_{𝑜} ≺ A \to A \in V$
3	2	adantr	$⊢ (1_{𝑜} ≺ A \land B ≼ A) \to A \in V$
4		1onn	$⊢ 1_{𝑜} \in ω$
5		xpsneng	$⊢ (A \in V \land 1_{𝑜} \in ω) \to (A \times \{1_{𝑜}\}) \approx A$
6	3 4 5	sylancl	$⊢ (1_{𝑜} ≺ A \land B ≼ A) \to (A \times \{1_{𝑜}\}) \approx A$
7	6	ensymd	$⊢ (1_{𝑜} ≺ A \land B ≼ A) \to A \approx (A \times \{1_{𝑜}\})$
8		endom	$⊢ A \approx (A \times \{1_{𝑜}\}) \to A ≼ (A \times \{1_{𝑜}\})$
9	7 8	syl	$⊢ (1_{𝑜} ≺ A \land B ≼ A) \to A ≼ (A \times \{1_{𝑜}\})$
10		simpr	$⊢ (1_{𝑜} ≺ A \land B ≼ A) \to B ≼ A$
11		0ex	$⊢ \emptyset \in V$
12		xpsneng	$⊢ (A \in V \land \emptyset \in V) \to (A \times \{\emptyset\}) \approx A$
13	3 11 12	sylancl	$⊢ (1_{𝑜} ≺ A \land B ≼ A) \to (A \times \{\emptyset\}) \approx A$
14	13	ensymd	$⊢ (1_{𝑜} ≺ A \land B ≼ A) \to A \approx (A \times \{\emptyset\})$
15		domentr	$⊢ (B ≼ A \land A \approx (A \times \{\emptyset\})) \to B ≼ (A \times \{\emptyset\})$
16	10 14 15	syl2anc	$⊢ (1_{𝑜} ≺ A \land B ≼ A) \to B ≼ (A \times \{\emptyset\})$
17		1n0	$⊢ 1_{𝑜} \neq \emptyset$
18		xpsndisj	$⊢ 1_{𝑜} \neq \emptyset \to (A \times \{1_{𝑜}\}) \cap (A \times \{\emptyset\}) = \emptyset$
19	17 18	mp1i	$⊢ (1_{𝑜} ≺ A \land B ≼ A) \to (A \times \{1_{𝑜}\}) \cap (A \times \{\emptyset\}) = \emptyset$
20		undom	$⊢ ((A ≼ (A \times \{1_{𝑜}\}) \land B ≼ (A \times \{\emptyset\})) \land (A \times \{1_{𝑜}\}) \cap (A \times \{\emptyset\}) = \emptyset) \to (A \cup B) ≼ ((A \times \{1_{𝑜}\}) \cup (A \times \{\emptyset\}))$
21	9 16 19 20	syl21anc	$⊢ (1_{𝑜} ≺ A \land B ≼ A) \to (A \cup B) ≼ ((A \times \{1_{𝑜}\}) \cup (A \times \{\emptyset\}))$
22		sdomentr	$⊢ (1_{𝑜} ≺ A \land A \approx (A \times \{1_{𝑜}\})) \to 1_{𝑜} ≺ (A \times \{1_{𝑜}\})$
23	7 22	syldan	$⊢ (1_{𝑜} ≺ A \land B ≼ A) \to 1_{𝑜} ≺ (A \times \{1_{𝑜}\})$
24		sdomentr	$⊢ (1_{𝑜} ≺ A \land A \approx (A \times \{\emptyset\})) \to 1_{𝑜} ≺ (A \times \{\emptyset\})$
25	14 24	syldan	$⊢ (1_{𝑜} ≺ A \land B ≼ A) \to 1_{𝑜} ≺ (A \times \{\emptyset\})$
26		unxpdom	$⊢ (1_{𝑜} ≺ (A \times \{1_{𝑜}\}) \land 1_{𝑜} ≺ (A \times \{\emptyset\})) \to ((A \times \{1_{𝑜}\}) \cup (A \times \{\emptyset\})) ≼ ((A \times \{1_{𝑜}\}) \times (A \times \{\emptyset\}))$
27	23 25 26	syl2anc	$⊢ (1_{𝑜} ≺ A \land B ≼ A) \to ((A \times \{1_{𝑜}\}) \cup (A \times \{\emptyset\})) ≼ ((A \times \{1_{𝑜}\}) \times (A \times \{\emptyset\}))$
28		xpen	$⊢ ((A \times \{1_{𝑜}\}) \approx A \land (A \times \{\emptyset\}) \approx A) \to ((A \times \{1_{𝑜}\}) \times (A \times \{\emptyset\})) \approx (A \times A)$
29	6 13 28	syl2anc	$⊢ (1_{𝑜} ≺ A \land B ≼ A) \to ((A \times \{1_{𝑜}\}) \times (A \times \{\emptyset\})) \approx (A \times A)$
30		domentr	$⊢ (((A \times \{1_{𝑜}\}) \cup (A \times \{\emptyset\})) ≼ ((A \times \{1_{𝑜}\}) \times (A \times \{\emptyset\})) \land ((A \times \{1_{𝑜}\}) \times (A \times \{\emptyset\})) \approx (A \times A)) \to ((A \times \{1_{𝑜}\}) \cup (A \times \{\emptyset\})) ≼ (A \times A)$
31	27 29 30	syl2anc	$⊢ (1_{𝑜} ≺ A \land B ≼ A) \to ((A \times \{1_{𝑜}\}) \cup (A \times \{\emptyset\})) ≼ (A \times A)$
32		domtr	$⊢ ((A \cup B) ≼ ((A \times \{1_{𝑜}\}) \cup (A \times \{\emptyset\})) \land ((A \times \{1_{𝑜}\}) \cup (A \times \{\emptyset\})) ≼ (A \times A)) \to (A \cup B) ≼ (A \times A)$
33	21 31 32	syl2anc	$⊢ (1_{𝑜} ≺ A \land B ≼ A) \to (A \cup B) ≼ (A \times A)$

Metamath Proof Explorer

Theorem unxpdom2

Proof