This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) ) )