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	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 )
6	2	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑥 ) ∈ 𝐶 )
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	⊢ ( 𝜑 → ( ◡ 𝐻 “ ( 𝑌 × 𝑍 ) ) = ( ( ◡ 𝐹 “ 𝑌 ) ∩ ( ◡ 𝐺 “ 𝑍 ) ) )