# Metamath Proof Explorer

## 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 ) )`
` |-  ( ( 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 )`