eldju1st

Description: The first component of an element of a disjoint union is either (/) or 1o . (Contributed by AV, 26-Jun-2022)

		Ref	Expression
	Assertion	eldju1st	$⊢ X \in (A ⊔︀ B) \to (1^{st} (X) = \emptyset \lor 1^{st} (X) = 1_{𝑜})$

Step	Hyp	Ref	Expression
1		djuss	$⊢ (A ⊔︀ B) \subseteq \{\emptyset, 1_{𝑜}\} \times (A \cup B)$
2		ssel2	$⊢ ((A ⊔︀ B) \subseteq \{\emptyset, 1_{𝑜}\} \times (A \cup B) \land X \in (A ⊔︀ B)) \to X \in (\{\emptyset, 1_{𝑜}\} \times (A \cup B))$
3		xp1st	$⊢ X \in (\{\emptyset, 1_{𝑜}\} \times (A \cup B)) \to 1^{st} (X) \in \{\emptyset, 1_{𝑜}\}$
4		elpri	$⊢ 1^{st} (X) \in \{\emptyset, 1_{𝑜}\} \to (1^{st} (X) = \emptyset \lor 1^{st} (X) = 1_{𝑜})$
5	2 3 4	3syl	$⊢ ((A ⊔︀ B) \subseteq \{\emptyset, 1_{𝑜}\} \times (A \cup B) \land X \in (A ⊔︀ B)) \to (1^{st} (X) = \emptyset \lor 1^{st} (X) = 1_{𝑜})$
6	1 5	mpan	$⊢ X \in (A ⊔︀ B) \to (1^{st} (X) = \emptyset \lor 1^{st} (X) = 1_{𝑜})$

Metamath Proof Explorer