djur

Description: A member of a disjoint union can be mapped from one of the classes which produced it. (Contributed by Jim Kingdon, 23-Jun-2022)

		Ref	Expression
	Assertion	djur	$⊢ C \in (A ⊔︀ B) \to (\exists x \in A C = inl (x) \lor \exists x \in B C = inr (x))$

Proof

Step	Hyp	Ref	Expression
1		df-dju	$⊢ (A ⊔︀ B) = (\{\emptyset\} \times A) \cup (\{1_{𝑜}\} \times B)$
2	1	eleq2i	$⊢ C \in (A ⊔︀ B) \leftrightarrow C \in ((\{\emptyset\} \times A) \cup (\{1_{𝑜}\} \times B))$
3		elun	$⊢ C \in ((\{\emptyset\} \times A) \cup (\{1_{𝑜}\} \times B)) \leftrightarrow (C \in (\{\emptyset\} \times A) \lor C \in (\{1_{𝑜}\} \times B))$
4	2 3	sylbb	$⊢ C \in (A ⊔︀ B) \to (C \in (\{\emptyset\} \times A) \lor C \in (\{1_{𝑜}\} \times B))$
5		xp2nd	$⊢ C \in (\{\emptyset\} \times A) \to 2^{nd} (C) \in A$
6		1st2nd2	$⊢ C \in (\{\emptyset\} \times A) \to C = ⟨1^{st} (C), 2^{nd} (C)⟩$
7		xp1st	$⊢ C \in (\{\emptyset\} \times A) \to 1^{st} (C) \in \{\emptyset\}$
8		elsni	$⊢ 1^{st} (C) \in \{\emptyset\} \to 1^{st} (C) = \emptyset$
9		opeq1	$⊢ 1^{st} (C) = \emptyset \to ⟨1^{st} (C), 2^{nd} (C)⟩ = ⟨\emptyset, 2^{nd} (C)⟩$
10	9	eqeq2d	$⊢ 1^{st} (C) = \emptyset \to (C = ⟨1^{st} (C), 2^{nd} (C)⟩ \leftrightarrow C = ⟨\emptyset, 2^{nd} (C)⟩)$
11	7 8 10	3syl	$⊢ C \in (\{\emptyset\} \times A) \to (C = ⟨1^{st} (C), 2^{nd} (C)⟩ \leftrightarrow C = ⟨\emptyset, 2^{nd} (C)⟩)$
12	6 11	mpbid	$⊢ C \in (\{\emptyset\} \times A) \to C = ⟨\emptyset, 2^{nd} (C)⟩$
13		fvexd	$⊢ C \in (\{\emptyset\} \times A) \to 2^{nd} (C) \in V$
14		opex	$⊢ ⟨\emptyset, 2^{nd} (C)⟩ \in V$
15		opeq2	$⊢ y = 2^{nd} (C) \to ⟨\emptyset, y⟩ = ⟨\emptyset, 2^{nd} (C)⟩$
16		df-inl	$⊢ inl = (y \in V ⟼ ⟨\emptyset, y⟩)$
17	15 16	fvmptg	$⊢ (2^{nd} (C) \in V \land ⟨\emptyset, 2^{nd} (C)⟩ \in V) \to inl (2^{nd} (C)) = ⟨\emptyset, 2^{nd} (C)⟩$
18	13 14 17	sylancl	$⊢ C \in (\{\emptyset\} \times A) \to inl (2^{nd} (C)) = ⟨\emptyset, 2^{nd} (C)⟩$
19	12 18	eqtr4d	$⊢ C \in (\{\emptyset\} \times A) \to C = inl (2^{nd} (C))$
20		fveq2	$⊢ x = 2^{nd} (C) \to inl (x) = inl (2^{nd} (C))$
21	20	rspceeqv	$⊢ (2^{nd} (C) \in A \land C = inl (2^{nd} (C))) \to \exists x \in A C = inl (x)$
22	5 19 21	syl2anc	$⊢ C \in (\{\emptyset\} \times A) \to \exists x \in A C = inl (x)$
23		xp2nd	$⊢ C \in (\{1_{𝑜}\} \times B) \to 2^{nd} (C) \in B$
24		1st2nd2	$⊢ C \in (\{1_{𝑜}\} \times B) \to C = ⟨1^{st} (C), 2^{nd} (C)⟩$
25		xp1st	$⊢ C \in (\{1_{𝑜}\} \times B) \to 1^{st} (C) \in \{1_{𝑜}\}$
26		elsni	$⊢ 1^{st} (C) \in \{1_{𝑜}\} \to 1^{st} (C) = 1_{𝑜}$
27		opeq1	$⊢ 1^{st} (C) = 1_{𝑜} \to ⟨1^{st} (C), 2^{nd} (C)⟩ = ⟨1_{𝑜}, 2^{nd} (C)⟩$
28	27	eqeq2d	$⊢ 1^{st} (C) = 1_{𝑜} \to (C = ⟨1^{st} (C), 2^{nd} (C)⟩ \leftrightarrow C = ⟨1_{𝑜}, 2^{nd} (C)⟩)$
29	25 26 28	3syl	$⊢ C \in (\{1_{𝑜}\} \times B) \to (C = ⟨1^{st} (C), 2^{nd} (C)⟩ \leftrightarrow C = ⟨1_{𝑜}, 2^{nd} (C)⟩)$
30	24 29	mpbid	$⊢ C \in (\{1_{𝑜}\} \times B) \to C = ⟨1_{𝑜}, 2^{nd} (C)⟩$
31		fvexd	$⊢ C \in (\{1_{𝑜}\} \times B) \to 2^{nd} (C) \in V$
32		opex	$⊢ ⟨1_{𝑜}, 2^{nd} (C)⟩ \in V$
33		opeq2	$⊢ z = 2^{nd} (C) \to ⟨1_{𝑜}, z⟩ = ⟨1_{𝑜}, 2^{nd} (C)⟩$
34		df-inr	$⊢ inr = (z \in V ⟼ ⟨1_{𝑜}, z⟩)$
35	33 34	fvmptg	$⊢ (2^{nd} (C) \in V \land ⟨1_{𝑜}, 2^{nd} (C)⟩ \in V) \to inr (2^{nd} (C)) = ⟨1_{𝑜}, 2^{nd} (C)⟩$
36	31 32 35	sylancl	$⊢ C \in (\{1_{𝑜}\} \times B) \to inr (2^{nd} (C)) = ⟨1_{𝑜}, 2^{nd} (C)⟩$
37	30 36	eqtr4d	$⊢ C \in (\{1_{𝑜}\} \times B) \to C = inr (2^{nd} (C))$
38		fveq2	$⊢ x = 2^{nd} (C) \to inr (x) = inr (2^{nd} (C))$
39	38	rspceeqv	$⊢ (2^{nd} (C) \in B \land C = inr (2^{nd} (C))) \to \exists x \in B C = inr (x)$
40	23 37 39	syl2anc	$⊢ C \in (\{1_{𝑜}\} \times B) \to \exists x \in B C = inr (x)$
41	22 40	orim12i	$⊢ (C \in (\{\emptyset\} \times A) \lor C \in (\{1_{𝑜}\} \times B)) \to (\exists x \in A C = inl (x) \lor \exists x \in B C = inr (x))$
42	4 41	syl	$⊢ C \in (A ⊔︀ B) \to (\exists x \in A C = inl (x) \lor \exists x \in B C = inr (x))$

Metamath Proof Explorer

Theorem djur

Proof