fimaproj

Description: Image of a cartesian product for a function on ordered pairs with values expressed as ordered pairs. Note that F and G are the projections of H to the first and second coordinate respectively. (Contributed by Thierry Arnoux, 30-Dec-2019)

	Ref	Expression
Hypotheses	fvproj.h	⊢ 𝐻 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑦 ) ⟩ )
	fimaproj.f	⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
	fimaproj.g	⊢ ( 𝜑 → 𝐺 Fn 𝐵 )
	fimaproj.x	⊢ ( 𝜑 → 𝑋 ⊆ 𝐴 )
	fimaproj.y	⊢ ( 𝜑 → 𝑌 ⊆ 𝐵 )
Assertion	fimaproj	⊢ ( 𝜑 → ( 𝐻 “ ( 𝑋 × 𝑌 ) ) = ( ( 𝐹 “ 𝑋 ) × ( 𝐺 “ 𝑌 ) ) )

Proof

Step	Hyp	Ref	Expression
1		fvproj.h	⊢ 𝐻 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑦 ) ⟩ )
2		fimaproj.f	⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
3		fimaproj.g	⊢ ( 𝜑 → 𝐺 Fn 𝐵 )
4		fimaproj.x	⊢ ( 𝜑 → 𝑋 ⊆ 𝐴 )
5		fimaproj.y	⊢ ( 𝜑 → 𝑌 ⊆ 𝐵 )
6		opex	⊢ ⟨ ( 𝐹 ‘ ( 1^st ‘ 𝑧 ) ) , ( 𝐺 ‘ ( 2^nd ‘ 𝑧 ) ) ⟩ ∈ V
7		vex	⊢ 𝑥 ∈ V
8		vex	⊢ 𝑦 ∈ V
9	7 8	op1std	⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 1^st ‘ 𝑧 ) = 𝑥 )
10	9	fveq2d	⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝐹 ‘ ( 1^st ‘ 𝑧 ) ) = ( 𝐹 ‘ 𝑥 ) )
11	7 8	op2ndd	⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 2^nd ‘ 𝑧 ) = 𝑦 )
12	11	fveq2d	⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝐺 ‘ ( 2^nd ‘ 𝑧 ) ) = ( 𝐺 ‘ 𝑦 ) )
13	10 12	opeq12d	⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ⟨ ( 𝐹 ‘ ( 1^st ‘ 𝑧 ) ) , ( 𝐺 ‘ ( 2^nd ‘ 𝑧 ) ) ⟩ = ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑦 ) ⟩ )
14	13	mpompt	⊢ ( 𝑧 ∈ ( 𝐴 × 𝐵 ) ↦ ⟨ ( 𝐹 ‘ ( 1^st ‘ 𝑧 ) ) , ( 𝐺 ‘ ( 2^nd ‘ 𝑧 ) ) ⟩ ) = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑦 ) ⟩ )
15	1 14	eqtr4i	⊢ 𝐻 = ( 𝑧 ∈ ( 𝐴 × 𝐵 ) ↦ ⟨ ( 𝐹 ‘ ( 1^st ‘ 𝑧 ) ) , ( 𝐺 ‘ ( 2^nd ‘ 𝑧 ) ) ⟩ )
16	6 15	fnmpti	⊢ 𝐻 Fn ( 𝐴 × 𝐵 )
17		xpss12	⊢ ( ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐵 ) → ( 𝑋 × 𝑌 ) ⊆ ( 𝐴 × 𝐵 ) )
18	4 5 17	syl2anc	⊢ ( 𝜑 → ( 𝑋 × 𝑌 ) ⊆ ( 𝐴 × 𝐵 ) )
19		fvelimab	⊢ ( ( 𝐻 Fn ( 𝐴 × 𝐵 ) ∧ ( 𝑋 × 𝑌 ) ⊆ ( 𝐴 × 𝐵 ) ) → ( 𝑐 ∈ ( 𝐻 “ ( 𝑋 × 𝑌 ) ) ↔ ∃ 𝑧 ∈ ( 𝑋 × 𝑌 ) ( 𝐻 ‘ 𝑧 ) = 𝑐 ) )
20	16 18 19	sylancr	⊢ ( 𝜑 → ( 𝑐 ∈ ( 𝐻 “ ( 𝑋 × 𝑌 ) ) ↔ ∃ 𝑧 ∈ ( 𝑋 × 𝑌 ) ( 𝐻 ‘ 𝑧 ) = 𝑐 ) )
21		simp-4r	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( ( 𝐹 “ 𝑋 ) × ( 𝐺 “ 𝑌 ) ) ) ∧ 𝑎 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑎 ) = ( 1^st ‘ 𝑐 ) ) ∧ 𝑏 ∈ 𝑌 ) ∧ ( 𝐺 ‘ 𝑏 ) = ( 2^nd ‘ 𝑐 ) ) → 𝑎 ∈ 𝑋 )
22		simplr	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( ( 𝐹 “ 𝑋 ) × ( 𝐺 “ 𝑌 ) ) ) ∧ 𝑎 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑎 ) = ( 1^st ‘ 𝑐 ) ) ∧ 𝑏 ∈ 𝑌 ) ∧ ( 𝐺 ‘ 𝑏 ) = ( 2^nd ‘ 𝑐 ) ) → 𝑏 ∈ 𝑌 )
23		opelxpi	⊢ ( ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌 ) → ⟨ 𝑎 , 𝑏 ⟩ ∈ ( 𝑋 × 𝑌 ) )
24	21 22 23	syl2anc	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( ( 𝐹 “ 𝑋 ) × ( 𝐺 “ 𝑌 ) ) ) ∧ 𝑎 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑎 ) = ( 1^st ‘ 𝑐 ) ) ∧ 𝑏 ∈ 𝑌 ) ∧ ( 𝐺 ‘ 𝑏 ) = ( 2^nd ‘ 𝑐 ) ) → ⟨ 𝑎 , 𝑏 ⟩ ∈ ( 𝑋 × 𝑌 ) )
25		simpllr	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( ( 𝐹 “ 𝑋 ) × ( 𝐺 “ 𝑌 ) ) ) ∧ 𝑎 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑎 ) = ( 1^st ‘ 𝑐 ) ) ∧ 𝑏 ∈ 𝑌 ) ∧ ( 𝐺 ‘ 𝑏 ) = ( 2^nd ‘ 𝑐 ) ) → ( 𝐹 ‘ 𝑎 ) = ( 1^st ‘ 𝑐 ) )
26		simpr	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( ( 𝐹 “ 𝑋 ) × ( 𝐺 “ 𝑌 ) ) ) ∧ 𝑎 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑎 ) = ( 1^st ‘ 𝑐 ) ) ∧ 𝑏 ∈ 𝑌 ) ∧ ( 𝐺 ‘ 𝑏 ) = ( 2^nd ‘ 𝑐 ) ) → ( 𝐺 ‘ 𝑏 ) = ( 2^nd ‘ 𝑐 ) )
27	25 26	opeq12d	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( ( 𝐹 “ 𝑋 ) × ( 𝐺 “ 𝑌 ) ) ) ∧ 𝑎 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑎 ) = ( 1^st ‘ 𝑐 ) ) ∧ 𝑏 ∈ 𝑌 ) ∧ ( 𝐺 ‘ 𝑏 ) = ( 2^nd ‘ 𝑐 ) ) → ⟨ ( 𝐹 ‘ 𝑎 ) , ( 𝐺 ‘ 𝑏 ) ⟩ = ⟨ ( 1^st ‘ 𝑐 ) , ( 2^nd ‘ 𝑐 ) ⟩ )
28	4	ad5antr	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( ( 𝐹 “ 𝑋 ) × ( 𝐺 “ 𝑌 ) ) ) ∧ 𝑎 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑎 ) = ( 1^st ‘ 𝑐 ) ) ∧ 𝑏 ∈ 𝑌 ) ∧ ( 𝐺 ‘ 𝑏 ) = ( 2^nd ‘ 𝑐 ) ) → 𝑋 ⊆ 𝐴 )
29	28 21	sseldd	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( ( 𝐹 “ 𝑋 ) × ( 𝐺 “ 𝑌 ) ) ) ∧ 𝑎 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑎 ) = ( 1^st ‘ 𝑐 ) ) ∧ 𝑏 ∈ 𝑌 ) ∧ ( 𝐺 ‘ 𝑏 ) = ( 2^nd ‘ 𝑐 ) ) → 𝑎 ∈ 𝐴 )
30	5	ad5antr	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( ( 𝐹 “ 𝑋 ) × ( 𝐺 “ 𝑌 ) ) ) ∧ 𝑎 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑎 ) = ( 1^st ‘ 𝑐 ) ) ∧ 𝑏 ∈ 𝑌 ) ∧ ( 𝐺 ‘ 𝑏 ) = ( 2^nd ‘ 𝑐 ) ) → 𝑌 ⊆ 𝐵 )
31	30 22	sseldd	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( ( 𝐹 “ 𝑋 ) × ( 𝐺 “ 𝑌 ) ) ) ∧ 𝑎 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑎 ) = ( 1^st ‘ 𝑐 ) ) ∧ 𝑏 ∈ 𝑌 ) ∧ ( 𝐺 ‘ 𝑏 ) = ( 2^nd ‘ 𝑐 ) ) → 𝑏 ∈ 𝐵 )
32	1 29 31	fvproj	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( ( 𝐹 “ 𝑋 ) × ( 𝐺 “ 𝑌 ) ) ) ∧ 𝑎 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑎 ) = ( 1^st ‘ 𝑐 ) ) ∧ 𝑏 ∈ 𝑌 ) ∧ ( 𝐺 ‘ 𝑏 ) = ( 2^nd ‘ 𝑐 ) ) → ( 𝐻 ‘ ⟨ 𝑎 , 𝑏 ⟩ ) = ⟨ ( 𝐹 ‘ 𝑎 ) , ( 𝐺 ‘ 𝑏 ) ⟩ )
33		1st2nd2	⊢ ( 𝑐 ∈ ( ( 𝐹 “ 𝑋 ) × ( 𝐺 “ 𝑌 ) ) → 𝑐 = ⟨ ( 1^st ‘ 𝑐 ) , ( 2^nd ‘ 𝑐 ) ⟩ )
34	33	ad5antlr	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( ( 𝐹 “ 𝑋 ) × ( 𝐺 “ 𝑌 ) ) ) ∧ 𝑎 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑎 ) = ( 1^st ‘ 𝑐 ) ) ∧ 𝑏 ∈ 𝑌 ) ∧ ( 𝐺 ‘ 𝑏 ) = ( 2^nd ‘ 𝑐 ) ) → 𝑐 = ⟨ ( 1^st ‘ 𝑐 ) , ( 2^nd ‘ 𝑐 ) ⟩ )
35	27 32 34	3eqtr4d	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( ( 𝐹 “ 𝑋 ) × ( 𝐺 “ 𝑌 ) ) ) ∧ 𝑎 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑎 ) = ( 1^st ‘ 𝑐 ) ) ∧ 𝑏 ∈ 𝑌 ) ∧ ( 𝐺 ‘ 𝑏 ) = ( 2^nd ‘ 𝑐 ) ) → ( 𝐻 ‘ ⟨ 𝑎 , 𝑏 ⟩ ) = 𝑐 )
36		fveqeq2	⊢ ( 𝑧 = ⟨ 𝑎 , 𝑏 ⟩ → ( ( 𝐻 ‘ 𝑧 ) = 𝑐 ↔ ( 𝐻 ‘ ⟨ 𝑎 , 𝑏 ⟩ ) = 𝑐 ) )
37	36	rspcev	⊢ ( ( ⟨ 𝑎 , 𝑏 ⟩ ∈ ( 𝑋 × 𝑌 ) ∧ ( 𝐻 ‘ ⟨ 𝑎 , 𝑏 ⟩ ) = 𝑐 ) → ∃ 𝑧 ∈ ( 𝑋 × 𝑌 ) ( 𝐻 ‘ 𝑧 ) = 𝑐 )
38	24 35 37	syl2anc	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( ( 𝐹 “ 𝑋 ) × ( 𝐺 “ 𝑌 ) ) ) ∧ 𝑎 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑎 ) = ( 1^st ‘ 𝑐 ) ) ∧ 𝑏 ∈ 𝑌 ) ∧ ( 𝐺 ‘ 𝑏 ) = ( 2^nd ‘ 𝑐 ) ) → ∃ 𝑧 ∈ ( 𝑋 × 𝑌 ) ( 𝐻 ‘ 𝑧 ) = 𝑐 )
39	3	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( ( 𝐹 “ 𝑋 ) × ( 𝐺 “ 𝑌 ) ) ) ∧ 𝑎 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑎 ) = ( 1^st ‘ 𝑐 ) ) → 𝐺 Fn 𝐵 )
40		fnfun	⊢ ( 𝐺 Fn 𝐵 → Fun 𝐺 )
41	39 40	syl	⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( ( 𝐹 “ 𝑋 ) × ( 𝐺 “ 𝑌 ) ) ) ∧ 𝑎 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑎 ) = ( 1^st ‘ 𝑐 ) ) → Fun 𝐺 )
42		xp2nd	⊢ ( 𝑐 ∈ ( ( 𝐹 “ 𝑋 ) × ( 𝐺 “ 𝑌 ) ) → ( 2^nd ‘ 𝑐 ) ∈ ( 𝐺 “ 𝑌 ) )
43	42	ad3antlr	⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( ( 𝐹 “ 𝑋 ) × ( 𝐺 “ 𝑌 ) ) ) ∧ 𝑎 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑎 ) = ( 1^st ‘ 𝑐 ) ) → ( 2^nd ‘ 𝑐 ) ∈ ( 𝐺 “ 𝑌 ) )
44		fvelima	⊢ ( ( Fun 𝐺 ∧ ( 2^nd ‘ 𝑐 ) ∈ ( 𝐺 “ 𝑌 ) ) → ∃ 𝑏 ∈ 𝑌 ( 𝐺 ‘ 𝑏 ) = ( 2^nd ‘ 𝑐 ) )
45	41 43 44	syl2anc	⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( ( 𝐹 “ 𝑋 ) × ( 𝐺 “ 𝑌 ) ) ) ∧ 𝑎 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑎 ) = ( 1^st ‘ 𝑐 ) ) → ∃ 𝑏 ∈ 𝑌 ( 𝐺 ‘ 𝑏 ) = ( 2^nd ‘ 𝑐 ) )
46	38 45	r19.29a	⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( ( 𝐹 “ 𝑋 ) × ( 𝐺 “ 𝑌 ) ) ) ∧ 𝑎 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑎 ) = ( 1^st ‘ 𝑐 ) ) → ∃ 𝑧 ∈ ( 𝑋 × 𝑌 ) ( 𝐻 ‘ 𝑧 ) = 𝑐 )
47	2	adantr	⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( ( 𝐹 “ 𝑋 ) × ( 𝐺 “ 𝑌 ) ) ) → 𝐹 Fn 𝐴 )
48		fnfun	⊢ ( 𝐹 Fn 𝐴 → Fun 𝐹 )
49	47 48	syl	⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( ( 𝐹 “ 𝑋 ) × ( 𝐺 “ 𝑌 ) ) ) → Fun 𝐹 )
50		xp1st	⊢ ( 𝑐 ∈ ( ( 𝐹 “ 𝑋 ) × ( 𝐺 “ 𝑌 ) ) → ( 1^st ‘ 𝑐 ) ∈ ( 𝐹 “ 𝑋 ) )
51	50	adantl	⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( ( 𝐹 “ 𝑋 ) × ( 𝐺 “ 𝑌 ) ) ) → ( 1^st ‘ 𝑐 ) ∈ ( 𝐹 “ 𝑋 ) )
52		fvelima	⊢ ( ( Fun 𝐹 ∧ ( 1^st ‘ 𝑐 ) ∈ ( 𝐹 “ 𝑋 ) ) → ∃ 𝑎 ∈ 𝑋 ( 𝐹 ‘ 𝑎 ) = ( 1^st ‘ 𝑐 ) )
53	49 51 52	syl2anc	⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( ( 𝐹 “ 𝑋 ) × ( 𝐺 “ 𝑌 ) ) ) → ∃ 𝑎 ∈ 𝑋 ( 𝐹 ‘ 𝑎 ) = ( 1^st ‘ 𝑐 ) )
54	46 53	r19.29a	⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( ( 𝐹 “ 𝑋 ) × ( 𝐺 “ 𝑌 ) ) ) → ∃ 𝑧 ∈ ( 𝑋 × 𝑌 ) ( 𝐻 ‘ 𝑧 ) = 𝑐 )
55		simpr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝐻 ‘ 𝑧 ) = 𝑐 ) → ( 𝐻 ‘ 𝑧 ) = 𝑐 )
56	18	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝐻 ‘ 𝑧 ) = 𝑐 ) → ( 𝑋 × 𝑌 ) ⊆ ( 𝐴 × 𝐵 ) )
57		simplr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝐻 ‘ 𝑧 ) = 𝑐 ) → 𝑧 ∈ ( 𝑋 × 𝑌 ) )
58	56 57	sseldd	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝐻 ‘ 𝑧 ) = 𝑐 ) → 𝑧 ∈ ( 𝐴 × 𝐵 ) )
59	15	fvmpt2	⊢ ( ( 𝑧 ∈ ( 𝐴 × 𝐵 ) ∧ ⟨ ( 𝐹 ‘ ( 1^st ‘ 𝑧 ) ) , ( 𝐺 ‘ ( 2^nd ‘ 𝑧 ) ) ⟩ ∈ V ) → ( 𝐻 ‘ 𝑧 ) = ⟨ ( 𝐹 ‘ ( 1^st ‘ 𝑧 ) ) , ( 𝐺 ‘ ( 2^nd ‘ 𝑧 ) ) ⟩ )
60	58 6 59	sylancl	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝐻 ‘ 𝑧 ) = 𝑐 ) → ( 𝐻 ‘ 𝑧 ) = ⟨ ( 𝐹 ‘ ( 1^st ‘ 𝑧 ) ) , ( 𝐺 ‘ ( 2^nd ‘ 𝑧 ) ) ⟩ )
61	2	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝐻 ‘ 𝑧 ) = 𝑐 ) → 𝐹 Fn 𝐴 )
62	4	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝐻 ‘ 𝑧 ) = 𝑐 ) → 𝑋 ⊆ 𝐴 )
63		xp1st	⊢ ( 𝑧 ∈ ( 𝑋 × 𝑌 ) → ( 1^st ‘ 𝑧 ) ∈ 𝑋 )
64	57 63	syl	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝐻 ‘ 𝑧 ) = 𝑐 ) → ( 1^st ‘ 𝑧 ) ∈ 𝑋 )
65		fnfvima	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ⊆ 𝐴 ∧ ( 1^st ‘ 𝑧 ) ∈ 𝑋 ) → ( 𝐹 ‘ ( 1^st ‘ 𝑧 ) ) ∈ ( 𝐹 “ 𝑋 ) )
66	61 62 64 65	syl3anc	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝐻 ‘ 𝑧 ) = 𝑐 ) → ( 𝐹 ‘ ( 1^st ‘ 𝑧 ) ) ∈ ( 𝐹 “ 𝑋 ) )
67	3	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝐻 ‘ 𝑧 ) = 𝑐 ) → 𝐺 Fn 𝐵 )
68	5	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝐻 ‘ 𝑧 ) = 𝑐 ) → 𝑌 ⊆ 𝐵 )
69		xp2nd	⊢ ( 𝑧 ∈ ( 𝑋 × 𝑌 ) → ( 2^nd ‘ 𝑧 ) ∈ 𝑌 )
70	57 69	syl	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝐻 ‘ 𝑧 ) = 𝑐 ) → ( 2^nd ‘ 𝑧 ) ∈ 𝑌 )
71		fnfvima	⊢ ( ( 𝐺 Fn 𝐵 ∧ 𝑌 ⊆ 𝐵 ∧ ( 2^nd ‘ 𝑧 ) ∈ 𝑌 ) → ( 𝐺 ‘ ( 2^nd ‘ 𝑧 ) ) ∈ ( 𝐺 “ 𝑌 ) )
72	67 68 70 71	syl3anc	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝐻 ‘ 𝑧 ) = 𝑐 ) → ( 𝐺 ‘ ( 2^nd ‘ 𝑧 ) ) ∈ ( 𝐺 “ 𝑌 ) )
73		opelxpi	⊢ ( ( ( 𝐹 ‘ ( 1^st ‘ 𝑧 ) ) ∈ ( 𝐹 “ 𝑋 ) ∧ ( 𝐺 ‘ ( 2^nd ‘ 𝑧 ) ) ∈ ( 𝐺 “ 𝑌 ) ) → ⟨ ( 𝐹 ‘ ( 1^st ‘ 𝑧 ) ) , ( 𝐺 ‘ ( 2^nd ‘ 𝑧 ) ) ⟩ ∈ ( ( 𝐹 “ 𝑋 ) × ( 𝐺 “ 𝑌 ) ) )
74	66 72 73	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝐻 ‘ 𝑧 ) = 𝑐 ) → ⟨ ( 𝐹 ‘ ( 1^st ‘ 𝑧 ) ) , ( 𝐺 ‘ ( 2^nd ‘ 𝑧 ) ) ⟩ ∈ ( ( 𝐹 “ 𝑋 ) × ( 𝐺 “ 𝑌 ) ) )
75	60 74	eqeltrd	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝐻 ‘ 𝑧 ) = 𝑐 ) → ( 𝐻 ‘ 𝑧 ) ∈ ( ( 𝐹 “ 𝑋 ) × ( 𝐺 “ 𝑌 ) ) )
76	55 75	eqeltrrd	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝐻 ‘ 𝑧 ) = 𝑐 ) → 𝑐 ∈ ( ( 𝐹 “ 𝑋 ) × ( 𝐺 “ 𝑌 ) ) )
77	76	r19.29an	⊢ ( ( 𝜑 ∧ ∃ 𝑧 ∈ ( 𝑋 × 𝑌 ) ( 𝐻 ‘ 𝑧 ) = 𝑐 ) → 𝑐 ∈ ( ( 𝐹 “ 𝑋 ) × ( 𝐺 “ 𝑌 ) ) )
78	54 77	impbida	⊢ ( 𝜑 → ( 𝑐 ∈ ( ( 𝐹 “ 𝑋 ) × ( 𝐺 “ 𝑌 ) ) ↔ ∃ 𝑧 ∈ ( 𝑋 × 𝑌 ) ( 𝐻 ‘ 𝑧 ) = 𝑐 ) )
79	20 78	bitr4d	⊢ ( 𝜑 → ( 𝑐 ∈ ( 𝐻 “ ( 𝑋 × 𝑌 ) ) ↔ 𝑐 ∈ ( ( 𝐹 “ 𝑋 ) × ( 𝐺 “ 𝑌 ) ) ) )
80	79	eqrdv	⊢ ( 𝜑 → ( 𝐻 “ ( 𝑋 × 𝑌 ) ) = ( ( 𝐹 “ 𝑋 ) × ( 𝐺 “ 𝑌 ) ) )

Metamath Proof Explorer

Theorem fimaproj

Proof