Theorem fimaproj 8161

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

Hypotheses

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

Assertion

Ref	Expression
fimaproj	⊢ (𝜑 → (𝐻 “ (𝑋 × 𝑌)) = ((𝐹 “ 𝑋) × (𝐺 “ 𝑌)))

Distinct variable groups:   𝑥,𝐴,𝑦   𝑥,𝐵,𝑦   𝑥,𝐹,𝑦   𝑥,𝐺,𝑦   𝑥,𝐻,𝑦

Allowed substitution hints:   𝜑(𝑥,𝑦)   𝑋(𝑥,𝑦)   𝑌(𝑥,𝑦)

Proof of Theorem fimaproj

Dummy variables 𝑎 𝑏 𝑧 𝑐 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		opex 5468	. . . . 5 ⊢ ⟨(𝐹‘(1st ‘𝑧)), (𝐺‘(2nd ‘𝑧))⟩ ∈ V
2		fvproj.h	. . . . . 6 ⊢ 𝐻 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ ⟨(𝐹‘𝑥), (𝐺‘𝑦)⟩)
3		vex 3483	. . . . . . . . . 10 ⊢ 𝑥 ∈ V
4		vex 3483	. . . . . . . . . 10 ⊢ 𝑦 ∈ V
5	3, 4	op1std 8025	. . . . . . . . 9 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → (1st ‘𝑧) = 𝑥)
6	5	fveq2d 6909	. . . . . . . 8 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → (𝐹‘(1st ‘𝑧)) = (𝐹‘𝑥))
7	3, 4	op2ndd 8026	. . . . . . . . 9 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → (2nd ‘𝑧) = 𝑦)
8	7	fveq2d 6909	. . . . . . . 8 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → (𝐺‘(2nd ‘𝑧)) = (𝐺‘𝑦))
9	6, 8	opeq12d 4880	. . . . . . 7 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → ⟨(𝐹‘(1st ‘𝑧)), (𝐺‘(2nd ‘𝑧))⟩ = ⟨(𝐹‘𝑥), (𝐺‘𝑦)⟩)
10	9	mpompt 7548	. . . . . 6 ⊢ (𝑧 ∈ (𝐴 × 𝐵) ↦ ⟨(𝐹‘(1st ‘𝑧)), (𝐺‘(2nd ‘𝑧))⟩) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ ⟨(𝐹‘𝑥), (𝐺‘𝑦)⟩)
11	2, 10	eqtr4i 2767	. . . . 5 ⊢ 𝐻 = (𝑧 ∈ (𝐴 × 𝐵) ↦ ⟨(𝐹‘(1st ‘𝑧)), (𝐺‘(2nd ‘𝑧))⟩)
12	1, 11	fnmpti 6710	. . . 4 ⊢ 𝐻 Fn (𝐴 × 𝐵)
13		fimaproj.x	. . . . 5 ⊢ (𝜑 → 𝑋 ⊆ 𝐴)
14		fimaproj.y	. . . . 5 ⊢ (𝜑 → 𝑌 ⊆ 𝐵)
15		xpss12 5699	. . . . 5 ⊢ ((𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐵) → (𝑋 × 𝑌) ⊆ (𝐴 × 𝐵))
16	13, 14, 15	syl2anc 584	. . . 4 ⊢ (𝜑 → (𝑋 × 𝑌) ⊆ (𝐴 × 𝐵))
17		fvelimab 6980	. . . 4 ⊢ ((𝐻 Fn (𝐴 × 𝐵) ∧ (𝑋 × 𝑌) ⊆ (𝐴 × 𝐵)) → (𝑐 ∈ (𝐻 “ (𝑋 × 𝑌)) ↔ ∃𝑧 ∈ (𝑋 × 𝑌)(𝐻‘𝑧) = 𝑐))
18	12, 16, 17	sylancr 587	. . 3 ⊢ (𝜑 → (𝑐 ∈ (𝐻 “ (𝑋 × 𝑌)) ↔ ∃𝑧 ∈ (𝑋 × 𝑌)(𝐻‘𝑧) = 𝑐))
19		simp-4r 783	. . . . . . . 8 ⊢ ((((((𝜑 ∧ 𝑐 ∈ ((𝐹 “ 𝑋) × (𝐺 “ 𝑌))) ∧ 𝑎 ∈ 𝑋) ∧ (𝐹‘𝑎) = (1st ‘𝑐)) ∧ 𝑏 ∈ 𝑌) ∧ (𝐺‘𝑏) = (2nd ‘𝑐)) → 𝑎 ∈ 𝑋)
20		simplr 768	. . . . . . . 8 ⊢ ((((((𝜑 ∧ 𝑐 ∈ ((𝐹 “ 𝑋) × (𝐺 “ 𝑌))) ∧ 𝑎 ∈ 𝑋) ∧ (𝐹‘𝑎) = (1st ‘𝑐)) ∧ 𝑏 ∈ 𝑌) ∧ (𝐺‘𝑏) = (2nd ‘𝑐)) → 𝑏 ∈ 𝑌)
21		opelxpi 5721	. . . . . . . 8 ⊢ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌) → ⟨𝑎, 𝑏⟩ ∈ (𝑋 × 𝑌))
22	19, 20, 21	syl2anc 584	. . . . . . 7 ⊢ ((((((𝜑 ∧ 𝑐 ∈ ((𝐹 “ 𝑋) × (𝐺 “ 𝑌))) ∧ 𝑎 ∈ 𝑋) ∧ (𝐹‘𝑎) = (1st ‘𝑐)) ∧ 𝑏 ∈ 𝑌) ∧ (𝐺‘𝑏) = (2nd ‘𝑐)) → ⟨𝑎, 𝑏⟩ ∈ (𝑋 × 𝑌))
23		simpllr 775	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑐 ∈ ((𝐹 “ 𝑋) × (𝐺 “ 𝑌))) ∧ 𝑎 ∈ 𝑋) ∧ (𝐹‘𝑎) = (1st ‘𝑐)) ∧ 𝑏 ∈ 𝑌) ∧ (𝐺‘𝑏) = (2nd ‘𝑐)) → (𝐹‘𝑎) = (1st ‘𝑐))
24		simpr 484	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑐 ∈ ((𝐹 “ 𝑋) × (𝐺 “ 𝑌))) ∧ 𝑎 ∈ 𝑋) ∧ (𝐹‘𝑎) = (1st ‘𝑐)) ∧ 𝑏 ∈ 𝑌) ∧ (𝐺‘𝑏) = (2nd ‘𝑐)) → (𝐺‘𝑏) = (2nd ‘𝑐))
25	23, 24	opeq12d 4880	. . . . . . . 8 ⊢ ((((((𝜑 ∧ 𝑐 ∈ ((𝐹 “ 𝑋) × (𝐺 “ 𝑌))) ∧ 𝑎 ∈ 𝑋) ∧ (𝐹‘𝑎) = (1st ‘𝑐)) ∧ 𝑏 ∈ 𝑌) ∧ (𝐺‘𝑏) = (2nd ‘𝑐)) → ⟨(𝐹‘𝑎), (𝐺‘𝑏)⟩ = ⟨(1st ‘𝑐), (2nd ‘𝑐)⟩)
26	13	ad5antr 734	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑐 ∈ ((𝐹 “ 𝑋) × (𝐺 “ 𝑌))) ∧ 𝑎 ∈ 𝑋) ∧ (𝐹‘𝑎) = (1st ‘𝑐)) ∧ 𝑏 ∈ 𝑌) ∧ (𝐺‘𝑏) = (2nd ‘𝑐)) → 𝑋 ⊆ 𝐴)
27	26, 19	sseldd 3983	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑐 ∈ ((𝐹 “ 𝑋) × (𝐺 “ 𝑌))) ∧ 𝑎 ∈ 𝑋) ∧ (𝐹‘𝑎) = (1st ‘𝑐)) ∧ 𝑏 ∈ 𝑌) ∧ (𝐺‘𝑏) = (2nd ‘𝑐)) → 𝑎 ∈ 𝐴)
28	14	ad5antr 734	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑐 ∈ ((𝐹 “ 𝑋) × (𝐺 “ 𝑌))) ∧ 𝑎 ∈ 𝑋) ∧ (𝐹‘𝑎) = (1st ‘𝑐)) ∧ 𝑏 ∈ 𝑌) ∧ (𝐺‘𝑏) = (2nd ‘𝑐)) → 𝑌 ⊆ 𝐵)
29	28, 20	sseldd 3983	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑐 ∈ ((𝐹 “ 𝑋) × (𝐺 “ 𝑌))) ∧ 𝑎 ∈ 𝑋) ∧ (𝐹‘𝑎) = (1st ‘𝑐)) ∧ 𝑏 ∈ 𝑌) ∧ (𝐺‘𝑏) = (2nd ‘𝑐)) → 𝑏 ∈ 𝐵)
30	2, 27, 29	fvproj 8160	. . . . . . . 8 ⊢ ((((((𝜑 ∧ 𝑐 ∈ ((𝐹 “ 𝑋) × (𝐺 “ 𝑌))) ∧ 𝑎 ∈ 𝑋) ∧ (𝐹‘𝑎) = (1st ‘𝑐)) ∧ 𝑏 ∈ 𝑌) ∧ (𝐺‘𝑏) = (2nd ‘𝑐)) → (𝐻‘⟨𝑎, 𝑏⟩) = ⟨(𝐹‘𝑎), (𝐺‘𝑏)⟩)
31		1st2nd2 8054	. . . . . . . . 9 ⊢ (𝑐 ∈ ((𝐹 “ 𝑋) × (𝐺 “ 𝑌)) → 𝑐 = ⟨(1st ‘𝑐), (2nd ‘𝑐)⟩)
32	31	ad5antlr 735	. . . . . . . 8 ⊢ ((((((𝜑 ∧ 𝑐 ∈ ((𝐹 “ 𝑋) × (𝐺 “ 𝑌))) ∧ 𝑎 ∈ 𝑋) ∧ (𝐹‘𝑎) = (1st ‘𝑐)) ∧ 𝑏 ∈ 𝑌) ∧ (𝐺‘𝑏) = (2nd ‘𝑐)) → 𝑐 = ⟨(1st ‘𝑐), (2nd ‘𝑐)⟩)
33	25, 30, 32	3eqtr4d 2786	. . . . . . 7 ⊢ ((((((𝜑 ∧ 𝑐 ∈ ((𝐹 “ 𝑋) × (𝐺 “ 𝑌))) ∧ 𝑎 ∈ 𝑋) ∧ (𝐹‘𝑎) = (1st ‘𝑐)) ∧ 𝑏 ∈ 𝑌) ∧ (𝐺‘𝑏) = (2nd ‘𝑐)) → (𝐻‘⟨𝑎, 𝑏⟩) = 𝑐)
34		fveqeq2 6914	. . . . . . . 8 ⊢ (𝑧 = ⟨𝑎, 𝑏⟩ → ((𝐻‘𝑧) = 𝑐 ↔ (𝐻‘⟨𝑎, 𝑏⟩) = 𝑐))
35	34	rspcev 3621	. . . . . . 7 ⊢ ((⟨𝑎, 𝑏⟩ ∈ (𝑋 × 𝑌) ∧ (𝐻‘⟨𝑎, 𝑏⟩) = 𝑐) → ∃𝑧 ∈ (𝑋 × 𝑌)(𝐻‘𝑧) = 𝑐)
36	22, 33, 35	syl2anc 584	. . . . . 6 ⊢ ((((((𝜑 ∧ 𝑐 ∈ ((𝐹 “ 𝑋) × (𝐺 “ 𝑌))) ∧ 𝑎 ∈ 𝑋) ∧ (𝐹‘𝑎) = (1st ‘𝑐)) ∧ 𝑏 ∈ 𝑌) ∧ (𝐺‘𝑏) = (2nd ‘𝑐)) → ∃𝑧 ∈ (𝑋 × 𝑌)(𝐻‘𝑧) = 𝑐)
37		fimaproj.g	. . . . . . . . 9 ⊢ (𝜑 → 𝐺 Fn 𝐵)
38	37	ad3antrrr 730	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑐 ∈ ((𝐹 “ 𝑋) × (𝐺 “ 𝑌))) ∧ 𝑎 ∈ 𝑋) ∧ (𝐹‘𝑎) = (1st ‘𝑐)) → 𝐺 Fn 𝐵)
39		fnfun 6667	. . . . . . . 8 ⊢ (𝐺 Fn 𝐵 → Fun 𝐺)
40	38, 39	syl 17	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑐 ∈ ((𝐹 “ 𝑋) × (𝐺 “ 𝑌))) ∧ 𝑎 ∈ 𝑋) ∧ (𝐹‘𝑎) = (1st ‘𝑐)) → Fun 𝐺)
41		xp2nd 8048	. . . . . . . 8 ⊢ (𝑐 ∈ ((𝐹 “ 𝑋) × (𝐺 “ 𝑌)) → (2nd ‘𝑐) ∈ (𝐺 “ 𝑌))
42	41	ad3antlr 731	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑐 ∈ ((𝐹 “ 𝑋) × (𝐺 “ 𝑌))) ∧ 𝑎 ∈ 𝑋) ∧ (𝐹‘𝑎) = (1st ‘𝑐)) → (2nd ‘𝑐) ∈ (𝐺 “ 𝑌))
43		fvelima 6973	. . . . . . 7 ⊢ ((Fun 𝐺 ∧ (2nd ‘𝑐) ∈ (𝐺 “ 𝑌)) → ∃𝑏 ∈ 𝑌 (𝐺‘𝑏) = (2nd ‘𝑐))
44	40, 42, 43	syl2anc 584	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑐 ∈ ((𝐹 “ 𝑋) × (𝐺 “ 𝑌))) ∧ 𝑎 ∈ 𝑋) ∧ (𝐹‘𝑎) = (1st ‘𝑐)) → ∃𝑏 ∈ 𝑌 (𝐺‘𝑏) = (2nd ‘𝑐))
45	36, 44	r19.29a 3161	. . . . 5 ⊢ ((((𝜑 ∧ 𝑐 ∈ ((𝐹 “ 𝑋) × (𝐺 “ 𝑌))) ∧ 𝑎 ∈ 𝑋) ∧ (𝐹‘𝑎) = (1st ‘𝑐)) → ∃𝑧 ∈ (𝑋 × 𝑌)(𝐻‘𝑧) = 𝑐)
46		fimaproj.f	. . . . . . . 8 ⊢ (𝜑 → 𝐹 Fn 𝐴)
47	46	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐹 “ 𝑋) × (𝐺 “ 𝑌))) → 𝐹 Fn 𝐴)
48		fnfun 6667	. . . . . . 7 ⊢ (𝐹 Fn 𝐴 → Fun 𝐹)
49	47, 48	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐹 “ 𝑋) × (𝐺 “ 𝑌))) → Fun 𝐹)
50		xp1st 8047	. . . . . . 7 ⊢ (𝑐 ∈ ((𝐹 “ 𝑋) × (𝐺 “ 𝑌)) → (1st ‘𝑐) ∈ (𝐹 “ 𝑋))
51	50	adantl 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐹 “ 𝑋) × (𝐺 “ 𝑌))) → (1st ‘𝑐) ∈ (𝐹 “ 𝑋))
52		fvelima 6973	. . . . . 6 ⊢ ((Fun 𝐹 ∧ (1st ‘𝑐) ∈ (𝐹 “ 𝑋)) → ∃𝑎 ∈ 𝑋 (𝐹‘𝑎) = (1st ‘𝑐))
53	49, 51, 52	syl2anc 584	. . . . 5 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐹 “ 𝑋) × (𝐺 “ 𝑌))) → ∃𝑎 ∈ 𝑋 (𝐹‘𝑎) = (1st ‘𝑐))
54	45, 53	r19.29a 3161	. . . 4 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐹 “ 𝑋) × (𝐺 “ 𝑌))) → ∃𝑧 ∈ (𝑋 × 𝑌)(𝐻‘𝑧) = 𝑐)
55		simpr 484	. . . . . 6 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝑋 × 𝑌)) ∧ (𝐻‘𝑧) = 𝑐) → (𝐻‘𝑧) = 𝑐)
56	16	ad2antrr 726	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝑋 × 𝑌)) ∧ (𝐻‘𝑧) = 𝑐) → (𝑋 × 𝑌) ⊆ (𝐴 × 𝐵))
57		simplr 768	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝑋 × 𝑌)) ∧ (𝐻‘𝑧) = 𝑐) → 𝑧 ∈ (𝑋 × 𝑌))
58	56, 57	sseldd 3983	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝑋 × 𝑌)) ∧ (𝐻‘𝑧) = 𝑐) → 𝑧 ∈ (𝐴 × 𝐵))
59	11	fvmpt2 7026	. . . . . . . 8 ⊢ ((𝑧 ∈ (𝐴 × 𝐵) ∧ ⟨(𝐹‘(1st ‘𝑧)), (𝐺‘(2nd ‘𝑧))⟩ ∈ V) → (𝐻‘𝑧) = ⟨(𝐹‘(1st ‘𝑧)), (𝐺‘(2nd ‘𝑧))⟩)
60	58, 1, 59	sylancl 586	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝑋 × 𝑌)) ∧ (𝐻‘𝑧) = 𝑐) → (𝐻‘𝑧) = ⟨(𝐹‘(1st ‘𝑧)), (𝐺‘(2nd ‘𝑧))⟩)
61	46	ad2antrr 726	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝑋 × 𝑌)) ∧ (𝐻‘𝑧) = 𝑐) → 𝐹 Fn 𝐴)
62	13	ad2antrr 726	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝑋 × 𝑌)) ∧ (𝐻‘𝑧) = 𝑐) → 𝑋 ⊆ 𝐴)
63		xp1st 8047	. . . . . . . . . 10 ⊢ (𝑧 ∈ (𝑋 × 𝑌) → (1st ‘𝑧) ∈ 𝑋)
64	57, 63	syl 17	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝑋 × 𝑌)) ∧ (𝐻‘𝑧) = 𝑐) → (1st ‘𝑧) ∈ 𝑋)
65		fnfvima 7254	. . . . . . . . 9 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑋 ⊆ 𝐴 ∧ (1st ‘𝑧) ∈ 𝑋) → (𝐹‘(1st ‘𝑧)) ∈ (𝐹 “ 𝑋))
66	61, 62, 64, 65	syl3anc 1372	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝑋 × 𝑌)) ∧ (𝐻‘𝑧) = 𝑐) → (𝐹‘(1st ‘𝑧)) ∈ (𝐹 “ 𝑋))
67	37	ad2antrr 726	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝑋 × 𝑌)) ∧ (𝐻‘𝑧) = 𝑐) → 𝐺 Fn 𝐵)
68	14	ad2antrr 726	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝑋 × 𝑌)) ∧ (𝐻‘𝑧) = 𝑐) → 𝑌 ⊆ 𝐵)
69		xp2nd 8048	. . . . . . . . . 10 ⊢ (𝑧 ∈ (𝑋 × 𝑌) → (2nd ‘𝑧) ∈ 𝑌)
70	57, 69	syl 17	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝑋 × 𝑌)) ∧ (𝐻‘𝑧) = 𝑐) → (2nd ‘𝑧) ∈ 𝑌)
71		fnfvima 7254	. . . . . . . . 9 ⊢ ((𝐺 Fn 𝐵 ∧ 𝑌 ⊆ 𝐵 ∧ (2nd ‘𝑧) ∈ 𝑌) → (𝐺‘(2nd ‘𝑧)) ∈ (𝐺 “ 𝑌))
72	67, 68, 70, 71	syl3anc 1372	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝑋 × 𝑌)) ∧ (𝐻‘𝑧) = 𝑐) → (𝐺‘(2nd ‘𝑧)) ∈ (𝐺 “ 𝑌))
73		opelxpi 5721	. . . . . . . 8 ⊢ (((𝐹‘(1st ‘𝑧)) ∈ (𝐹 “ 𝑋) ∧ (𝐺‘(2nd ‘𝑧)) ∈ (𝐺 “ 𝑌)) → ⟨(𝐹‘(1st ‘𝑧)), (𝐺‘(2nd ‘𝑧))⟩ ∈ ((𝐹 “ 𝑋) × (𝐺 “ 𝑌)))
74	66, 72, 73	syl2anc 584	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝑋 × 𝑌)) ∧ (𝐻‘𝑧) = 𝑐) → ⟨(𝐹‘(1st ‘𝑧)), (𝐺‘(2nd ‘𝑧))⟩ ∈ ((𝐹 “ 𝑋) × (𝐺 “ 𝑌)))
75	60, 74	eqeltrd 2840	. . . . . 6 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝑋 × 𝑌)) ∧ (𝐻‘𝑧) = 𝑐) → (𝐻‘𝑧) ∈ ((𝐹 “ 𝑋) × (𝐺 “ 𝑌)))
76	55, 75	eqeltrrd 2841	. . . . 5 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝑋 × 𝑌)) ∧ (𝐻‘𝑧) = 𝑐) → 𝑐 ∈ ((𝐹 “ 𝑋) × (𝐺 “ 𝑌)))
77	76	r19.29an 3157	. . . 4 ⊢ ((𝜑 ∧ ∃𝑧 ∈ (𝑋 × 𝑌)(𝐻‘𝑧) = 𝑐) → 𝑐 ∈ ((𝐹 “ 𝑋) × (𝐺 “ 𝑌)))
78	54, 77	impbida 800	. . 3 ⊢ (𝜑 → (𝑐 ∈ ((𝐹 “ 𝑋) × (𝐺 “ 𝑌)) ↔ ∃𝑧 ∈ (𝑋 × 𝑌)(𝐻‘𝑧) = 𝑐))
79	18, 78	bitr4d 282	. 2 ⊢ (𝜑 → (𝑐 ∈ (𝐻 “ (𝑋 × 𝑌)) ↔ 𝑐 ∈ ((𝐹 “ 𝑋) × (𝐺 “ 𝑌))))
80	79	eqrdv 2734	1 ⊢ (𝜑 → (𝐻 “ (𝑋 × 𝑌)) = ((𝐹 “ 𝑋) × (𝐺 “ 𝑌)))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1539   ∈ wcel 2107  ∃wrex 3069  Vcvv 3479   ⊆ wss 3950  ⟨cop 4631   ↦ cmpt 5224   × cxp 5682   “ cima 5687  Fun wfun 6554   Fn wfn 6555  ‘cfv 6560   ∈ cmpo 7434  1^st c1st 8013  2^nd c2nd 8014

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2707  ax-sep 5295  ax-nul 5305  ax-pr 5431  ax-un 7756

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2728  df-clel 2815  df-nfc 2891  df-ne 2940  df-ral 3061  df-rex 3070  df-rab 3436  df-v 3481  df-sbc 3788  df-csb 3899  df-dif 3953  df-un 3955  df-in 3957  df-ss 3967  df-nul 4333  df-if 4525  df-sn 4626  df-pr 4628  df-op 4632  df-uni 4907  df-iun 4992  df-br 5143  df-opab 5205  df-mpt 5225  df-id 5577  df-xp 5690  df-rel 5691  df-cnv 5692  df-co 5693  df-dm 5694  df-rn 5695  df-res 5696  df-ima 5697  df-iota 6513  df-fun 6562  df-fn 6563  df-fv 6568  df-ov 7435  df-oprab 7436  df-mpo 7437  df-1st 8015  df-2nd 8016

This theorem is referenced by:  txomap  33834