# Metamath Proof Explorer

## Theorem xppreima2

Description: The preimage of a Cartesian product is the intersection of the preimages of each component function. (Contributed by Thierry Arnoux, 7-Jun-2017)

Ref Expression
Hypotheses xppreima2.1 ${⊢}{\phi }\to {F}:{A}⟶{B}$
xppreima2.2 ${⊢}{\phi }\to {G}:{A}⟶{C}$
xppreima2.3 ${⊢}{H}=\left({x}\in {A}⟼⟨{F}\left({x}\right),{G}\left({x}\right)⟩\right)$
Assertion xppreima2 ${⊢}{\phi }\to {{H}}^{-1}\left[{Y}×{Z}\right]={{F}}^{-1}\left[{Y}\right]\cap {{G}}^{-1}\left[{Z}\right]$

### Proof

Step Hyp Ref Expression
1 xppreima2.1 ${⊢}{\phi }\to {F}:{A}⟶{B}$
2 xppreima2.2 ${⊢}{\phi }\to {G}:{A}⟶{C}$
3 xppreima2.3 ${⊢}{H}=\left({x}\in {A}⟼⟨{F}\left({x}\right),{G}\left({x}\right)⟩\right)$
4 3 funmpt2 ${⊢}\mathrm{Fun}{H}$
5 1 ffvelrnda ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {F}\left({x}\right)\in {B}$
6 2 ffvelrnda ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {G}\left({x}\right)\in {C}$
7 opelxp ${⊢}⟨{F}\left({x}\right),{G}\left({x}\right)⟩\in \left({B}×{C}\right)↔\left({F}\left({x}\right)\in {B}\wedge {G}\left({x}\right)\in {C}\right)$
8 5 6 7 sylanbrc ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to ⟨{F}\left({x}\right),{G}\left({x}\right)⟩\in \left({B}×{C}\right)$
9 8 3 fmptd ${⊢}{\phi }\to {H}:{A}⟶{B}×{C}$
10 9 frnd ${⊢}{\phi }\to \mathrm{ran}{H}\subseteq {B}×{C}$
11 xpss ${⊢}{B}×{C}\subseteq \mathrm{V}×\mathrm{V}$
12 10 11 sstrdi ${⊢}{\phi }\to \mathrm{ran}{H}\subseteq \mathrm{V}×\mathrm{V}$
13 xppreima ${⊢}\left(\mathrm{Fun}{H}\wedge \mathrm{ran}{H}\subseteq \mathrm{V}×\mathrm{V}\right)\to {{H}}^{-1}\left[{Y}×{Z}\right]={\left({1}^{st}\circ {H}\right)}^{-1}\left[{Y}\right]\cap {\left({2}^{nd}\circ {H}\right)}^{-1}\left[{Z}\right]$
14 4 12 13 sylancr ${⊢}{\phi }\to {{H}}^{-1}\left[{Y}×{Z}\right]={\left({1}^{st}\circ {H}\right)}^{-1}\left[{Y}\right]\cap {\left({2}^{nd}\circ {H}\right)}^{-1}\left[{Z}\right]$
15 fo1st ${⊢}{1}^{st}:\mathrm{V}\underset{onto}{⟶}\mathrm{V}$
16 fofn ${⊢}{1}^{st}:\mathrm{V}\underset{onto}{⟶}\mathrm{V}\to {1}^{st}Fn\mathrm{V}$
17 15 16 ax-mp ${⊢}{1}^{st}Fn\mathrm{V}$
18 opex ${⊢}⟨{F}\left({x}\right),{G}\left({x}\right)⟩\in \mathrm{V}$
19 18 3 fnmpti ${⊢}{H}Fn{A}$
20 ssv ${⊢}\mathrm{ran}{H}\subseteq \mathrm{V}$
21 fnco ${⊢}\left({1}^{st}Fn\mathrm{V}\wedge {H}Fn{A}\wedge \mathrm{ran}{H}\subseteq \mathrm{V}\right)\to \left({1}^{st}\circ {H}\right)Fn{A}$
22 17 19 20 21 mp3an ${⊢}\left({1}^{st}\circ {H}\right)Fn{A}$
23 22 a1i ${⊢}{\phi }\to \left({1}^{st}\circ {H}\right)Fn{A}$
24 1 ffnd ${⊢}{\phi }\to {F}Fn{A}$
25 4 a1i ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to \mathrm{Fun}{H}$
26 12 adantr ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to \mathrm{ran}{H}\subseteq \mathrm{V}×\mathrm{V}$
27 simpr ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {x}\in {A}$
28 18 3 dmmpti ${⊢}\mathrm{dom}{H}={A}$
29 27 28 eleqtrrdi ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {x}\in \mathrm{dom}{H}$
30 opfv ${⊢}\left(\left(\mathrm{Fun}{H}\wedge \mathrm{ran}{H}\subseteq \mathrm{V}×\mathrm{V}\right)\wedge {x}\in \mathrm{dom}{H}\right)\to {H}\left({x}\right)=⟨\left({1}^{st}\circ {H}\right)\left({x}\right),\left({2}^{nd}\circ {H}\right)\left({x}\right)⟩$
31 25 26 29 30 syl21anc ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {H}\left({x}\right)=⟨\left({1}^{st}\circ {H}\right)\left({x}\right),\left({2}^{nd}\circ {H}\right)\left({x}\right)⟩$
32 3 fvmpt2 ${⊢}\left({x}\in {A}\wedge ⟨{F}\left({x}\right),{G}\left({x}\right)⟩\in \left({B}×{C}\right)\right)\to {H}\left({x}\right)=⟨{F}\left({x}\right),{G}\left({x}\right)⟩$
33 27 8 32 syl2anc ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {H}\left({x}\right)=⟨{F}\left({x}\right),{G}\left({x}\right)⟩$
34 31 33 eqtr3d ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to ⟨\left({1}^{st}\circ {H}\right)\left({x}\right),\left({2}^{nd}\circ {H}\right)\left({x}\right)⟩=⟨{F}\left({x}\right),{G}\left({x}\right)⟩$
35 fvex ${⊢}\left({1}^{st}\circ {H}\right)\left({x}\right)\in \mathrm{V}$
36 fvex ${⊢}\left({2}^{nd}\circ {H}\right)\left({x}\right)\in \mathrm{V}$
37 35 36 opth ${⊢}⟨\left({1}^{st}\circ {H}\right)\left({x}\right),\left({2}^{nd}\circ {H}\right)\left({x}\right)⟩=⟨{F}\left({x}\right),{G}\left({x}\right)⟩↔\left(\left({1}^{st}\circ {H}\right)\left({x}\right)={F}\left({x}\right)\wedge \left({2}^{nd}\circ {H}\right)\left({x}\right)={G}\left({x}\right)\right)$
38 34 37 sylib ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to \left(\left({1}^{st}\circ {H}\right)\left({x}\right)={F}\left({x}\right)\wedge \left({2}^{nd}\circ {H}\right)\left({x}\right)={G}\left({x}\right)\right)$
39 38 simpld ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to \left({1}^{st}\circ {H}\right)\left({x}\right)={F}\left({x}\right)$
40 23 24 39 eqfnfvd ${⊢}{\phi }\to {1}^{st}\circ {H}={F}$
41 40 cnveqd ${⊢}{\phi }\to {\left({1}^{st}\circ {H}\right)}^{-1}={{F}}^{-1}$
42 41 imaeq1d ${⊢}{\phi }\to {\left({1}^{st}\circ {H}\right)}^{-1}\left[{Y}\right]={{F}}^{-1}\left[{Y}\right]$
43 fo2nd ${⊢}{2}^{nd}:\mathrm{V}\underset{onto}{⟶}\mathrm{V}$
44 fofn ${⊢}{2}^{nd}:\mathrm{V}\underset{onto}{⟶}\mathrm{V}\to {2}^{nd}Fn\mathrm{V}$
45 43 44 ax-mp ${⊢}{2}^{nd}Fn\mathrm{V}$
46 fnco ${⊢}\left({2}^{nd}Fn\mathrm{V}\wedge {H}Fn{A}\wedge \mathrm{ran}{H}\subseteq \mathrm{V}\right)\to \left({2}^{nd}\circ {H}\right)Fn{A}$
47 45 19 20 46 mp3an ${⊢}\left({2}^{nd}\circ {H}\right)Fn{A}$
48 47 a1i ${⊢}{\phi }\to \left({2}^{nd}\circ {H}\right)Fn{A}$
49 2 ffnd ${⊢}{\phi }\to {G}Fn{A}$
50 38 simprd ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to \left({2}^{nd}\circ {H}\right)\left({x}\right)={G}\left({x}\right)$
51 48 49 50 eqfnfvd ${⊢}{\phi }\to {2}^{nd}\circ {H}={G}$
52 51 cnveqd ${⊢}{\phi }\to {\left({2}^{nd}\circ {H}\right)}^{-1}={{G}}^{-1}$
53 52 imaeq1d ${⊢}{\phi }\to {\left({2}^{nd}\circ {H}\right)}^{-1}\left[{Z}\right]={{G}}^{-1}\left[{Z}\right]$
54 42 53 ineq12d ${⊢}{\phi }\to {\left({1}^{st}\circ {H}\right)}^{-1}\left[{Y}\right]\cap {\left({2}^{nd}\circ {H}\right)}^{-1}\left[{Z}\right]={{F}}^{-1}\left[{Y}\right]\cap {{G}}^{-1}\left[{Z}\right]$
55 14 54 eqtrd ${⊢}{\phi }\to {{H}}^{-1}\left[{Y}×{Z}\right]={{F}}^{-1}\left[{Y}\right]\cap {{G}}^{-1}\left[{Z}\right]$