# Metamath Proof Explorer

## Theorem djulcl

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

Ref Expression
Assertion djulcl
`|- ( C e. A -> ( inl ` C ) e. ( A |_| B ) )`

### Proof

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