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	|- ( ( X e. ( A |_| B ) /\ ( 1st ` X ) =/= (/) ) -> ( 2nd ` X ) e. B )

Proof

Step	Hyp	Ref	Expression
1		df-dju	|- ( A |_| B ) = ( ( { (/) } X. A ) u. ( { 1o } X. B ) )
2	1	eleq2i	|- ( X e. ( A |_| B ) <-> X e. ( ( { (/) } X. A ) u. ( { 1o } X. B ) ) )
3		elun	|- ( X e. ( ( { (/) } X. A ) u. ( { 1o } X. B ) ) <-> ( X e. ( { (/) } X. A ) \/ X e. ( { 1o } X. B ) ) )
4	2 3	bitri	|- ( X e. ( A |_| B ) <-> ( X e. ( { (/) } X. A ) \/ X e. ( { 1o } X. B ) ) )
5		elxp6	|- ( X e. ( { (/) } X. A ) <-> ( X = <. ( 1st ` X ) , ( 2nd ` X ) >. /\ ( ( 1st ` X ) e. { (/) } /\ ( 2nd ` X ) e. A ) ) )
6		elsni	|- ( ( 1st ` X ) e. { (/) } -> ( 1st ` X ) = (/) )
7		eqneqall	|- ( ( 1st ` X ) = (/) -> ( ( 1st ` X ) =/= (/) -> ( 2nd ` X ) e. B ) )
8	6 7	syl	|- ( ( 1st ` X ) e. { (/) } -> ( ( 1st ` X ) =/= (/) -> ( 2nd ` X ) e. B ) )
9	8	ad2antrl	|- ( ( X = <. ( 1st ` X ) , ( 2nd ` X ) >. /\ ( ( 1st ` X ) e. { (/) } /\ ( 2nd ` X ) e. A ) ) -> ( ( 1st ` X ) =/= (/) -> ( 2nd ` X ) e. B ) )
10	5 9	sylbi	|- ( X e. ( { (/) } X. A ) -> ( ( 1st ` X ) =/= (/) -> ( 2nd ` X ) e. B ) )
11		elxp6	|- ( X e. ( { 1o } X. B ) <-> ( X = <. ( 1st ` X ) , ( 2nd ` X ) >. /\ ( ( 1st ` X ) e. { 1o } /\ ( 2nd ` X ) e. B ) ) )
12		simprr	|- ( ( X = <. ( 1st ` X ) , ( 2nd ` X ) >. /\ ( ( 1st ` X ) e. { 1o } /\ ( 2nd ` X ) e. B ) ) -> ( 2nd ` X ) e. B )
13	12	a1d	|- ( ( X = <. ( 1st ` X ) , ( 2nd ` X ) >. /\ ( ( 1st ` X ) e. { 1o } /\ ( 2nd ` X ) e. B ) ) -> ( ( 1st ` X ) =/= (/) -> ( 2nd ` X ) e. B ) )
14	11 13	sylbi	|- ( X e. ( { 1o } X. B ) -> ( ( 1st ` X ) =/= (/) -> ( 2nd ` X ) e. B ) )
15	10 14	jaoi	|- ( ( X e. ( { (/) } X. A ) \/ X e. ( { 1o } X. B ) ) -> ( ( 1st ` X ) =/= (/) -> ( 2nd ` X ) e. B ) )
16	4 15	sylbi	|- ( X e. ( A |_| B ) -> ( ( 1st ` X ) =/= (/) -> ( 2nd ` X ) e. B ) )
17	16	imp	|- ( ( X e. ( A |_| B ) /\ ( 1st ` X ) =/= (/) ) -> ( 2nd ` X ) e. B )