Metamath Proof Explorer


Theorem djur

Description: A member of a disjoint union can be mapped from one of the classes which produced it. (Contributed by Jim Kingdon, 23-Jun-2022)

Ref Expression
Assertion djur CA⊔︀BxAC=inlxxBC=inrx

Proof

Step Hyp Ref Expression
1 df-dju A⊔︀B=×A1𝑜×B
2 1 eleq2i CA⊔︀BC×A1𝑜×B
3 elun C×A1𝑜×BC×AC1𝑜×B
4 2 3 sylbb CA⊔︀BC×AC1𝑜×B
5 xp2nd C×A2ndCA
6 1st2nd2 C×AC=1stC2ndC
7 xp1st C×A1stC
8 elsni 1stC1stC=
9 opeq1 1stC=1stC2ndC=2ndC
10 9 eqeq2d 1stC=C=1stC2ndCC=2ndC
11 7 8 10 3syl C×AC=1stC2ndCC=2ndC
12 6 11 mpbid C×AC=2ndC
13 fvexd C×A2ndCV
14 opex 2ndCV
15 opeq2 y=2ndCy=2ndC
16 df-inl inl=yVy
17 15 16 fvmptg 2ndCV2ndCVinl2ndC=2ndC
18 13 14 17 sylancl C×Ainl2ndC=2ndC
19 12 18 eqtr4d C×AC=inl2ndC
20 fveq2 x=2ndCinlx=inl2ndC
21 20 rspceeqv 2ndCAC=inl2ndCxAC=inlx
22 5 19 21 syl2anc C×AxAC=inlx
23 xp2nd C1𝑜×B2ndCB
24 1st2nd2 C1𝑜×BC=1stC2ndC
25 xp1st C1𝑜×B1stC1𝑜
26 elsni 1stC1𝑜1stC=1𝑜
27 opeq1 1stC=1𝑜1stC2ndC=1𝑜2ndC
28 27 eqeq2d 1stC=1𝑜C=1stC2ndCC=1𝑜2ndC
29 25 26 28 3syl C1𝑜×BC=1stC2ndCC=1𝑜2ndC
30 24 29 mpbid C1𝑜×BC=1𝑜2ndC
31 fvexd C1𝑜×B2ndCV
32 opex 1𝑜2ndCV
33 opeq2 z=2ndC1𝑜z=1𝑜2ndC
34 df-inr inr=zV1𝑜z
35 33 34 fvmptg 2ndCV1𝑜2ndCVinr2ndC=1𝑜2ndC
36 31 32 35 sylancl C1𝑜×Binr2ndC=1𝑜2ndC
37 30 36 eqtr4d C1𝑜×BC=inr2ndC
38 fveq2 x=2ndCinrx=inr2ndC
39 38 rspceeqv 2ndCBC=inr2ndCxBC=inrx
40 23 37 39 syl2anc C1𝑜×BxBC=inrx
41 22 40 orim12i C×AC1𝑜×BxAC=inlxxBC=inrx
42 4 41 syl CA⊔︀BxAC=inlxxBC=inrx