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