# Metamath Proof Explorer

## Theorem djur

Description: A member of a disjoint union can be mapped from one of the classes which produced it. (Contributed by Jim Kingdon, 23-Jun-2022)

Ref Expression
Assertion djur
`|- ( C e. ( A |_| B ) -> ( E. x e. A C = ( inl ` x ) \/ E. x e. B C = ( inr ` x ) ) )`

### Proof

Step Hyp Ref Expression
1 df-dju
` |-  ( A |_| B ) = ( ( { (/) } X. A ) u. ( { 1o } X. B ) )`
2 1 eleq2i
` |-  ( C e. ( A |_| B ) <-> C e. ( ( { (/) } X. A ) u. ( { 1o } X. B ) ) )`
3 elun
` |-  ( C e. ( ( { (/) } X. A ) u. ( { 1o } X. B ) ) <-> ( C e. ( { (/) } X. A ) \/ C e. ( { 1o } X. B ) ) )`
4 2 3 sylbb
` |-  ( C e. ( A |_| B ) -> ( C e. ( { (/) } X. A ) \/ C e. ( { 1o } X. B ) ) )`
5 xp2nd
` |-  ( C e. ( { (/) } X. A ) -> ( 2nd ` C ) e. A )`
6 1st2nd2
` |-  ( C e. ( { (/) } X. A ) -> C = <. ( 1st ` C ) , ( 2nd ` C ) >. )`
7 xp1st
` |-  ( C e. ( { (/) } X. A ) -> ( 1st ` C ) e. { (/) } )`
8 elsni
` |-  ( ( 1st ` C ) e. { (/) } -> ( 1st ` C ) = (/) )`
9 opeq1
` |-  ( ( 1st ` C ) = (/) -> <. ( 1st ` C ) , ( 2nd ` C ) >. = <. (/) , ( 2nd ` C ) >. )`
10 9 eqeq2d
` |-  ( ( 1st ` C ) = (/) -> ( C = <. ( 1st ` C ) , ( 2nd ` C ) >. <-> C = <. (/) , ( 2nd ` C ) >. ) )`
11 7 8 10 3syl
` |-  ( C e. ( { (/) } X. A ) -> ( C = <. ( 1st ` C ) , ( 2nd ` C ) >. <-> C = <. (/) , ( 2nd ` C ) >. ) )`
12 6 11 mpbid
` |-  ( C e. ( { (/) } X. A ) -> C = <. (/) , ( 2nd ` C ) >. )`
13 fvexd
` |-  ( C e. ( { (/) } X. A ) -> ( 2nd ` C ) e. _V )`
14 opex
` |-  <. (/) , ( 2nd ` C ) >. e. _V`
15 opeq2
` |-  ( y = ( 2nd ` C ) -> <. (/) , y >. = <. (/) , ( 2nd ` C ) >. )`
16 df-inl
` |-  inl = ( y e. _V |-> <. (/) , y >. )`
17 15 16 fvmptg
` |-  ( ( ( 2nd ` C ) e. _V /\ <. (/) , ( 2nd ` C ) >. e. _V ) -> ( inl ` ( 2nd ` C ) ) = <. (/) , ( 2nd ` C ) >. )`
18 13 14 17 sylancl
` |-  ( C e. ( { (/) } X. A ) -> ( inl ` ( 2nd ` C ) ) = <. (/) , ( 2nd ` C ) >. )`
19 12 18 eqtr4d
` |-  ( C e. ( { (/) } X. A ) -> C = ( inl ` ( 2nd ` C ) ) )`
20 fveq2
` |-  ( x = ( 2nd ` C ) -> ( inl ` x ) = ( inl ` ( 2nd ` C ) ) )`
21 20 rspceeqv
` |-  ( ( ( 2nd ` C ) e. A /\ C = ( inl ` ( 2nd ` C ) ) ) -> E. x e. A C = ( inl ` x ) )`
22 5 19 21 syl2anc
` |-  ( C e. ( { (/) } X. A ) -> E. x e. A C = ( inl ` x ) )`
23 xp2nd
` |-  ( C e. ( { 1o } X. B ) -> ( 2nd ` C ) e. B )`
24 1st2nd2
` |-  ( C e. ( { 1o } X. B ) -> C = <. ( 1st ` C ) , ( 2nd ` C ) >. )`
25 xp1st
` |-  ( C e. ( { 1o } X. B ) -> ( 1st ` C ) e. { 1o } )`
26 elsni
` |-  ( ( 1st ` C ) e. { 1o } -> ( 1st ` C ) = 1o )`
27 opeq1
` |-  ( ( 1st ` C ) = 1o -> <. ( 1st ` C ) , ( 2nd ` C ) >. = <. 1o , ( 2nd ` C ) >. )`
28 27 eqeq2d
` |-  ( ( 1st ` C ) = 1o -> ( C = <. ( 1st ` C ) , ( 2nd ` C ) >. <-> C = <. 1o , ( 2nd ` C ) >. ) )`
29 25 26 28 3syl
` |-  ( C e. ( { 1o } X. B ) -> ( C = <. ( 1st ` C ) , ( 2nd ` C ) >. <-> C = <. 1o , ( 2nd ` C ) >. ) )`
30 24 29 mpbid
` |-  ( C e. ( { 1o } X. B ) -> C = <. 1o , ( 2nd ` C ) >. )`
31 fvexd
` |-  ( C e. ( { 1o } X. B ) -> ( 2nd ` C ) e. _V )`
32 opex
` |-  <. 1o , ( 2nd ` C ) >. e. _V`
33 opeq2
` |-  ( z = ( 2nd ` C ) -> <. 1o , z >. = <. 1o , ( 2nd ` C ) >. )`
34 df-inr
` |-  inr = ( z e. _V |-> <. 1o , z >. )`
35 33 34 fvmptg
` |-  ( ( ( 2nd ` C ) e. _V /\ <. 1o , ( 2nd ` C ) >. e. _V ) -> ( inr ` ( 2nd ` C ) ) = <. 1o , ( 2nd ` C ) >. )`
36 31 32 35 sylancl
` |-  ( C e. ( { 1o } X. B ) -> ( inr ` ( 2nd ` C ) ) = <. 1o , ( 2nd ` C ) >. )`
37 30 36 eqtr4d
` |-  ( C e. ( { 1o } X. B ) -> C = ( inr ` ( 2nd ` C ) ) )`
38 fveq2
` |-  ( x = ( 2nd ` C ) -> ( inr ` x ) = ( inr ` ( 2nd ` C ) ) )`
39 38 rspceeqv
` |-  ( ( ( 2nd ` C ) e. B /\ C = ( inr ` ( 2nd ` C ) ) ) -> E. x e. B C = ( inr ` x ) )`
40 23 37 39 syl2anc
` |-  ( C e. ( { 1o } X. B ) -> E. x e. B C = ( inr ` x ) )`
41 22 40 orim12i
` |-  ( ( C e. ( { (/) } X. A ) \/ C e. ( { 1o } X. B ) ) -> ( E. x e. A C = ( inl ` x ) \/ E. x e. B C = ( inr ` x ) ) )`
42 4 41 syl
` |-  ( C e. ( A |_| B ) -> ( E. x e. A C = ( inl ` x ) \/ E. x e. B C = ( inr ` x ) ) )`