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