djuun

Description: The disjoint union of two classes is the union of the images of those two classes under right and left injection. (Contributed by Jim Kingdon, 22-Jun-2022)

		Ref	Expression
	Assertion	djuun	$⊢ inl [A] \cup inr [B] = (A ⊔︀ B)$

Proof

Step	Hyp	Ref	Expression
1		elun	$⊢ x \in (inl [A] \cup inr [B]) \leftrightarrow (x \in inl [A] \lor x \in inr [B])$
2		djulf1o	$⊢ inl : V \underset{1-1 onto}{⟶} \{\emptyset\} \times V$
3		f1ofn	$⊢ inl : V \underset{1-1 onto}{⟶} \{\emptyset\} \times V \to inl Fn V$
4	2 3	ax-mp	$⊢ inl Fn V$
5		ssv	$⊢ A \subseteq V$
6		fvelimab	$⊢ (inl Fn V \land A \subseteq V) \to (x \in inl [A] \leftrightarrow \exists u \in A inl (u) = x)$
7	4 5 6	mp2an	$⊢ x \in inl [A] \leftrightarrow \exists u \in A inl (u) = x$
8	7	biimpi	$⊢ x \in inl [A] \to \exists u \in A inl (u) = x$
9		simprr	$⊢ (x \in inl [A] \land (u \in A \land inl (u) = x)) \to inl (u) = x$
10		vex	$⊢ u \in V$
11		opex	$⊢ ⟨\emptyset, u⟩ \in V$
12		opeq2	$⊢ z = u \to ⟨\emptyset, z⟩ = ⟨\emptyset, u⟩$
13		df-inl	$⊢ inl = (z \in V ⟼ ⟨\emptyset, z⟩)$
14	12 13	fvmptg	$⊢ (u \in V \land ⟨\emptyset, u⟩ \in V) \to inl (u) = ⟨\emptyset, u⟩$
15	10 11 14	mp2an	$⊢ inl (u) = ⟨\emptyset, u⟩$
16		0ex	$⊢ \emptyset \in V$
17	16	snid	$⊢ \emptyset \in \{\emptyset\}$
18		opelxpi	$⊢ (\emptyset \in \{\emptyset\} \land u \in A) \to ⟨\emptyset, u⟩ \in (\{\emptyset\} \times A)$
19	17 18	mpan	$⊢ u \in A \to ⟨\emptyset, u⟩ \in (\{\emptyset\} \times A)$
20	19	ad2antrl	$⊢ (x \in inl [A] \land (u \in A \land inl (u) = x)) \to ⟨\emptyset, u⟩ \in (\{\emptyset\} \times A)$
21	15 20	eqeltrid	$⊢ (x \in inl [A] \land (u \in A \land inl (u) = x)) \to inl (u) \in (\{\emptyset\} \times A)$
22	9 21	eqeltrrd	$⊢ (x \in inl [A] \land (u \in A \land inl (u) = x)) \to x \in (\{\emptyset\} \times A)$
23	8 22	rexlimddv	$⊢ x \in inl [A] \to x \in (\{\emptyset\} \times A)$
24		elun1	$⊢ x \in (\{\emptyset\} \times A) \to x \in ((\{\emptyset\} \times A) \cup (\{1_{𝑜}\} \times B))$
25	23 24	syl	$⊢ x \in inl [A] \to x \in ((\{\emptyset\} \times A) \cup (\{1_{𝑜}\} \times B))$
26		df-dju	$⊢ (A ⊔︀ B) = (\{\emptyset\} \times A) \cup (\{1_{𝑜}\} \times B)$
27	25 26	eleqtrrdi	$⊢ x \in inl [A] \to x \in (A ⊔︀ B)$
28		djurf1o	$⊢ inr : V \underset{1-1 onto}{⟶} \{1_{𝑜}\} \times V$
29		f1ofn	$⊢ inr : V \underset{1-1 onto}{⟶} \{1_{𝑜}\} \times V \to inr Fn V$
30	28 29	ax-mp	$⊢ inr Fn V$
31		ssv	$⊢ B \subseteq V$
32		fvelimab	$⊢ (inr Fn V \land B \subseteq V) \to (x \in inr [B] \leftrightarrow \exists u \in B inr (u) = x)$
33	30 31 32	mp2an	$⊢ x \in inr [B] \leftrightarrow \exists u \in B inr (u) = x$
34	33	biimpi	$⊢ x \in inr [B] \to \exists u \in B inr (u) = x$
35		simprr	$⊢ (x \in inr [B] \land (u \in B \land inr (u) = x)) \to inr (u) = x$
36		opex	$⊢ ⟨1_{𝑜}, u⟩ \in V$
37		opeq2	$⊢ z = u \to ⟨1_{𝑜}, z⟩ = ⟨1_{𝑜}, u⟩$
38		df-inr	$⊢ inr = (z \in V ⟼ ⟨1_{𝑜}, z⟩)$
39	37 38	fvmptg	$⊢ (u \in V \land ⟨1_{𝑜}, u⟩ \in V) \to inr (u) = ⟨1_{𝑜}, u⟩$
40	10 36 39	mp2an	$⊢ inr (u) = ⟨1_{𝑜}, u⟩$
41		1oex	$⊢ 1_{𝑜} \in V$
42	41	snid	$⊢ 1_{𝑜} \in \{1_{𝑜}\}$
43		opelxpi	$⊢ (1_{𝑜} \in \{1_{𝑜}\} \land u \in B) \to ⟨1_{𝑜}, u⟩ \in (\{1_{𝑜}\} \times B)$
44	42 43	mpan	$⊢ u \in B \to ⟨1_{𝑜}, u⟩ \in (\{1_{𝑜}\} \times B)$
45	44	ad2antrl	$⊢ (x \in inr [B] \land (u \in B \land inr (u) = x)) \to ⟨1_{𝑜}, u⟩ \in (\{1_{𝑜}\} \times B)$
46	40 45	eqeltrid	$⊢ (x \in inr [B] \land (u \in B \land inr (u) = x)) \to inr (u) \in (\{1_{𝑜}\} \times B)$
47	35 46	eqeltrrd	$⊢ (x \in inr [B] \land (u \in B \land inr (u) = x)) \to x \in (\{1_{𝑜}\} \times B)$
48	34 47	rexlimddv	$⊢ x \in inr [B] \to x \in (\{1_{𝑜}\} \times B)$
49		elun2	$⊢ x \in (\{1_{𝑜}\} \times B) \to x \in ((\{\emptyset\} \times A) \cup (\{1_{𝑜}\} \times B))$
50	48 49	syl	$⊢ x \in inr [B] \to x \in ((\{\emptyset\} \times A) \cup (\{1_{𝑜}\} \times B))$
51	50 26	eleqtrrdi	$⊢ x \in inr [B] \to x \in (A ⊔︀ B)$
52	27 51	jaoi	$⊢ (x \in inl [A] \lor x \in inr [B]) \to x \in (A ⊔︀ B)$
53	1 52	sylbi	$⊢ x \in (inl [A] \cup inr [B]) \to x \in (A ⊔︀ B)$
54	53	ssriv	$⊢ inl [A] \cup inr [B] \subseteq (A ⊔︀ B)$
55		djur	$⊢ x \in (A ⊔︀ B) \to (\exists y \in A x = inl (y) \lor \exists y \in B x = inr (y))$
56		vex	$⊢ y \in V$
57		f1odm	$⊢ inl : V \underset{1-1 onto}{⟶} \{\emptyset\} \times V \to dom inl = V$
58	2 57	ax-mp	$⊢ dom inl = V$
59	56 58	eleqtrri	$⊢ y \in dom inl$
60		simpl	$⊢ (y \in A \land x = inl (y)) \to y \in A$
61	13	funmpt2	$⊢ Fun inl$
62		funfvima	$⊢ (Fun inl \land y \in dom inl) \to (y \in A \to inl (y) \in inl [A])$
63	61 62	mpan	$⊢ y \in dom inl \to (y \in A \to inl (y) \in inl [A])$
64	59 60 63	mpsyl	$⊢ (y \in A \land x = inl (y)) \to inl (y) \in inl [A]$
65		eleq1	$⊢ x = inl (y) \to (x \in inl [A] \leftrightarrow inl (y) \in inl [A])$
66	65	adantl	$⊢ (y \in A \land x = inl (y)) \to (x \in inl [A] \leftrightarrow inl (y) \in inl [A])$
67	64 66	mpbird	$⊢ (y \in A \land x = inl (y)) \to x \in inl [A]$
68	67	rexlimiva	$⊢ \exists y \in A x = inl (y) \to x \in inl [A]$
69		f1odm	$⊢ inr : V \underset{1-1 onto}{⟶} \{1_{𝑜}\} \times V \to dom inr = V$
70	28 69	ax-mp	$⊢ dom inr = V$
71	56 70	eleqtrri	$⊢ y \in dom inr$
72		simpl	$⊢ (y \in B \land x = inr (y)) \to y \in B$
73		f1ofun	$⊢ inr : V \underset{1-1 onto}{⟶} \{1_{𝑜}\} \times V \to Fun inr$
74	28 73	ax-mp	$⊢ Fun inr$
75		funfvima	$⊢ (Fun inr \land y \in dom inr) \to (y \in B \to inr (y) \in inr [B])$
76	74 75	mpan	$⊢ y \in dom inr \to (y \in B \to inr (y) \in inr [B])$
77	71 72 76	mpsyl	$⊢ (y \in B \land x = inr (y)) \to inr (y) \in inr [B]$
78		eleq1	$⊢ x = inr (y) \to (x \in inr [B] \leftrightarrow inr (y) \in inr [B])$
79	78	adantl	$⊢ (y \in B \land x = inr (y)) \to (x \in inr [B] \leftrightarrow inr (y) \in inr [B])$
80	77 79	mpbird	$⊢ (y \in B \land x = inr (y)) \to x \in inr [B]$
81	80	rexlimiva	$⊢ \exists y \in B x = inr (y) \to x \in inr [B]$
82	68 81	orim12i	$⊢ (\exists y \in A x = inl (y) \lor \exists y \in B x = inr (y)) \to (x \in inl [A] \lor x \in inr [B])$
83	55 82	syl	$⊢ x \in (A ⊔︀ B) \to (x \in inl [A] \lor x \in inr [B])$
84	83 1	sylibr	$⊢ x \in (A ⊔︀ B) \to x \in (inl [A] \cup inr [B])$
85	84	ssriv	$⊢ (A ⊔︀ B) \subseteq inl [A] \cup inr [B]$
86	54 85	eqssi	$⊢ inl [A] \cup inr [B] = (A ⊔︀ B)$

Metamath Proof Explorer

Theorem djuun

Proof