eldju2ndl

Description: The second component of an element of a disjoint union is an element of the left class of the disjoint union if its first component is the empty set. (Contributed by AV, 26-Jun-2022)

		Ref	Expression
	Assertion	eldju2ndl	$⊢ (X \in (A ⊔︀ B) \land 1^{st} (X) = \emptyset) \to 2^{nd} (X) \in A$

Proof

Step	Hyp	Ref	Expression
1		df-dju	$⊢ (A ⊔︀ B) = (\{\emptyset\} \times A) \cup (\{1_{𝑜}\} \times B)$
2	1	eleq2i	$⊢ X \in (A ⊔︀ B) \leftrightarrow X \in ((\{\emptyset\} \times A) \cup (\{1_{𝑜}\} \times B))$
3		elun	$⊢ X \in ((\{\emptyset\} \times A) \cup (\{1_{𝑜}\} \times B)) \leftrightarrow (X \in (\{\emptyset\} \times A) \lor X \in (\{1_{𝑜}\} \times B))$
4	2 3	bitri	$⊢ X \in (A ⊔︀ B) \leftrightarrow (X \in (\{\emptyset\} \times A) \lor X \in (\{1_{𝑜}\} \times B))$
5		elxp6	$⊢ X \in (\{\emptyset\} \times A) \leftrightarrow (X = ⟨1^{st} (X), 2^{nd} (X)⟩ \land (1^{st} (X) \in \{\emptyset\} \land 2^{nd} (X) \in A))$
6		simprr	$⊢ (X = ⟨1^{st} (X), 2^{nd} (X)⟩ \land (1^{st} (X) \in \{\emptyset\} \land 2^{nd} (X) \in A)) \to 2^{nd} (X) \in A$
7	6	a1d	$⊢ (X = ⟨1^{st} (X), 2^{nd} (X)⟩ \land (1^{st} (X) \in \{\emptyset\} \land 2^{nd} (X) \in A)) \to (1^{st} (X) = \emptyset \to 2^{nd} (X) \in A)$
8	5 7	sylbi	$⊢ X \in (\{\emptyset\} \times A) \to (1^{st} (X) = \emptyset \to 2^{nd} (X) \in A)$
9		elxp6	$⊢ X \in (\{1_{𝑜}\} \times B) \leftrightarrow (X = ⟨1^{st} (X), 2^{nd} (X)⟩ \land (1^{st} (X) \in \{1_{𝑜}\} \land 2^{nd} (X) \in B))$
10		elsni	$⊢ 1^{st} (X) \in \{1_{𝑜}\} \to 1^{st} (X) = 1_{𝑜}$
11		1n0	$⊢ 1_{𝑜} \neq \emptyset$
12		neeq1	$⊢ 1^{st} (X) = 1_{𝑜} \to (1^{st} (X) \neq \emptyset \leftrightarrow 1_{𝑜} \neq \emptyset)$
13	11 12	mpbiri	$⊢ 1^{st} (X) = 1_{𝑜} \to 1^{st} (X) \neq \emptyset$
14		eqneqall	$⊢ 1^{st} (X) = \emptyset \to (1^{st} (X) \neq \emptyset \to 2^{nd} (X) \in A)$
15	14	com12	$⊢ 1^{st} (X) \neq \emptyset \to (1^{st} (X) = \emptyset \to 2^{nd} (X) \in A)$
16	10 13 15	3syl	$⊢ 1^{st} (X) \in \{1_{𝑜}\} \to (1^{st} (X) = \emptyset \to 2^{nd} (X) \in A)$
17	16	ad2antrl	$⊢ (X = ⟨1^{st} (X), 2^{nd} (X)⟩ \land (1^{st} (X) \in \{1_{𝑜}\} \land 2^{nd} (X) \in B)) \to (1^{st} (X) = \emptyset \to 2^{nd} (X) \in A)$
18	9 17	sylbi	$⊢ X \in (\{1_{𝑜}\} \times B) \to (1^{st} (X) = \emptyset \to 2^{nd} (X) \in A)$
19	8 18	jaoi	$⊢ (X \in (\{\emptyset\} \times A) \lor X \in (\{1_{𝑜}\} \times B)) \to (1^{st} (X) = \emptyset \to 2^{nd} (X) \in A)$
20	4 19	sylbi	$⊢ X \in (A ⊔︀ B) \to (1^{st} (X) = \emptyset \to 2^{nd} (X) \in A)$
21	20	imp	$⊢ (X \in (A ⊔︀ B) \land 1^{st} (X) = \emptyset) \to 2^{nd} (X) \in A$

Metamath Proof Explorer

Theorem eldju2ndl

Proof