Metamath Proof Explorer

Theorem djuun

Description: The disjoint union of two classes is the union of the images of those two classes under right and left injection. (Contributed by Jim Kingdon, 22-Jun-2022)

Ref Expression
Assertion djuun 
|- ( ( inl " A ) u. ( inr " B ) ) = ( A |_| B )

Proof

Step Hyp Ref Expression
1 elun 
 |-  ( x e. ( ( inl " A ) u. ( inr " B ) ) <-> ( x e. ( inl " A ) \/ x e. ( inr " B ) ) )
2 djulf1o 
 |-  inl : _V -1-1-onto-> ( { (/) } X. _V )
3 f1ofn 
 |-  ( inl : _V -1-1-onto-> ( { (/) } X. _V ) -> inl Fn _V )
4 2 3 ax-mp 
 |-  inl Fn _V
5 ssv 
 |-  A C_ _V
6 fvelimab 
 |-  ( ( inl Fn _V /\ A C_ _V ) -> ( x e. ( inl " A ) <-> E. u e. A ( inl ` u ) = x ) )
7 4 5 6 mp2an 
 |-  ( x e. ( inl " A ) <-> E. u e. A ( inl ` u ) = x )
8 7 biimpi 
 |-  ( x e. ( inl " A ) -> E. u e. A ( inl ` u ) = x )
9 simprr 
 |-  ( ( x e. ( inl " A ) /\ ( u e. A /\ ( inl ` u ) = x ) ) -> ( inl ` u ) = x )
10 vex 
 |-  u e. _V
11 opex 
 |-  <. (/) , u >. e. _V
12 opeq2 
 |-  ( z = u -> <. (/) , z >. = <. (/) , u >. )
13 df-inl 
 |-  inl = ( z e. _V |-> <. (/) , z >. )
14 12 13 fvmptg 
 |-  ( ( u e. _V /\ <. (/) , u >. e. _V ) -> ( inl ` u ) = <. (/) , u >. )
15 10 11 14 mp2an 
 |-  ( inl ` u ) = <. (/) , u >.
16 0ex 
 |-  (/) e. _V
17 16 snid 
 |-  (/) e. { (/) }
18 opelxpi 
 |-  ( ( (/) e. { (/) } /\ u e. A ) -> <. (/) , u >. e. ( { (/) } X. A ) )
19 17 18 mpan 
 |-  ( u e. A -> <. (/) , u >. e. ( { (/) } X. A ) )
20 19 ad2antrl 
 |-  ( ( x e. ( inl " A ) /\ ( u e. A /\ ( inl ` u ) = x ) ) -> <. (/) , u >. e. ( { (/) } X. A ) )
21 15 20 eqeltrid 
 |-  ( ( x e. ( inl " A ) /\ ( u e. A /\ ( inl ` u ) = x ) ) -> ( inl ` u ) e. ( { (/) } X. A ) )
22 9 21 eqeltrrd 
 |-  ( ( x e. ( inl " A ) /\ ( u e. A /\ ( inl ` u ) = x ) ) -> x e. ( { (/) } X. A ) )
23 8 22 rexlimddv 
 |-  ( x e. ( inl " A ) -> x e. ( { (/) } X. A ) )
24 elun1 
 |-  ( x e. ( { (/) } X. A ) -> x e. ( ( { (/) } X. A ) u. ( { 1o } X. B ) ) )
25 23 24 syl 
 |-  ( x e. ( inl " A ) -> x e. ( ( { (/) } X. A ) u. ( { 1o } X. B ) ) )
26 df-dju 
 |-  ( A |_| B ) = ( ( { (/) } X. A ) u. ( { 1o } X. B ) )
27 25 26 eleqtrrdi 
 |-  ( x e. ( inl " A ) -> x e. ( A |_| B ) )
28 djurf1o 
 |-  inr : _V -1-1-onto-> ( { 1o } X. _V )
29 f1ofn 
 |-  ( inr : _V -1-1-onto-> ( { 1o } X. _V ) -> inr Fn _V )
30 28 29 ax-mp 
 |-  inr Fn _V
31 ssv 
 |-  B C_ _V
32 fvelimab 
 |-  ( ( inr Fn _V /\ B C_ _V ) -> ( x e. ( inr " B ) <-> E. u e. B ( inr ` u ) = x ) )
33 30 31 32 mp2an 
 |-  ( x e. ( inr " B ) <-> E. u e. B ( inr ` u ) = x )
34 33 biimpi 
 |-  ( x e. ( inr " B ) -> E. u e. B ( inr ` u ) = x )
35 simprr 
 |-  ( ( x e. ( inr " B ) /\ ( u e. B /\ ( inr ` u ) = x ) ) -> ( inr ` u ) = x )
36 opex 
 |-  <. 1o , u >. e. _V
37 opeq2 
 |-  ( z = u -> <. 1o , z >. = <. 1o , u >. )
38 df-inr 
 |-  inr = ( z e. _V |-> <. 1o , z >. )
39 37 38 fvmptg 
 |-  ( ( u e. _V /\ <. 1o , u >. e. _V ) -> ( inr ` u ) = <. 1o , u >. )
40 10 36 39 mp2an 
 |-  ( inr ` u ) = <. 1o , u >.
41 1oex 
 |-  1o e. _V
42 41 snid 
 |-  1o e. { 1o }
43 opelxpi 
 |-  ( ( 1o e. { 1o } /\ u e. B ) -> <. 1o , u >. e. ( { 1o } X. B ) )
44 42 43 mpan 
 |-  ( u e. B -> <. 1o , u >. e. ( { 1o } X. B ) )
45 44 ad2antrl 
 |-  ( ( x e. ( inr " B ) /\ ( u e. B /\ ( inr ` u ) = x ) ) -> <. 1o , u >. e. ( { 1o } X. B ) )
46 40 45 eqeltrid 
 |-  ( ( x e. ( inr " B ) /\ ( u e. B /\ ( inr ` u ) = x ) ) -> ( inr ` u ) e. ( { 1o } X. B ) )
47 35 46 eqeltrrd 
 |-  ( ( x e. ( inr " B ) /\ ( u e. B /\ ( inr ` u ) = x ) ) -> x e. ( { 1o } X. B ) )
48 34 47 rexlimddv 
 |-  ( x e. ( inr " B ) -> x e. ( { 1o } X. B ) )
49 elun2 
 |-  ( x e. ( { 1o } X. B ) -> x e. ( ( { (/) } X. A ) u. ( { 1o } X. B ) ) )
50 48 49 syl 
 |-  ( x e. ( inr " B ) -> x e. ( ( { (/) } X. A ) u. ( { 1o } X. B ) ) )
51 50 26 eleqtrrdi 
 |-  ( x e. ( inr " B ) -> x e. ( A |_| B ) )
52 27 51 jaoi 
 |-  ( ( x e. ( inl " A ) \/ x e. ( inr " B ) ) -> x e. ( A |_| B ) )
53 1 52 sylbi 
 |-  ( x e. ( ( inl " A ) u. ( inr " B ) ) -> x e. ( A |_| B ) )
54 53 ssriv 
 |-  ( ( inl " A ) u. ( inr " B ) ) C_ ( A |_| B )
55 djur 
 |-  ( x e. ( A |_| B ) -> ( E. y e. A x = ( inl ` y ) \/ E. y e. B x = ( inr ` y ) ) )
56 vex 
 |-  y e. _V
57 f1odm 
 |-  ( inl : _V -1-1-onto-> ( { (/) } X. _V ) -> dom inl = _V )
58 2 57 ax-mp 
 |-  dom inl = _V
59 56 58 eleqtrri 
 |-  y e. dom inl
60 simpl 
 |-  ( ( y e. A /\ x = ( inl ` y ) ) -> y e. A )
61 13 funmpt2 
 |-  Fun inl
62 funfvima 
 |-  ( ( Fun inl /\ y e. dom inl ) -> ( y e. A -> ( inl ` y ) e. ( inl " A ) ) )
63 61 62 mpan 
 |-  ( y e. dom inl -> ( y e. A -> ( inl ` y ) e. ( inl " A ) ) )
64 59 60 63 mpsyl 
 |-  ( ( y e. A /\ x = ( inl ` y ) ) -> ( inl ` y ) e. ( inl " A ) )
65 eleq1 
 |-  ( x = ( inl ` y ) -> ( x e. ( inl " A ) <-> ( inl ` y ) e. ( inl " A ) ) )
66 65 adantl 
 |-  ( ( y e. A /\ x = ( inl ` y ) ) -> ( x e. ( inl " A ) <-> ( inl ` y ) e. ( inl " A ) ) )
67 64 66 mpbird 
 |-  ( ( y e. A /\ x = ( inl ` y ) ) -> x e. ( inl " A ) )
68 67 rexlimiva 
 |-  ( E. y e. A x = ( inl ` y ) -> x e. ( inl " A ) )
69 f1odm 
 |-  ( inr : _V -1-1-onto-> ( { 1o } X. _V ) -> dom inr = _V )
70 28 69 ax-mp 
 |-  dom inr = _V
71 56 70 eleqtrri 
 |-  y e. dom inr
72 simpl 
 |-  ( ( y e. B /\ x = ( inr ` y ) ) -> y e. B )
73 f1ofun 
 |-  ( inr : _V -1-1-onto-> ( { 1o } X. _V ) -> Fun inr )
74 28 73 ax-mp 
 |-  Fun inr
75 funfvima 
 |-  ( ( Fun inr /\ y e. dom inr ) -> ( y e. B -> ( inr ` y ) e. ( inr " B ) ) )
76 74 75 mpan 
 |-  ( y e. dom inr -> ( y e. B -> ( inr ` y ) e. ( inr " B ) ) )
77 71 72 76 mpsyl 
 |-  ( ( y e. B /\ x = ( inr ` y ) ) -> ( inr ` y ) e. ( inr " B ) )
78 eleq1 
 |-  ( x = ( inr ` y ) -> ( x e. ( inr " B ) <-> ( inr ` y ) e. ( inr " B ) ) )
79 78 adantl 
 |-  ( ( y e. B /\ x = ( inr ` y ) ) -> ( x e. ( inr " B ) <-> ( inr ` y ) e. ( inr " B ) ) )
80 77 79 mpbird 
 |-  ( ( y e. B /\ x = ( inr ` y ) ) -> x e. ( inr " B ) )
81 80 rexlimiva 
 |-  ( E. y e. B x = ( inr ` y ) -> x e. ( inr " B ) )
82 68 81 orim12i 
 |-  ( ( E. y e. A x = ( inl ` y ) \/ E. y e. B x = ( inr ` y ) ) -> ( x e. ( inl " A ) \/ x e. ( inr " B ) ) )
83 55 82 syl 
 |-  ( x e. ( A |_| B ) -> ( x e. ( inl " A ) \/ x e. ( inr " B ) ) )
84 83 1 sylibr 
 |-  ( x e. ( A |_| B ) -> x e. ( ( inl " A ) u. ( inr " B ) ) )
85 84 ssriv 
 |-  ( A |_| B ) C_ ( ( inl " A ) u. ( inr " B ) )
86 54 85 eqssi 
 |-  ( ( inl " A ) u. ( inr " B ) ) = ( A |_| B )