djuunxp

Description: The union of a disjoint union and its inversion is the Cartesian product of an unordered pair and the union of the left and right classes of the disjoint unions. (Proposed by GL, 4-Jul-2022.) (Contributed by AV, 4-Jul-2022)

		Ref	Expression
	Assertion	djuunxp	$⊢ (A ⊔︀ B) \cup (B ⊔︀ A) = \{\emptyset, 1_{𝑜}\} \times (A \cup B)$

Proof

Step	Hyp	Ref	Expression
1		djuss	$⊢ (A ⊔︀ B) \subseteq \{\emptyset, 1_{𝑜}\} \times (A \cup B)$
2		djuss	$⊢ (B ⊔︀ A) \subseteq \{\emptyset, 1_{𝑜}\} \times (B \cup A)$
3		uncom	$⊢ A \cup B = B \cup A$
4	3	xpeq2i	$⊢ \{\emptyset, 1_{𝑜}\} \times (A \cup B) = \{\emptyset, 1_{𝑜}\} \times (B \cup A)$
5	2 4	sseqtrri	$⊢ (B ⊔︀ A) \subseteq \{\emptyset, 1_{𝑜}\} \times (A \cup B)$
6	1 5	unssi	$⊢ (A ⊔︀ B) \cup (B ⊔︀ A) \subseteq \{\emptyset, 1_{𝑜}\} \times (A \cup B)$
7		elxpi	$⊢ x \in (\{\emptyset, 1_{𝑜}\} \times (A \cup B)) \to \exists y \exists z (x = ⟨y, z⟩ \land (y \in \{\emptyset, 1_{𝑜}\} \land z \in (A \cup B)))$
8		vex	$⊢ y \in V$
9	8	elpr	$⊢ y \in \{\emptyset, 1_{𝑜}\} \leftrightarrow (y = \emptyset \lor y = 1_{𝑜})$
10		elun	$⊢ z \in (A \cup B) \leftrightarrow (z \in A \lor z \in B)$
11		velsn	$⊢ y \in \{\emptyset\} \leftrightarrow y = \emptyset$
12	11	biimpri	$⊢ y = \emptyset \to y \in \{\emptyset\}$
13	12	anim1i	$⊢ (y = \emptyset \land z \in A) \to (y \in \{\emptyset\} \land z \in A)$
14	13	ancoms	$⊢ (z \in A \land y = \emptyset) \to (y \in \{\emptyset\} \land z \in A)$
15		opelxp	$⊢ ⟨y, z⟩ \in (\{\emptyset\} \times A) \leftrightarrow (y \in \{\emptyset\} \land z \in A)$
16	14 15	sylibr	$⊢ (z \in A \land y = \emptyset) \to ⟨y, z⟩ \in (\{\emptyset\} \times A)$
17	16	orcd	$⊢ (z \in A \land y = \emptyset) \to (⟨y, z⟩ \in (\{\emptyset\} \times A) \lor ⟨y, z⟩ \in (\{1_{𝑜}\} \times B))$
18		elun	$⊢ ⟨y, z⟩ \in ((\{\emptyset\} \times A) \cup (\{1_{𝑜}\} \times B)) \leftrightarrow (⟨y, z⟩ \in (\{\emptyset\} \times A) \lor ⟨y, z⟩ \in (\{1_{𝑜}\} \times B))$
19	17 18	sylibr	$⊢ (z \in A \land y = \emptyset) \to ⟨y, z⟩ \in ((\{\emptyset\} \times A) \cup (\{1_{𝑜}\} \times B))$
20	19	orcd	$⊢ (z \in A \land y = \emptyset) \to (⟨y, z⟩ \in ((\{\emptyset\} \times A) \cup (\{1_{𝑜}\} \times B)) \lor (⟨y, z⟩ \in (\{\emptyset\} \times B) \lor ⟨y, z⟩ \in (\{1_{𝑜}\} \times A)))$
21	20	ex	$⊢ z \in A \to (y = \emptyset \to (⟨y, z⟩ \in ((\{\emptyset\} \times A) \cup (\{1_{𝑜}\} \times B)) \lor (⟨y, z⟩ \in (\{\emptyset\} \times B) \lor ⟨y, z⟩ \in (\{1_{𝑜}\} \times A))))$
22	12	anim1i	$⊢ (y = \emptyset \land z \in B) \to (y \in \{\emptyset\} \land z \in B)$
23	22	ancoms	$⊢ (z \in B \land y = \emptyset) \to (y \in \{\emptyset\} \land z \in B)$
24		opelxp	$⊢ ⟨y, z⟩ \in (\{\emptyset\} \times B) \leftrightarrow (y \in \{\emptyset\} \land z \in B)$
25	23 24	sylibr	$⊢ (z \in B \land y = \emptyset) \to ⟨y, z⟩ \in (\{\emptyset\} \times B)$
26	25	orcd	$⊢ (z \in B \land y = \emptyset) \to (⟨y, z⟩ \in (\{\emptyset\} \times B) \lor ⟨y, z⟩ \in (\{1_{𝑜}\} \times A))$
27	26	olcd	$⊢ (z \in B \land y = \emptyset) \to (⟨y, z⟩ \in ((\{\emptyset\} \times A) \cup (\{1_{𝑜}\} \times B)) \lor (⟨y, z⟩ \in (\{\emptyset\} \times B) \lor ⟨y, z⟩ \in (\{1_{𝑜}\} \times A)))$
28	27	ex	$⊢ z \in B \to (y = \emptyset \to (⟨y, z⟩ \in ((\{\emptyset\} \times A) \cup (\{1_{𝑜}\} \times B)) \lor (⟨y, z⟩ \in (\{\emptyset\} \times B) \lor ⟨y, z⟩ \in (\{1_{𝑜}\} \times A))))$
29	21 28	jaoi	$⊢ (z \in A \lor z \in B) \to (y = \emptyset \to (⟨y, z⟩ \in ((\{\emptyset\} \times A) \cup (\{1_{𝑜}\} \times B)) \lor (⟨y, z⟩ \in (\{\emptyset\} \times B) \lor ⟨y, z⟩ \in (\{1_{𝑜}\} \times A))))$
30	29	com12	$⊢ y = \emptyset \to ((z \in A \lor z \in B) \to (⟨y, z⟩ \in ((\{\emptyset\} \times A) \cup (\{1_{𝑜}\} \times B)) \lor (⟨y, z⟩ \in (\{\emptyset\} \times B) \lor ⟨y, z⟩ \in (\{1_{𝑜}\} \times A))))$
31		velsn	$⊢ y \in \{1_{𝑜}\} \leftrightarrow y = 1_{𝑜}$
32	31	biimpri	$⊢ y = 1_{𝑜} \to y \in \{1_{𝑜}\}$
33	32	anim1i	$⊢ (y = 1_{𝑜} \land z \in A) \to (y \in \{1_{𝑜}\} \land z \in A)$
34	33	ancoms	$⊢ (z \in A \land y = 1_{𝑜}) \to (y \in \{1_{𝑜}\} \land z \in A)$
35		opelxp	$⊢ ⟨y, z⟩ \in (\{1_{𝑜}\} \times A) \leftrightarrow (y \in \{1_{𝑜}\} \land z \in A)$
36	34 35	sylibr	$⊢ (z \in A \land y = 1_{𝑜}) \to ⟨y, z⟩ \in (\{1_{𝑜}\} \times A)$
37	36	olcd	$⊢ (z \in A \land y = 1_{𝑜}) \to (⟨y, z⟩ \in (\{\emptyset\} \times B) \lor ⟨y, z⟩ \in (\{1_{𝑜}\} \times A))$
38	37	olcd	$⊢ (z \in A \land y = 1_{𝑜}) \to (⟨y, z⟩ \in ((\{\emptyset\} \times A) \cup (\{1_{𝑜}\} \times B)) \lor (⟨y, z⟩ \in (\{\emptyset\} \times B) \lor ⟨y, z⟩ \in (\{1_{𝑜}\} \times A)))$
39	38	ex	$⊢ z \in A \to (y = 1_{𝑜} \to (⟨y, z⟩ \in ((\{\emptyset\} \times A) \cup (\{1_{𝑜}\} \times B)) \lor (⟨y, z⟩ \in (\{\emptyset\} \times B) \lor ⟨y, z⟩ \in (\{1_{𝑜}\} \times A))))$
40	32	anim1i	$⊢ (y = 1_{𝑜} \land z \in B) \to (y \in \{1_{𝑜}\} \land z \in B)$
41	40	ancoms	$⊢ (z \in B \land y = 1_{𝑜}) \to (y \in \{1_{𝑜}\} \land z \in B)$
42		opelxp	$⊢ ⟨y, z⟩ \in (\{1_{𝑜}\} \times B) \leftrightarrow (y \in \{1_{𝑜}\} \land z \in B)$
43	41 42	sylibr	$⊢ (z \in B \land y = 1_{𝑜}) \to ⟨y, z⟩ \in (\{1_{𝑜}\} \times B)$
44	43	olcd	$⊢ (z \in B \land y = 1_{𝑜}) \to (⟨y, z⟩ \in (\{\emptyset\} \times A) \lor ⟨y, z⟩ \in (\{1_{𝑜}\} \times B))$
45	44 18	sylibr	$⊢ (z \in B \land y = 1_{𝑜}) \to ⟨y, z⟩ \in ((\{\emptyset\} \times A) \cup (\{1_{𝑜}\} \times B))$
46	45	orcd	$⊢ (z \in B \land y = 1_{𝑜}) \to (⟨y, z⟩ \in ((\{\emptyset\} \times A) \cup (\{1_{𝑜}\} \times B)) \lor (⟨y, z⟩ \in (\{\emptyset\} \times B) \lor ⟨y, z⟩ \in (\{1_{𝑜}\} \times A)))$
47	46	ex	$⊢ z \in B \to (y = 1_{𝑜} \to (⟨y, z⟩ \in ((\{\emptyset\} \times A) \cup (\{1_{𝑜}\} \times B)) \lor (⟨y, z⟩ \in (\{\emptyset\} \times B) \lor ⟨y, z⟩ \in (\{1_{𝑜}\} \times A))))$
48	39 47	jaoi	$⊢ (z \in A \lor z \in B) \to (y = 1_{𝑜} \to (⟨y, z⟩ \in ((\{\emptyset\} \times A) \cup (\{1_{𝑜}\} \times B)) \lor (⟨y, z⟩ \in (\{\emptyset\} \times B) \lor ⟨y, z⟩ \in (\{1_{𝑜}\} \times A))))$
49	48	com12	$⊢ y = 1_{𝑜} \to ((z \in A \lor z \in B) \to (⟨y, z⟩ \in ((\{\emptyset\} \times A) \cup (\{1_{𝑜}\} \times B)) \lor (⟨y, z⟩ \in (\{\emptyset\} \times B) \lor ⟨y, z⟩ \in (\{1_{𝑜}\} \times A))))$
50	30 49	jaoi	$⊢ (y = \emptyset \lor y = 1_{𝑜}) \to ((z \in A \lor z \in B) \to (⟨y, z⟩ \in ((\{\emptyset\} \times A) \cup (\{1_{𝑜}\} \times B)) \lor (⟨y, z⟩ \in (\{\emptyset\} \times B) \lor ⟨y, z⟩ \in (\{1_{𝑜}\} \times A))))$
51	50	imp	$⊢ ((y = \emptyset \lor y = 1_{𝑜}) \land (z \in A \lor z \in B)) \to (⟨y, z⟩ \in ((\{\emptyset\} \times A) \cup (\{1_{𝑜}\} \times B)) \lor (⟨y, z⟩ \in (\{\emptyset\} \times B) \lor ⟨y, z⟩ \in (\{1_{𝑜}\} \times A)))$
52	9 10 51	syl2anb	$⊢ (y \in \{\emptyset, 1_{𝑜}\} \land z \in (A \cup B)) \to (⟨y, z⟩ \in ((\{\emptyset\} \times A) \cup (\{1_{𝑜}\} \times B)) \lor (⟨y, z⟩ \in (\{\emptyset\} \times B) \lor ⟨y, z⟩ \in (\{1_{𝑜}\} \times A)))$
53		elun	$⊢ ⟨y, z⟩ \in ((A ⊔︀ B) \cup (B ⊔︀ A)) \leftrightarrow (⟨y, z⟩ \in (A ⊔︀ B) \lor ⟨y, z⟩ \in (B ⊔︀ A))$
54		df-dju	$⊢ (A ⊔︀ B) = (\{\emptyset\} \times A) \cup (\{1_{𝑜}\} \times B)$
55	54	eleq2i	$⊢ ⟨y, z⟩ \in (A ⊔︀ B) \leftrightarrow ⟨y, z⟩ \in ((\{\emptyset\} \times A) \cup (\{1_{𝑜}\} \times B))$
56		df-dju	$⊢ (B ⊔︀ A) = (\{\emptyset\} \times B) \cup (\{1_{𝑜}\} \times A)$
57	56	eleq2i	$⊢ ⟨y, z⟩ \in (B ⊔︀ A) \leftrightarrow ⟨y, z⟩ \in ((\{\emptyset\} \times B) \cup (\{1_{𝑜}\} \times A))$
58		elun	$⊢ ⟨y, z⟩ \in ((\{\emptyset\} \times B) \cup (\{1_{𝑜}\} \times A)) \leftrightarrow (⟨y, z⟩ \in (\{\emptyset\} \times B) \lor ⟨y, z⟩ \in (\{1_{𝑜}\} \times A))$
59	57 58	bitri	$⊢ ⟨y, z⟩ \in (B ⊔︀ A) \leftrightarrow (⟨y, z⟩ \in (\{\emptyset\} \times B) \lor ⟨y, z⟩ \in (\{1_{𝑜}\} \times A))$
60	55 59	orbi12i	$⊢ (⟨y, z⟩ \in (A ⊔︀ B) \lor ⟨y, z⟩ \in (B ⊔︀ A)) \leftrightarrow (⟨y, z⟩ \in ((\{\emptyset\} \times A) \cup (\{1_{𝑜}\} \times B)) \lor (⟨y, z⟩ \in (\{\emptyset\} \times B) \lor ⟨y, z⟩ \in (\{1_{𝑜}\} \times A)))$
61	53 60	bitri	$⊢ ⟨y, z⟩ \in ((A ⊔︀ B) \cup (B ⊔︀ A)) \leftrightarrow (⟨y, z⟩ \in ((\{\emptyset\} \times A) \cup (\{1_{𝑜}\} \times B)) \lor (⟨y, z⟩ \in (\{\emptyset\} \times B) \lor ⟨y, z⟩ \in (\{1_{𝑜}\} \times A)))$
62	52 61	sylibr	$⊢ (y \in \{\emptyset, 1_{𝑜}\} \land z \in (A \cup B)) \to ⟨y, z⟩ \in ((A ⊔︀ B) \cup (B ⊔︀ A))$
63	62	adantl	$⊢ (x = ⟨y, z⟩ \land (y \in \{\emptyset, 1_{𝑜}\} \land z \in (A \cup B))) \to ⟨y, z⟩ \in ((A ⊔︀ B) \cup (B ⊔︀ A))$
64		eleq1	$⊢ x = ⟨y, z⟩ \to (x \in ((A ⊔︀ B) \cup (B ⊔︀ A)) \leftrightarrow ⟨y, z⟩ \in ((A ⊔︀ B) \cup (B ⊔︀ A)))$
65	64	adantr	$⊢ (x = ⟨y, z⟩ \land (y \in \{\emptyset, 1_{𝑜}\} \land z \in (A \cup B))) \to (x \in ((A ⊔︀ B) \cup (B ⊔︀ A)) \leftrightarrow ⟨y, z⟩ \in ((A ⊔︀ B) \cup (B ⊔︀ A)))$
66	63 65	mpbird	$⊢ (x = ⟨y, z⟩ \land (y \in \{\emptyset, 1_{𝑜}\} \land z \in (A \cup B))) \to x \in ((A ⊔︀ B) \cup (B ⊔︀ A))$
67	66	exlimivv	$⊢ \exists y \exists z (x = ⟨y, z⟩ \land (y \in \{\emptyset, 1_{𝑜}\} \land z \in (A \cup B))) \to x \in ((A ⊔︀ B) \cup (B ⊔︀ A))$
68	7 67	syl	$⊢ x \in (\{\emptyset, 1_{𝑜}\} \times (A \cup B)) \to x \in ((A ⊔︀ B) \cup (B ⊔︀ A))$
69	68	ssriv	$⊢ \{\emptyset, 1_{𝑜}\} \times (A \cup B) \subseteq (A ⊔︀ B) \cup (B ⊔︀ A)$
70	6 69	eqssi	$⊢ (A ⊔︀ B) \cup (B ⊔︀ A) = \{\emptyset, 1_{𝑜}\} \times (A \cup B)$

Metamath Proof Explorer

Theorem djuunxp

Proof