Metamath Proof Explorer

Theorem eldju2ndl

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

Ref Expression
Assertion eldju2ndl 
|- ( ( X e. ( A |_| B ) /\ ( 1st ` X ) = (/) ) -> ( 2nd ` X ) e. A )

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 simprr 
 |-  ( ( X = <. ( 1st ` X ) , ( 2nd ` X ) >. /\ ( ( 1st ` X ) e. { (/) } /\ ( 2nd ` X ) e. A ) ) -> ( 2nd ` X ) e. A )
7 6 a1d 
 |-  ( ( X = <. ( 1st ` X ) , ( 2nd ` X ) >. /\ ( ( 1st ` X ) e. { (/) } /\ ( 2nd ` X ) e. A ) ) -> ( ( 1st ` X ) = (/) -> ( 2nd ` X ) e. A ) )
8 5 7 sylbi 
 |-  ( X e. ( { (/) } X. A ) -> ( ( 1st ` X ) = (/) -> ( 2nd ` X ) e. A ) )
9 elxp6 
 |-  ( X e. ( { 1o } X. B ) <-> ( X = <. ( 1st ` X ) , ( 2nd ` X ) >. /\ ( ( 1st ` X ) e. { 1o } /\ ( 2nd ` X ) e. B ) ) )
10 elsni 
 |-  ( ( 1st ` X ) e. { 1o } -> ( 1st ` X ) = 1o )
11 1n0 
 |-  1o =/= (/)
12 neeq1 
 |-  ( ( 1st ` X ) = 1o -> ( ( 1st ` X ) =/= (/) <-> 1o =/= (/) ) )
13 11 12 mpbiri 
 |-  ( ( 1st ` X ) = 1o -> ( 1st ` X ) =/= (/) )
14 eqneqall 
 |-  ( ( 1st ` X ) = (/) -> ( ( 1st ` X ) =/= (/) -> ( 2nd ` X ) e. A ) )
15 14 com12 
 |-  ( ( 1st ` X ) =/= (/) -> ( ( 1st ` X ) = (/) -> ( 2nd ` X ) e. A ) )
16 10 13 15 3syl 
 |-  ( ( 1st ` X ) e. { 1o } -> ( ( 1st ` X ) = (/) -> ( 2nd ` X ) e. A ) )
17 16 ad2antrl 
 |-  ( ( X = <. ( 1st ` X ) , ( 2nd ` X ) >. /\ ( ( 1st ` X ) e. { 1o } /\ ( 2nd ` X ) e. B ) ) -> ( ( 1st ` X ) = (/) -> ( 2nd ` X ) e. A ) )
18 9 17 sylbi 
 |-  ( X e. ( { 1o } X. B ) -> ( ( 1st ` X ) = (/) -> ( 2nd ` X ) e. A ) )
19 8 18 jaoi 
 |-  ( ( X e. ( { (/) } X. A ) \/ X e. ( { 1o } X. B ) ) -> ( ( 1st ` X ) = (/) -> ( 2nd ` X ) e. A ) )
20 4 19 sylbi 
 |-  ( X e. ( A |_| B ) -> ( ( 1st ` X ) = (/) -> ( 2nd ` X ) e. A ) )
21 20 imp 
 |-  ( ( X e. ( A |_| B ) /\ ( 1st ` X ) = (/) ) -> ( 2nd ` X ) e. A )