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

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 ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
xppreima2.2 ⊢ ( 𝜑 → 𝐺 : 𝐴 ⟶ 𝐶 )
xppreima2.3 ⊢ 𝐻 = ( 𝑥 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ )
Assertion xppreima2 ( 𝜑 → ( ◡ 𝐻 “ ( 𝑌 × 𝑍 ) ) = ( ( ◡ 𝐹 “ 𝑌 ) ∩ ( ◡ 𝐺 “ 𝑍 ) ) )

Proof

Step Hyp Ref Expression
1 xppreima2.1 ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
2 xppreima2.2 ⊢ ( 𝜑 → 𝐺 : 𝐴 ⟶ 𝐶 )
3 xppreima2.3 ⊢ 𝐻 = ( 𝑥 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ )
4 3 funmpt2 ⊢ Fun 𝐻
5 1 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 )
6 2 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑥 ) ∈ 𝐶 )
7 opelxp ⊢ ( ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ∈ ( 𝐵 × 𝐶 ) ↔ ( ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ∧ ( 𝐺 ‘ 𝑥 ) ∈ 𝐶 ) )
8 5 6 7 sylanbrc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ∈ ( 𝐵 × 𝐶 ) )
9 8 3 fmptd ⊢ ( 𝜑 → 𝐻 : 𝐴 ⟶ ( 𝐵 × 𝐶 ) )
10 9 frnd ⊢ ( 𝜑 → ran 𝐻 ⊆ ( 𝐵 × 𝐶 ) )
11 xpss ⊢ ( 𝐵 × 𝐶 ) ⊆ ( V × V )
12 10 11 sstrdi ⊢ ( 𝜑 → ran 𝐻 ⊆ ( V × V ) )
13 xppreima ⊢ ( ( Fun 𝐻 ∧ ran 𝐻 ⊆ ( V × V ) ) → ( ◡ 𝐻 “ ( 𝑌 × 𝑍 ) ) = ( ( ◡ ( 1st ∘ 𝐻 ) “ 𝑌 ) ∩ ( ◡ ( 2nd ∘ 𝐻 ) “ 𝑍 ) ) )
14 4 12 13 sylancr ⊢ ( 𝜑 → ( ◡ 𝐻 “ ( 𝑌 × 𝑍 ) ) = ( ( ◡ ( 1st ∘ 𝐻 ) “ 𝑌 ) ∩ ( ◡ ( 2nd ∘ 𝐻 ) “ 𝑍 ) ) )
15 fo1st ⊢ 1st : V –onto→ V
16 fofn ⊢ ( 1st : V –onto→ V → 1st Fn V )
17 15 16 ax-mp ⊢ 1st Fn V
18 opex ⊢ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ∈ V
19 18 3 fnmpti ⊢ 𝐻 Fn 𝐴
20 ssv ⊢ ran 𝐻 ⊆ V
21 fnco ⊢ ( ( 1st Fn V ∧ 𝐻 Fn 𝐴 ∧ ran 𝐻 ⊆ V ) → ( 1st ∘ 𝐻 ) Fn 𝐴 )
22 17 19 20 21 mp3an ⊢ ( 1st ∘ 𝐻 ) Fn 𝐴
23 22 a1i ⊢ ( 𝜑 → ( 1st ∘ 𝐻 ) Fn 𝐴 )
24 1 ffnd ⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
25 4 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → Fun 𝐻 )
26 12 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ran 𝐻 ⊆ ( V × V ) )
27 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐴 )
28 18 3 dmmpti ⊢ dom 𝐻 = 𝐴
29 27 28 eleqtrrdi ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ dom 𝐻 )
30 opfv ⊢ ( ( ( Fun 𝐻 ∧ ran 𝐻 ⊆ ( V × V ) ) ∧ 𝑥 ∈ dom 𝐻 ) → ( 𝐻 ‘ 𝑥 ) = ⟨ ( ( 1st ∘ 𝐻 ) ‘ 𝑥 ) , ( ( 2nd ∘ 𝐻 ) ‘ 𝑥 ) ⟩ )
31 25 26 29 30 syl21anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐻 ‘ 𝑥 ) = ⟨ ( ( 1st ∘ 𝐻 ) ‘ 𝑥 ) , ( ( 2nd ∘ 𝐻 ) ‘ 𝑥 ) ⟩ )
32 3 fvmpt2 ⊢ ( ( 𝑥 ∈ 𝐴 ∧ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ∈ ( 𝐵 × 𝐶 ) ) → ( 𝐻 ‘ 𝑥 ) = ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ )
33 27 8 32 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐻 ‘ 𝑥 ) = ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ )
34 31 33 eqtr3d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ⟨ ( ( 1st ∘ 𝐻 ) ‘ 𝑥 ) , ( ( 2nd ∘ 𝐻 ) ‘ 𝑥 ) ⟩ = ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ )
35 fvex ⊢ ( ( 1st ∘ 𝐻 ) ‘ 𝑥 ) ∈ V
36 fvex ⊢ ( ( 2nd ∘ 𝐻 ) ‘ 𝑥 ) ∈ V
37 35 36 opth ⊢ ( ⟨ ( ( 1st ∘ 𝐻 ) ‘ 𝑥 ) , ( ( 2nd ∘ 𝐻 ) ‘ 𝑥 ) ⟩ = ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ↔ ( ( ( 1st ∘ 𝐻 ) ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) ∧ ( ( 2nd ∘ 𝐻 ) ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) )
38 34 37 sylib ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( ( 1st ∘ 𝐻 ) ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) ∧ ( ( 2nd ∘ 𝐻 ) ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) )
39 38 simpld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( 1st ∘ 𝐻 ) ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
40 23 24 39 eqfnfvd ⊢ ( 𝜑 → ( 1st ∘ 𝐻 ) = 𝐹 )
41 40 cnveqd ⊢ ( 𝜑 → ◡ ( 1st ∘ 𝐻 ) = ◡ 𝐹 )
42 41 imaeq1d ⊢ ( 𝜑 → ( ◡ ( 1st ∘ 𝐻 ) “ 𝑌 ) = ( ◡ 𝐹 “ 𝑌 ) )
43 fo2nd ⊢ 2nd : V –onto→ V
44 fofn ⊢ ( 2nd : V –onto→ V → 2nd Fn V )
45 43 44 ax-mp ⊢ 2nd Fn V
46 fnco ⊢ ( ( 2nd Fn V ∧ 𝐻 Fn 𝐴 ∧ ran 𝐻 ⊆ V ) → ( 2nd ∘ 𝐻 ) Fn 𝐴 )
47 45 19 20 46 mp3an ⊢ ( 2nd ∘ 𝐻 ) Fn 𝐴
48 47 a1i ⊢ ( 𝜑 → ( 2nd ∘ 𝐻 ) Fn 𝐴 )
49 2 ffnd ⊢ ( 𝜑 → 𝐺 Fn 𝐴 )
50 38 simprd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( 2nd ∘ 𝐻 ) ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) )
51 48 49 50 eqfnfvd ⊢ ( 𝜑 → ( 2nd ∘ 𝐻 ) = 𝐺 )
52 51 cnveqd ⊢ ( 𝜑 → ◡ ( 2nd ∘ 𝐻 ) = ◡ 𝐺 )
53 52 imaeq1d ⊢ ( 𝜑 → ( ◡ ( 2nd ∘ 𝐻 ) “ 𝑍 ) = ( ◡ 𝐺 “ 𝑍 ) )
54 42 53 ineq12d ⊢ ( 𝜑 → ( ( ◡ ( 1st ∘ 𝐻 ) “ 𝑌 ) ∩ ( ◡ ( 2nd ∘ 𝐻 ) “ 𝑍 ) ) = ( ( ◡ 𝐹 “ 𝑌 ) ∩ ( ◡ 𝐺 “ 𝑍 ) ) )
55 14 54 eqtrd ⊢ ( 𝜑 → ( ◡ 𝐻 “ ( 𝑌 × 𝑍 ) ) = ( ( ◡ 𝐹 “ 𝑌 ) ∩ ( ◡ 𝐺 “ 𝑍 ) ) )