Theorem 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 \left(A\mathrm{\bigsqcup ︀}B\right)\to \left(1^{st}\left(X\right)=\varnothing \vee 1^{st}\left(X\right)=1_{𝑜}\right)$$

Proof

Step	Hyp	Ref	Expression
1		djuss	$$⊢\left(A\mathrm{\bigsqcup ︀}B\right)\subseteq \left\{\varnothing ,1_{𝑜}\right\}\times \left(A\cup B\right)$$
2		ssel2	$$⊢\left(\left(A\mathrm{\bigsqcup ︀}B\right)\subseteq \left\{\varnothing ,1_{𝑜}\right\}\times \left(A\cup B\right)\wedge X\in \left(A\mathrm{\bigsqcup ︀}B\right)\right)\to X\in \left(\left\{\varnothing ,1_{𝑜}\right\}\times \left(A\cup B\right)\right)$$
3		xp1st	$$⊢X\in \left(\left\{\varnothing ,1_{𝑜}\right\}\times \left(A\cup B\right)\right)\to 1^{st}\left(X\right)\in \left\{\varnothing ,1_{𝑜}\right\}$$
4		elpri	$$⊢1^{st}\left(X\right)\in \left\{\varnothing ,1_{𝑜}\right\}\to \left(1^{st}\left(X\right)=\varnothing \vee 1^{st}\left(X\right)=1_{𝑜}\right)$$
5	2 3 4	3syl	$$⊢\left(\left(A\mathrm{\bigsqcup ︀}B\right)\subseteq \left\{\varnothing ,1_{𝑜}\right\}\times \left(A\cup B\right)\wedge X\in \left(A\mathrm{\bigsqcup ︀}B\right)\right)\to \left(1^{st}\left(X\right)=\varnothing \vee 1^{st}\left(X\right)=1_{𝑜}\right)$$
6	1 5	mpan	$$⊢X\in \left(A\mathrm{\bigsqcup ︀}B\right)\to \left(1^{st}\left(X\right)=\varnothing \vee 1^{st}\left(X\right)=1_{𝑜}\right)$$