Theorem eldju2ndr

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

	Ref	Expression
Assertion	eldju2ndr	$$⊢\left(X\in \left(A\mathrm{\bigsqcup ︀}B\right)\wedge 1^{st}\left(X\right)\ne \varnothing \right)\to 2^{nd}\left(X\right)\in B$$

Proof

Step	Hyp	Ref	Expression
1		df-dju	$$⊢\left(A\mathrm{\bigsqcup ︀}B\right)=\left(\left\{\varnothing \right\}\times A\right)\cup \left(\left\{1_{𝑜}\right\}\times B\right)$$
2	1	eleq2i	$$⊢X\in \left(A\mathrm{\bigsqcup ︀}B\right)\leftrightarrow X\in \left(\left(\left\{\varnothing \right\}\times A\right)\cup \left(\left\{1_{𝑜}\right\}\times B\right)\right)$$
3		elun	$$⊢X\in \left(\left(\left\{\varnothing \right\}\times A\right)\cup \left(\left\{1_{𝑜}\right\}\times B\right)\right)\leftrightarrow \left(X\in \left(\left\{\varnothing \right\}\times A\right)\vee X\in \left(\left\{1_{𝑜}\right\}\times B\right)\right)$$
4	2 3	bitri	$$⊢X\in \left(A\mathrm{\bigsqcup ︀}B\right)\leftrightarrow \left(X\in \left(\left\{\varnothing \right\}\times A\right)\vee X\in \left(\left\{1_{𝑜}\right\}\times B\right)\right)$$
5		elxp6	$$⊢X\in \left(\left\{\varnothing \right\}\times A\right)\leftrightarrow \left(X=⟨1^{st}\left(X\right),2^{nd}\left(X\right)⟩\wedge \left(1^{st}\left(X\right)\in \left\{\varnothing \right\}\wedge 2^{nd}\left(X\right)\in A\right)\right)$$
6		elsni	$$⊢1^{st}\left(X\right)\in \left\{\varnothing \right\}\to 1^{st}\left(X\right)=\varnothing$$
7		eqneqall	$$⊢1^{st}\left(X\right)=\varnothing \to \left(1^{st}\left(X\right)\ne \varnothing \to 2^{nd}\left(X\right)\in B\right)$$
8	6 7	syl	$$⊢1^{st}\left(X\right)\in \left\{\varnothing \right\}\to \left(1^{st}\left(X\right)\ne \varnothing \to 2^{nd}\left(X\right)\in B\right)$$
9	8	ad2antrl	$$⊢\left(X=⟨1^{st}\left(X\right),2^{nd}\left(X\right)⟩\wedge \left(1^{st}\left(X\right)\in \left\{\varnothing \right\}\wedge 2^{nd}\left(X\right)\in A\right)\right)\to \left(1^{st}\left(X\right)\ne \varnothing \to 2^{nd}\left(X\right)\in B\right)$$
10	5 9	sylbi	$$⊢X\in \left(\left\{\varnothing \right\}\times A\right)\to \left(1^{st}\left(X\right)\ne \varnothing \to 2^{nd}\left(X\right)\in B\right)$$
11		elxp6	$$⊢X\in \left(\left\{1_{𝑜}\right\}\times B\right)\leftrightarrow \left(X=⟨1^{st}\left(X\right),2^{nd}\left(X\right)⟩\wedge \left(1^{st}\left(X\right)\in \left\{1_{𝑜}\right\}\wedge 2^{nd}\left(X\right)\in B\right)\right)$$
12		simprr	$$⊢\left(X=⟨1^{st}\left(X\right),2^{nd}\left(X\right)⟩\wedge \left(1^{st}\left(X\right)\in \left\{1_{𝑜}\right\}\wedge 2^{nd}\left(X\right)\in B\right)\right)\to 2^{nd}\left(X\right)\in B$$
13	12	a1d	$$⊢\left(X=⟨1^{st}\left(X\right),2^{nd}\left(X\right)⟩\wedge \left(1^{st}\left(X\right)\in \left\{1_{𝑜}\right\}\wedge 2^{nd}\left(X\right)\in B\right)\right)\to \left(1^{st}\left(X\right)\ne \varnothing \to 2^{nd}\left(X\right)\in B\right)$$
14	11 13	sylbi	$$⊢X\in \left(\left\{1_{𝑜}\right\}\times B\right)\to \left(1^{st}\left(X\right)\ne \varnothing \to 2^{nd}\left(X\right)\in B\right)$$
15	10 14	jaoi	$$⊢\left(X\in \left(\left\{\varnothing \right\}\times A\right)\vee X\in \left(\left\{1_{𝑜}\right\}\times B\right)\right)\to \left(1^{st}\left(X\right)\ne \varnothing \to 2^{nd}\left(X\right)\in B\right)$$
16	4 15	sylbi	$$⊢X\in \left(A\mathrm{\bigsqcup ︀}B\right)\to \left(1^{st}\left(X\right)\ne \varnothing \to 2^{nd}\left(X\right)\in B\right)$$
17	16	imp	$$⊢\left(X\in \left(A\mathrm{\bigsqcup ︀}B\right)\wedge 1^{st}\left(X\right)\ne \varnothing \right)\to 2^{nd}\left(X\right)\in B$$