# Metamath Proof Explorer

## Theorem djurcl

Description: Right closure of disjoint union. (Contributed by Jim Kingdon, 21-Jun-2022)

Ref Expression
Assertion djurcl
`|- ( C e. B -> ( inr ` C ) e. ( A |_| B ) )`

### Proof

Step Hyp Ref Expression
1 elex
` |-  ( C e. B -> C e. _V )`
2 1oex
` |-  1o e. _V`
3 2 snid
` |-  1o e. { 1o }`
4 opelxpi
` |-  ( ( 1o e. { 1o } /\ C e. B ) -> <. 1o , C >. e. ( { 1o } X. B ) )`
5 3 4 mpan
` |-  ( C e. B -> <. 1o , C >. e. ( { 1o } X. B ) )`
6 opeq2
` |-  ( x = C -> <. 1o , x >. = <. 1o , C >. )`
7 df-inr
` |-  inr = ( x e. _V |-> <. 1o , x >. )`
8 6 7 fvmptg
` |-  ( ( C e. _V /\ <. 1o , C >. e. ( { 1o } X. B ) ) -> ( inr ` C ) = <. 1o , C >. )`
9 1 5 8 syl2anc
` |-  ( C e. B -> ( inr ` C ) = <. 1o , C >. )`
10 elun2
` |-  ( <. 1o , C >. e. ( { 1o } X. B ) -> <. 1o , C >. e. ( ( { (/) } X. A ) u. ( { 1o } X. B ) ) )`
11 5 10 syl
` |-  ( C e. B -> <. 1o , C >. e. ( ( { (/) } X. A ) u. ( { 1o } X. B ) ) )`
12 df-dju
` |-  ( A |_| B ) = ( ( { (/) } X. A ) u. ( { 1o } X. B ) )`
13 11 12 eleqtrrdi
` |-  ( C e. B -> <. 1o , C >. e. ( A |_| B ) )`
14 9 13 eqeltrd
` |-  ( C e. B -> ( inr ` C ) e. ( A |_| B ) )`