Metamath Proof Explorer

Theorem djuss

Description: A disjoint union is a subclass of a Cartesian product. (Contributed by AV, 25-Jun-2022)

Ref Expression
Assertion djuss 
|- ( A |_| B ) C_ ( { (/) , 1o } X. ( A u. B ) )

Proof

Step Hyp Ref Expression
1 djur 
 |-  ( x e. ( A |_| B ) -> ( E. y e. A x = ( inl ` y ) \/ E. y e. B x = ( inr ` y ) ) )
2 simpr 
 |-  ( ( y e. A /\ x = ( inl ` y ) ) -> x = ( inl ` y ) )
3 df-inl 
 |-  inl = ( x e. _V |-> <. (/) , x >. )
4 opeq2 
 |-  ( x = y -> <. (/) , x >. = <. (/) , y >. )
5 elex 
 |-  ( y e. A -> y e. _V )
6 opex 
 |-  <. (/) , y >. e. _V
7 6 a1i 
 |-  ( y e. A -> <. (/) , y >. e. _V )
8 3 4 5 7 fvmptd3 
 |-  ( y e. A -> ( inl ` y ) = <. (/) , y >. )
9 8 adantr 
 |-  ( ( y e. A /\ x = ( inl ` y ) ) -> ( inl ` y ) = <. (/) , y >. )
10 2 9 eqtrd 
 |-  ( ( y e. A /\ x = ( inl ` y ) ) -> x = <. (/) , y >. )
11 elun1 
 |-  ( y e. A -> y e. ( A u. B ) )
12 0ex 
 |-  (/) e. _V
13 12 prid1 
 |-  (/) e. { (/) , 1o }
14 11 13 jctil 
 |-  ( y e. A -> ( (/) e. { (/) , 1o } /\ y e. ( A u. B ) ) )
15 14 adantr 
 |-  ( ( y e. A /\ x = ( inl ` y ) ) -> ( (/) e. { (/) , 1o } /\ y e. ( A u. B ) ) )
16 opelxp 
 |-  ( <. (/) , y >. e. ( { (/) , 1o } X. ( A u. B ) ) <-> ( (/) e. { (/) , 1o } /\ y e. ( A u. B ) ) )
17 15 16 sylibr 
 |-  ( ( y e. A /\ x = ( inl ` y ) ) -> <. (/) , y >. e. ( { (/) , 1o } X. ( A u. B ) ) )
18 10 17 eqeltrd 
 |-  ( ( y e. A /\ x = ( inl ` y ) ) -> x e. ( { (/) , 1o } X. ( A u. B ) ) )
19 18 rexlimiva 
 |-  ( E. y e. A x = ( inl ` y ) -> x e. ( { (/) , 1o } X. ( A u. B ) ) )
20 simpr 
 |-  ( ( y e. B /\ x = ( inr ` y ) ) -> x = ( inr ` y ) )
21 df-inr 
 |-  inr = ( x e. _V |-> <. 1o , x >. )
22 opeq2 
 |-  ( x = y -> <. 1o , x >. = <. 1o , y >. )
23 elex 
 |-  ( y e. B -> y e. _V )
24 opex 
 |-  <. 1o , y >. e. _V
25 24 a1i 
 |-  ( y e. B -> <. 1o , y >. e. _V )
26 21 22 23 25 fvmptd3 
 |-  ( y e. B -> ( inr ` y ) = <. 1o , y >. )
27 26 adantr 
 |-  ( ( y e. B /\ x = ( inr ` y ) ) -> ( inr ` y ) = <. 1o , y >. )
28 20 27 eqtrd 
 |-  ( ( y e. B /\ x = ( inr ` y ) ) -> x = <. 1o , y >. )
29 elun2 
 |-  ( y e. B -> y e. ( A u. B ) )
30 29 adantr 
 |-  ( ( y e. B /\ x = ( inr ` y ) ) -> y e. ( A u. B ) )
31 1oex 
 |-  1o e. _V
32 31 prid2 
 |-  1o e. { (/) , 1o }
33 30 32 jctil 
 |-  ( ( y e. B /\ x = ( inr ` y ) ) -> ( 1o e. { (/) , 1o } /\ y e. ( A u. B ) ) )
34 opelxp 
 |-  ( <. 1o , y >. e. ( { (/) , 1o } X. ( A u. B ) ) <-> ( 1o e. { (/) , 1o } /\ y e. ( A u. B ) ) )
35 33 34 sylibr 
 |-  ( ( y e. B /\ x = ( inr ` y ) ) -> <. 1o , y >. e. ( { (/) , 1o } X. ( A u. B ) ) )
36 28 35 eqeltrd 
 |-  ( ( y e. B /\ x = ( inr ` y ) ) -> x e. ( { (/) , 1o } X. ( A u. B ) ) )
37 36 rexlimiva 
 |-  ( E. y e. B x = ( inr ` y ) -> x e. ( { (/) , 1o } X. ( A u. B ) ) )
38 19 37 jaoi 
 |-  ( ( E. y e. A x = ( inl ` y ) \/ E. y e. B x = ( inr ` y ) ) -> x e. ( { (/) , 1o } X. ( A u. B ) ) )
39 1 38 syl 
 |-  ( x e. ( A |_| B ) -> x e. ( { (/) , 1o } X. ( A u. B ) ) )
40 39 ssriv 
 |-  ( A |_| B ) C_ ( { (/) , 1o } X. ( A u. B ) )