This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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