# Metamath Proof Explorer

## Theorem mapunen

Description: Equinumerosity law for set exponentiation of a disjoint union. Exercise 4.45 of Mendelson p. 255. (Contributed by NM, 23-Sep-2004) (Revised by Mario Carneiro, 29-Apr-2015)

Ref Expression
Assertion mapunen ${⊢}\left(\left({A}\in {V}\wedge {B}\in {W}\wedge {C}\in {X}\right)\wedge {A}\cap {B}=\varnothing \right)\to \left({{C}}^{\left({A}\cup {B}\right)}\right)\approx \left(\left({{C}}^{{A}}\right)×\left({{C}}^{{B}}\right)\right)$

### Proof

Step Hyp Ref Expression
1 ovex ${⊢}{{C}}^{\left({A}\cup {B}\right)}\in \mathrm{V}$
2 1 a1i ${⊢}\left(\left({A}\in {V}\wedge {B}\in {W}\wedge {C}\in {X}\right)\wedge {A}\cap {B}=\varnothing \right)\to {{C}}^{\left({A}\cup {B}\right)}\in \mathrm{V}$
3 ovex ${⊢}{{C}}^{{A}}\in \mathrm{V}$
4 ovex ${⊢}{{C}}^{{B}}\in \mathrm{V}$
5 3 4 xpex ${⊢}\left({{C}}^{{A}}\right)×\left({{C}}^{{B}}\right)\in \mathrm{V}$
6 5 a1i ${⊢}\left(\left({A}\in {V}\wedge {B}\in {W}\wedge {C}\in {X}\right)\wedge {A}\cap {B}=\varnothing \right)\to \left({{C}}^{{A}}\right)×\left({{C}}^{{B}}\right)\in \mathrm{V}$
7 elmapi ${⊢}{x}\in \left({{C}}^{\left({A}\cup {B}\right)}\right)\to {x}:{A}\cup {B}⟶{C}$
8 ssun1 ${⊢}{A}\subseteq {A}\cup {B}$
9 fssres ${⊢}\left({x}:{A}\cup {B}⟶{C}\wedge {A}\subseteq {A}\cup {B}\right)\to \left({{x}↾}_{{A}}\right):{A}⟶{C}$
10 7 8 9 sylancl ${⊢}{x}\in \left({{C}}^{\left({A}\cup {B}\right)}\right)\to \left({{x}↾}_{{A}}\right):{A}⟶{C}$
11 ssun2 ${⊢}{B}\subseteq {A}\cup {B}$
12 fssres ${⊢}\left({x}:{A}\cup {B}⟶{C}\wedge {B}\subseteq {A}\cup {B}\right)\to \left({{x}↾}_{{B}}\right):{B}⟶{C}$
13 7 11 12 sylancl ${⊢}{x}\in \left({{C}}^{\left({A}\cup {B}\right)}\right)\to \left({{x}↾}_{{B}}\right):{B}⟶{C}$
14 10 13 jca ${⊢}{x}\in \left({{C}}^{\left({A}\cup {B}\right)}\right)\to \left(\left({{x}↾}_{{A}}\right):{A}⟶{C}\wedge \left({{x}↾}_{{B}}\right):{B}⟶{C}\right)$
15 opelxp ${⊢}⟨{{x}↾}_{{A}},{{x}↾}_{{B}}⟩\in \left(\left({{C}}^{{A}}\right)×\left({{C}}^{{B}}\right)\right)↔\left({{x}↾}_{{A}}\in \left({{C}}^{{A}}\right)\wedge {{x}↾}_{{B}}\in \left({{C}}^{{B}}\right)\right)$
16 simpl3 ${⊢}\left(\left({A}\in {V}\wedge {B}\in {W}\wedge {C}\in {X}\right)\wedge {A}\cap {B}=\varnothing \right)\to {C}\in {X}$
17 simpl1 ${⊢}\left(\left({A}\in {V}\wedge {B}\in {W}\wedge {C}\in {X}\right)\wedge {A}\cap {B}=\varnothing \right)\to {A}\in {V}$
18 16 17 elmapd ${⊢}\left(\left({A}\in {V}\wedge {B}\in {W}\wedge {C}\in {X}\right)\wedge {A}\cap {B}=\varnothing \right)\to \left({{x}↾}_{{A}}\in \left({{C}}^{{A}}\right)↔\left({{x}↾}_{{A}}\right):{A}⟶{C}\right)$
19 simpl2 ${⊢}\left(\left({A}\in {V}\wedge {B}\in {W}\wedge {C}\in {X}\right)\wedge {A}\cap {B}=\varnothing \right)\to {B}\in {W}$
20 16 19 elmapd ${⊢}\left(\left({A}\in {V}\wedge {B}\in {W}\wedge {C}\in {X}\right)\wedge {A}\cap {B}=\varnothing \right)\to \left({{x}↾}_{{B}}\in \left({{C}}^{{B}}\right)↔\left({{x}↾}_{{B}}\right):{B}⟶{C}\right)$
21 18 20 anbi12d ${⊢}\left(\left({A}\in {V}\wedge {B}\in {W}\wedge {C}\in {X}\right)\wedge {A}\cap {B}=\varnothing \right)\to \left(\left({{x}↾}_{{A}}\in \left({{C}}^{{A}}\right)\wedge {{x}↾}_{{B}}\in \left({{C}}^{{B}}\right)\right)↔\left(\left({{x}↾}_{{A}}\right):{A}⟶{C}\wedge \left({{x}↾}_{{B}}\right):{B}⟶{C}\right)\right)$
22 15 21 syl5bb ${⊢}\left(\left({A}\in {V}\wedge {B}\in {W}\wedge {C}\in {X}\right)\wedge {A}\cap {B}=\varnothing \right)\to \left(⟨{{x}↾}_{{A}},{{x}↾}_{{B}}⟩\in \left(\left({{C}}^{{A}}\right)×\left({{C}}^{{B}}\right)\right)↔\left(\left({{x}↾}_{{A}}\right):{A}⟶{C}\wedge \left({{x}↾}_{{B}}\right):{B}⟶{C}\right)\right)$
23 14 22 syl5ibr ${⊢}\left(\left({A}\in {V}\wedge {B}\in {W}\wedge {C}\in {X}\right)\wedge {A}\cap {B}=\varnothing \right)\to \left({x}\in \left({{C}}^{\left({A}\cup {B}\right)}\right)\to ⟨{{x}↾}_{{A}},{{x}↾}_{{B}}⟩\in \left(\left({{C}}^{{A}}\right)×\left({{C}}^{{B}}\right)\right)\right)$
24 xp1st ${⊢}{y}\in \left(\left({{C}}^{{A}}\right)×\left({{C}}^{{B}}\right)\right)\to {1}^{st}\left({y}\right)\in \left({{C}}^{{A}}\right)$
25 24 adantl ${⊢}\left(\left(\left({A}\in {V}\wedge {B}\in {W}\wedge {C}\in {X}\right)\wedge {A}\cap {B}=\varnothing \right)\wedge {y}\in \left(\left({{C}}^{{A}}\right)×\left({{C}}^{{B}}\right)\right)\right)\to {1}^{st}\left({y}\right)\in \left({{C}}^{{A}}\right)$
26 elmapi ${⊢}{1}^{st}\left({y}\right)\in \left({{C}}^{{A}}\right)\to {1}^{st}\left({y}\right):{A}⟶{C}$
27 25 26 syl ${⊢}\left(\left(\left({A}\in {V}\wedge {B}\in {W}\wedge {C}\in {X}\right)\wedge {A}\cap {B}=\varnothing \right)\wedge {y}\in \left(\left({{C}}^{{A}}\right)×\left({{C}}^{{B}}\right)\right)\right)\to {1}^{st}\left({y}\right):{A}⟶{C}$
28 xp2nd ${⊢}{y}\in \left(\left({{C}}^{{A}}\right)×\left({{C}}^{{B}}\right)\right)\to {2}^{nd}\left({y}\right)\in \left({{C}}^{{B}}\right)$
29 28 adantl ${⊢}\left(\left(\left({A}\in {V}\wedge {B}\in {W}\wedge {C}\in {X}\right)\wedge {A}\cap {B}=\varnothing \right)\wedge {y}\in \left(\left({{C}}^{{A}}\right)×\left({{C}}^{{B}}\right)\right)\right)\to {2}^{nd}\left({y}\right)\in \left({{C}}^{{B}}\right)$
30 elmapi ${⊢}{2}^{nd}\left({y}\right)\in \left({{C}}^{{B}}\right)\to {2}^{nd}\left({y}\right):{B}⟶{C}$
31 29 30 syl ${⊢}\left(\left(\left({A}\in {V}\wedge {B}\in {W}\wedge {C}\in {X}\right)\wedge {A}\cap {B}=\varnothing \right)\wedge {y}\in \left(\left({{C}}^{{A}}\right)×\left({{C}}^{{B}}\right)\right)\right)\to {2}^{nd}\left({y}\right):{B}⟶{C}$
32 simplr ${⊢}\left(\left(\left({A}\in {V}\wedge {B}\in {W}\wedge {C}\in {X}\right)\wedge {A}\cap {B}=\varnothing \right)\wedge {y}\in \left(\left({{C}}^{{A}}\right)×\left({{C}}^{{B}}\right)\right)\right)\to {A}\cap {B}=\varnothing$
33 27 31 32 fun2d ${⊢}\left(\left(\left({A}\in {V}\wedge {B}\in {W}\wedge {C}\in {X}\right)\wedge {A}\cap {B}=\varnothing \right)\wedge {y}\in \left(\left({{C}}^{{A}}\right)×\left({{C}}^{{B}}\right)\right)\right)\to \left({1}^{st}\left({y}\right)\cup {2}^{nd}\left({y}\right)\right):{A}\cup {B}⟶{C}$
34 33 ex ${⊢}\left(\left({A}\in {V}\wedge {B}\in {W}\wedge {C}\in {X}\right)\wedge {A}\cap {B}=\varnothing \right)\to \left({y}\in \left(\left({{C}}^{{A}}\right)×\left({{C}}^{{B}}\right)\right)\to \left({1}^{st}\left({y}\right)\cup {2}^{nd}\left({y}\right)\right):{A}\cup {B}⟶{C}\right)$
35 unexg ${⊢}\left({A}\in {V}\wedge {B}\in {W}\right)\to {A}\cup {B}\in \mathrm{V}$
36 17 19 35 syl2anc ${⊢}\left(\left({A}\in {V}\wedge {B}\in {W}\wedge {C}\in {X}\right)\wedge {A}\cap {B}=\varnothing \right)\to {A}\cup {B}\in \mathrm{V}$
37 16 36 elmapd ${⊢}\left(\left({A}\in {V}\wedge {B}\in {W}\wedge {C}\in {X}\right)\wedge {A}\cap {B}=\varnothing \right)\to \left({1}^{st}\left({y}\right)\cup {2}^{nd}\left({y}\right)\in \left({{C}}^{\left({A}\cup {B}\right)}\right)↔\left({1}^{st}\left({y}\right)\cup {2}^{nd}\left({y}\right)\right):{A}\cup {B}⟶{C}\right)$
38 34 37 sylibrd ${⊢}\left(\left({A}\in {V}\wedge {B}\in {W}\wedge {C}\in {X}\right)\wedge {A}\cap {B}=\varnothing \right)\to \left({y}\in \left(\left({{C}}^{{A}}\right)×\left({{C}}^{{B}}\right)\right)\to {1}^{st}\left({y}\right)\cup {2}^{nd}\left({y}\right)\in \left({{C}}^{\left({A}\cup {B}\right)}\right)\right)$
39 1st2nd2 ${⊢}{y}\in \left(\left({{C}}^{{A}}\right)×\left({{C}}^{{B}}\right)\right)\to {y}=⟨{1}^{st}\left({y}\right),{2}^{nd}\left({y}\right)⟩$
40 39 ad2antll ${⊢}\left(\left(\left({A}\in {V}\wedge {B}\in {W}\wedge {C}\in {X}\right)\wedge {A}\cap {B}=\varnothing \right)\wedge \left({x}\in \left({{C}}^{\left({A}\cup {B}\right)}\right)\wedge {y}\in \left(\left({{C}}^{{A}}\right)×\left({{C}}^{{B}}\right)\right)\right)\right)\to {y}=⟨{1}^{st}\left({y}\right),{2}^{nd}\left({y}\right)⟩$
41 27 adantrl ${⊢}\left(\left(\left({A}\in {V}\wedge {B}\in {W}\wedge {C}\in {X}\right)\wedge {A}\cap {B}=\varnothing \right)\wedge \left({x}\in \left({{C}}^{\left({A}\cup {B}\right)}\right)\wedge {y}\in \left(\left({{C}}^{{A}}\right)×\left({{C}}^{{B}}\right)\right)\right)\right)\to {1}^{st}\left({y}\right):{A}⟶{C}$
42 31 adantrl ${⊢}\left(\left(\left({A}\in {V}\wedge {B}\in {W}\wedge {C}\in {X}\right)\wedge {A}\cap {B}=\varnothing \right)\wedge \left({x}\in \left({{C}}^{\left({A}\cup {B}\right)}\right)\wedge {y}\in \left(\left({{C}}^{{A}}\right)×\left({{C}}^{{B}}\right)\right)\right)\right)\to {2}^{nd}\left({y}\right):{B}⟶{C}$
43 res0 ${⊢}{{1}^{st}\left({y}\right)↾}_{\varnothing }=\varnothing$
44 res0 ${⊢}{{2}^{nd}\left({y}\right)↾}_{\varnothing }=\varnothing$
45 43 44 eqtr4i ${⊢}{{1}^{st}\left({y}\right)↾}_{\varnothing }={{2}^{nd}\left({y}\right)↾}_{\varnothing }$
46 simplr ${⊢}\left(\left(\left({A}\in {V}\wedge {B}\in {W}\wedge {C}\in {X}\right)\wedge {A}\cap {B}=\varnothing \right)\wedge \left({x}\in \left({{C}}^{\left({A}\cup {B}\right)}\right)\wedge {y}\in \left(\left({{C}}^{{A}}\right)×\left({{C}}^{{B}}\right)\right)\right)\right)\to {A}\cap {B}=\varnothing$
47 46 reseq2d ${⊢}\left(\left(\left({A}\in {V}\wedge {B}\in {W}\wedge {C}\in {X}\right)\wedge {A}\cap {B}=\varnothing \right)\wedge \left({x}\in \left({{C}}^{\left({A}\cup {B}\right)}\right)\wedge {y}\in \left(\left({{C}}^{{A}}\right)×\left({{C}}^{{B}}\right)\right)\right)\right)\to {{1}^{st}\left({y}\right)↾}_{\left({A}\cap {B}\right)}={{1}^{st}\left({y}\right)↾}_{\varnothing }$
48 46 reseq2d ${⊢}\left(\left(\left({A}\in {V}\wedge {B}\in {W}\wedge {C}\in {X}\right)\wedge {A}\cap {B}=\varnothing \right)\wedge \left({x}\in \left({{C}}^{\left({A}\cup {B}\right)}\right)\wedge {y}\in \left(\left({{C}}^{{A}}\right)×\left({{C}}^{{B}}\right)\right)\right)\right)\to {{2}^{nd}\left({y}\right)↾}_{\left({A}\cap {B}\right)}={{2}^{nd}\left({y}\right)↾}_{\varnothing }$
49 45 47 48 3eqtr4a ${⊢}\left(\left(\left({A}\in {V}\wedge {B}\in {W}\wedge {C}\in {X}\right)\wedge {A}\cap {B}=\varnothing \right)\wedge \left({x}\in \left({{C}}^{\left({A}\cup {B}\right)}\right)\wedge {y}\in \left(\left({{C}}^{{A}}\right)×\left({{C}}^{{B}}\right)\right)\right)\right)\to {{1}^{st}\left({y}\right)↾}_{\left({A}\cap {B}\right)}={{2}^{nd}\left({y}\right)↾}_{\left({A}\cap {B}\right)}$
50 fresaunres1 ${⊢}\left({1}^{st}\left({y}\right):{A}⟶{C}\wedge {2}^{nd}\left({y}\right):{B}⟶{C}\wedge {{1}^{st}\left({y}\right)↾}_{\left({A}\cap {B}\right)}={{2}^{nd}\left({y}\right)↾}_{\left({A}\cap {B}\right)}\right)\to {\left({1}^{st}\left({y}\right)\cup {2}^{nd}\left({y}\right)\right)↾}_{{A}}={1}^{st}\left({y}\right)$
51 41 42 49 50 syl3anc ${⊢}\left(\left(\left({A}\in {V}\wedge {B}\in {W}\wedge {C}\in {X}\right)\wedge {A}\cap {B}=\varnothing \right)\wedge \left({x}\in \left({{C}}^{\left({A}\cup {B}\right)}\right)\wedge {y}\in \left(\left({{C}}^{{A}}\right)×\left({{C}}^{{B}}\right)\right)\right)\right)\to {\left({1}^{st}\left({y}\right)\cup {2}^{nd}\left({y}\right)\right)↾}_{{A}}={1}^{st}\left({y}\right)$
52 fresaunres2 ${⊢}\left({1}^{st}\left({y}\right):{A}⟶{C}\wedge {2}^{nd}\left({y}\right):{B}⟶{C}\wedge {{1}^{st}\left({y}\right)↾}_{\left({A}\cap {B}\right)}={{2}^{nd}\left({y}\right)↾}_{\left({A}\cap {B}\right)}\right)\to {\left({1}^{st}\left({y}\right)\cup {2}^{nd}\left({y}\right)\right)↾}_{{B}}={2}^{nd}\left({y}\right)$
53 41 42 49 52 syl3anc ${⊢}\left(\left(\left({A}\in {V}\wedge {B}\in {W}\wedge {C}\in {X}\right)\wedge {A}\cap {B}=\varnothing \right)\wedge \left({x}\in \left({{C}}^{\left({A}\cup {B}\right)}\right)\wedge {y}\in \left(\left({{C}}^{{A}}\right)×\left({{C}}^{{B}}\right)\right)\right)\right)\to {\left({1}^{st}\left({y}\right)\cup {2}^{nd}\left({y}\right)\right)↾}_{{B}}={2}^{nd}\left({y}\right)$
54 51 53 opeq12d ${⊢}\left(\left(\left({A}\in {V}\wedge {B}\in {W}\wedge {C}\in {X}\right)\wedge {A}\cap {B}=\varnothing \right)\wedge \left({x}\in \left({{C}}^{\left({A}\cup {B}\right)}\right)\wedge {y}\in \left(\left({{C}}^{{A}}\right)×\left({{C}}^{{B}}\right)\right)\right)\right)\to ⟨{\left({1}^{st}\left({y}\right)\cup {2}^{nd}\left({y}\right)\right)↾}_{{A}},{\left({1}^{st}\left({y}\right)\cup {2}^{nd}\left({y}\right)\right)↾}_{{B}}⟩=⟨{1}^{st}\left({y}\right),{2}^{nd}\left({y}\right)⟩$
55 40 54 eqtr4d ${⊢}\left(\left(\left({A}\in {V}\wedge {B}\in {W}\wedge {C}\in {X}\right)\wedge {A}\cap {B}=\varnothing \right)\wedge \left({x}\in \left({{C}}^{\left({A}\cup {B}\right)}\right)\wedge {y}\in \left(\left({{C}}^{{A}}\right)×\left({{C}}^{{B}}\right)\right)\right)\right)\to {y}=⟨{\left({1}^{st}\left({y}\right)\cup {2}^{nd}\left({y}\right)\right)↾}_{{A}},{\left({1}^{st}\left({y}\right)\cup {2}^{nd}\left({y}\right)\right)↾}_{{B}}⟩$
56 reseq1 ${⊢}{x}={1}^{st}\left({y}\right)\cup {2}^{nd}\left({y}\right)\to {{x}↾}_{{A}}={\left({1}^{st}\left({y}\right)\cup {2}^{nd}\left({y}\right)\right)↾}_{{A}}$
57 reseq1 ${⊢}{x}={1}^{st}\left({y}\right)\cup {2}^{nd}\left({y}\right)\to {{x}↾}_{{B}}={\left({1}^{st}\left({y}\right)\cup {2}^{nd}\left({y}\right)\right)↾}_{{B}}$
58 56 57 opeq12d ${⊢}{x}={1}^{st}\left({y}\right)\cup {2}^{nd}\left({y}\right)\to ⟨{{x}↾}_{{A}},{{x}↾}_{{B}}⟩=⟨{\left({1}^{st}\left({y}\right)\cup {2}^{nd}\left({y}\right)\right)↾}_{{A}},{\left({1}^{st}\left({y}\right)\cup {2}^{nd}\left({y}\right)\right)↾}_{{B}}⟩$
59 58 eqeq2d ${⊢}{x}={1}^{st}\left({y}\right)\cup {2}^{nd}\left({y}\right)\to \left({y}=⟨{{x}↾}_{{A}},{{x}↾}_{{B}}⟩↔{y}=⟨{\left({1}^{st}\left({y}\right)\cup {2}^{nd}\left({y}\right)\right)↾}_{{A}},{\left({1}^{st}\left({y}\right)\cup {2}^{nd}\left({y}\right)\right)↾}_{{B}}⟩\right)$
60 55 59 syl5ibrcom ${⊢}\left(\left(\left({A}\in {V}\wedge {B}\in {W}\wedge {C}\in {X}\right)\wedge {A}\cap {B}=\varnothing \right)\wedge \left({x}\in \left({{C}}^{\left({A}\cup {B}\right)}\right)\wedge {y}\in \left(\left({{C}}^{{A}}\right)×\left({{C}}^{{B}}\right)\right)\right)\right)\to \left({x}={1}^{st}\left({y}\right)\cup {2}^{nd}\left({y}\right)\to {y}=⟨{{x}↾}_{{A}},{{x}↾}_{{B}}⟩\right)$
61 ffn ${⊢}{x}:{A}\cup {B}⟶{C}\to {x}Fn\left({A}\cup {B}\right)$
62 fnresdm ${⊢}{x}Fn\left({A}\cup {B}\right)\to {{x}↾}_{\left({A}\cup {B}\right)}={x}$
63 7 61 62 3syl ${⊢}{x}\in \left({{C}}^{\left({A}\cup {B}\right)}\right)\to {{x}↾}_{\left({A}\cup {B}\right)}={x}$
64 63 ad2antrl ${⊢}\left(\left(\left({A}\in {V}\wedge {B}\in {W}\wedge {C}\in {X}\right)\wedge {A}\cap {B}=\varnothing \right)\wedge \left({x}\in \left({{C}}^{\left({A}\cup {B}\right)}\right)\wedge {y}\in \left(\left({{C}}^{{A}}\right)×\left({{C}}^{{B}}\right)\right)\right)\right)\to {{x}↾}_{\left({A}\cup {B}\right)}={x}$
65 64 eqcomd ${⊢}\left(\left(\left({A}\in {V}\wedge {B}\in {W}\wedge {C}\in {X}\right)\wedge {A}\cap {B}=\varnothing \right)\wedge \left({x}\in \left({{C}}^{\left({A}\cup {B}\right)}\right)\wedge {y}\in \left(\left({{C}}^{{A}}\right)×\left({{C}}^{{B}}\right)\right)\right)\right)\to {x}={{x}↾}_{\left({A}\cup {B}\right)}$
66 vex ${⊢}{x}\in \mathrm{V}$
67 66 resex ${⊢}{{x}↾}_{{A}}\in \mathrm{V}$
68 66 resex ${⊢}{{x}↾}_{{B}}\in \mathrm{V}$
69 67 68 op1std ${⊢}{y}=⟨{{x}↾}_{{A}},{{x}↾}_{{B}}⟩\to {1}^{st}\left({y}\right)={{x}↾}_{{A}}$
70 67 68 op2ndd ${⊢}{y}=⟨{{x}↾}_{{A}},{{x}↾}_{{B}}⟩\to {2}^{nd}\left({y}\right)={{x}↾}_{{B}}$
71 69 70 uneq12d ${⊢}{y}=⟨{{x}↾}_{{A}},{{x}↾}_{{B}}⟩\to {1}^{st}\left({y}\right)\cup {2}^{nd}\left({y}\right)=\left({{x}↾}_{{A}}\right)\cup \left({{x}↾}_{{B}}\right)$
72 resundi ${⊢}{{x}↾}_{\left({A}\cup {B}\right)}=\left({{x}↾}_{{A}}\right)\cup \left({{x}↾}_{{B}}\right)$
73 71 72 syl6eqr ${⊢}{y}=⟨{{x}↾}_{{A}},{{x}↾}_{{B}}⟩\to {1}^{st}\left({y}\right)\cup {2}^{nd}\left({y}\right)={{x}↾}_{\left({A}\cup {B}\right)}$
74 73 eqeq2d ${⊢}{y}=⟨{{x}↾}_{{A}},{{x}↾}_{{B}}⟩\to \left({x}={1}^{st}\left({y}\right)\cup {2}^{nd}\left({y}\right)↔{x}={{x}↾}_{\left({A}\cup {B}\right)}\right)$
75 65 74 syl5ibrcom ${⊢}\left(\left(\left({A}\in {V}\wedge {B}\in {W}\wedge {C}\in {X}\right)\wedge {A}\cap {B}=\varnothing \right)\wedge \left({x}\in \left({{C}}^{\left({A}\cup {B}\right)}\right)\wedge {y}\in \left(\left({{C}}^{{A}}\right)×\left({{C}}^{{B}}\right)\right)\right)\right)\to \left({y}=⟨{{x}↾}_{{A}},{{x}↾}_{{B}}⟩\to {x}={1}^{st}\left({y}\right)\cup {2}^{nd}\left({y}\right)\right)$
76 60 75 impbid ${⊢}\left(\left(\left({A}\in {V}\wedge {B}\in {W}\wedge {C}\in {X}\right)\wedge {A}\cap {B}=\varnothing \right)\wedge \left({x}\in \left({{C}}^{\left({A}\cup {B}\right)}\right)\wedge {y}\in \left(\left({{C}}^{{A}}\right)×\left({{C}}^{{B}}\right)\right)\right)\right)\to \left({x}={1}^{st}\left({y}\right)\cup {2}^{nd}\left({y}\right)↔{y}=⟨{{x}↾}_{{A}},{{x}↾}_{{B}}⟩\right)$
77 76 ex ${⊢}\left(\left({A}\in {V}\wedge {B}\in {W}\wedge {C}\in {X}\right)\wedge {A}\cap {B}=\varnothing \right)\to \left(\left({x}\in \left({{C}}^{\left({A}\cup {B}\right)}\right)\wedge {y}\in \left(\left({{C}}^{{A}}\right)×\left({{C}}^{{B}}\right)\right)\right)\to \left({x}={1}^{st}\left({y}\right)\cup {2}^{nd}\left({y}\right)↔{y}=⟨{{x}↾}_{{A}},{{x}↾}_{{B}}⟩\right)\right)$
78 2 6 23 38 77 en3d ${⊢}\left(\left({A}\in {V}\wedge {B}\in {W}\wedge {C}\in {X}\right)\wedge {A}\cap {B}=\varnothing \right)\to \left({{C}}^{\left({A}\cup {B}\right)}\right)\approx \left(\left({{C}}^{{A}}\right)×\left({{C}}^{{B}}\right)\right)$