Theorem fimaproj 29228

Description: Image of a cartesian product for a function on pairs, given two projections 𝐹 and 𝐺. (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 4859	. . . . 5 ⊢ ⟨(𝐹‘(1st ‘𝑧)), (𝐺‘(2nd ‘𝑧))⟩ ∈ V
2		fvproj.h	. . . . . 6 ⊢ 𝐻 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ ⟨(𝐹‘𝑥), (𝐺‘𝑦)⟩)
3		vex 3176	. . . . . . . . . 10 ⊢ 𝑥 ∈ V
4		vex 3176	. . . . . . . . . 10 ⊢ 𝑦 ∈ V
5	3, 4	op1std 7069	. . . . . . . . 9 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → (1st ‘𝑧) = 𝑥)
6	5	fveq2d 6107	. . . . . . . 8 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → (𝐹‘(1st ‘𝑧)) = (𝐹‘𝑥))
7	3, 4	op2ndd 7070	. . . . . . . . 9 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → (2nd ‘𝑧) = 𝑦)
8	7	fveq2d 6107	. . . . . . . 8 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → (𝐺‘(2nd ‘𝑧)) = (𝐺‘𝑦))
9	6, 8	opeq12d 4348	. . . . . . 7 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → ⟨(𝐹‘(1st ‘𝑧)), (𝐺‘(2nd ‘𝑧))⟩ = ⟨(𝐹‘𝑥), (𝐺‘𝑦)⟩)
10	9	mpt2mpt 6650	. . . . . 6 ⊢ (𝑧 ∈ (𝐴 × 𝐵) ↦ ⟨(𝐹‘(1st ‘𝑧)), (𝐺‘(2nd ‘𝑧))⟩) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ ⟨(𝐹‘𝑥), (𝐺‘𝑦)⟩)
11	2, 10	eqtr4i 2635	. . . . 5 ⊢ 𝐻 = (𝑧 ∈ (𝐴 × 𝐵) ↦ ⟨(𝐹‘(1st ‘𝑧)), (𝐺‘(2nd ‘𝑧))⟩)
12	1, 11	fnmpti 5935	. . . 4 ⊢ 𝐻 Fn (𝐴 × 𝐵)
13		fimaproj.x	. . . . 5 ⊢ (𝜑 → 𝑋 ⊆ 𝐴)
14		fimaproj.y	. . . . 5 ⊢ (𝜑 → 𝑌 ⊆ 𝐵)
15		xpss12 5148	. . . . 5 ⊢ ((𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐵) → (𝑋 × 𝑌) ⊆ (𝐴 × 𝐵))
16	13, 14, 15	syl2anc 691	. . . 4 ⊢ (𝜑 → (𝑋 × 𝑌) ⊆ (𝐴 × 𝐵))
17		fvelimab 6163	. . . 4 ⊢ ((𝐻 Fn (𝐴 × 𝐵) ∧ (𝑋 × 𝑌) ⊆ (𝐴 × 𝐵)) → (𝑐 ∈ (𝐻 “ (𝑋 × 𝑌)) ↔ ∃𝑧 ∈ (𝑋 × 𝑌)(𝐻‘𝑧) = 𝑐))
18	12, 16, 17	sylancr 694	. . 3 ⊢ (𝜑 → (𝑐 ∈ (𝐻 “ (𝑋 × 𝑌)) ↔ ∃𝑧 ∈ (𝑋 × 𝑌)(𝐻‘𝑧) = 𝑐))
19		simp-4r 803	. . . . . . . 8 ⊢ ((((((𝜑 ∧ 𝑐 ∈ ((𝐹 “ 𝑋) × (𝐺 “ 𝑌))) ∧ 𝑎 ∈ 𝑋) ∧ (𝐹‘𝑎) = (1st ‘𝑐)) ∧ 𝑏 ∈ 𝑌) ∧ (𝐺‘𝑏) = (2nd ‘𝑐)) → 𝑎 ∈ 𝑋)
20		simplr 788	. . . . . . . 8 ⊢ ((((((𝜑 ∧ 𝑐 ∈ ((𝐹 “ 𝑋) × (𝐺 “ 𝑌))) ∧ 𝑎 ∈ 𝑋) ∧ (𝐹‘𝑎) = (1st ‘𝑐)) ∧ 𝑏 ∈ 𝑌) ∧ (𝐺‘𝑏) = (2nd ‘𝑐)) → 𝑏 ∈ 𝑌)
21		opelxpi 5072	. . . . . . . 8 ⊢ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌) → ⟨𝑎, 𝑏⟩ ∈ (𝑋 × 𝑌))
22	19, 20, 21	syl2anc 691	. . . . . . 7 ⊢ ((((((𝜑 ∧ 𝑐 ∈ ((𝐹 “ 𝑋) × (𝐺 “ 𝑌))) ∧ 𝑎 ∈ 𝑋) ∧ (𝐹‘𝑎) = (1st ‘𝑐)) ∧ 𝑏 ∈ 𝑌) ∧ (𝐺‘𝑏) = (2nd ‘𝑐)) → ⟨𝑎, 𝑏⟩ ∈ (𝑋 × 𝑌))
23		simpllr 795	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑐 ∈ ((𝐹 “ 𝑋) × (𝐺 “ 𝑌))) ∧ 𝑎 ∈ 𝑋) ∧ (𝐹‘𝑎) = (1st ‘𝑐)) ∧ 𝑏 ∈ 𝑌) ∧ (𝐺‘𝑏) = (2nd ‘𝑐)) → (𝐹‘𝑎) = (1st ‘𝑐))
24		simpr 476	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑐 ∈ ((𝐹 “ 𝑋) × (𝐺 “ 𝑌))) ∧ 𝑎 ∈ 𝑋) ∧ (𝐹‘𝑎) = (1st ‘𝑐)) ∧ 𝑏 ∈ 𝑌) ∧ (𝐺‘𝑏) = (2nd ‘𝑐)) → (𝐺‘𝑏) = (2nd ‘𝑐))
25	23, 24	opeq12d 4348	. . . . . . . 8 ⊢ ((((((𝜑 ∧ 𝑐 ∈ ((𝐹 “ 𝑋) × (𝐺 “ 𝑌))) ∧ 𝑎 ∈ 𝑋) ∧ (𝐹‘𝑎) = (1st ‘𝑐)) ∧ 𝑏 ∈ 𝑌) ∧ (𝐺‘𝑏) = (2nd ‘𝑐)) → ⟨(𝐹‘𝑎), (𝐺‘𝑏)⟩ = ⟨(1st ‘𝑐), (2nd ‘𝑐)⟩)
26	13	ad5antr 766	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑐 ∈ ((𝐹 “ 𝑋) × (𝐺 “ 𝑌))) ∧ 𝑎 ∈ 𝑋) ∧ (𝐹‘𝑎) = (1st ‘𝑐)) ∧ 𝑏 ∈ 𝑌) ∧ (𝐺‘𝑏) = (2nd ‘𝑐)) → 𝑋 ⊆ 𝐴)
27	26, 19	sseldd 3569	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑐 ∈ ((𝐹 “ 𝑋) × (𝐺 “ 𝑌))) ∧ 𝑎 ∈ 𝑋) ∧ (𝐹‘𝑎) = (1st ‘𝑐)) ∧ 𝑏 ∈ 𝑌) ∧ (𝐺‘𝑏) = (2nd ‘𝑐)) → 𝑎 ∈ 𝐴)
28	14	ad5antr 766	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑐 ∈ ((𝐹 “ 𝑋) × (𝐺 “ 𝑌))) ∧ 𝑎 ∈ 𝑋) ∧ (𝐹‘𝑎) = (1st ‘𝑐)) ∧ 𝑏 ∈ 𝑌) ∧ (𝐺‘𝑏) = (2nd ‘𝑐)) → 𝑌 ⊆ 𝐵)
29	28, 20	sseldd 3569	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑐 ∈ ((𝐹 “ 𝑋) × (𝐺 “ 𝑌))) ∧ 𝑎 ∈ 𝑋) ∧ (𝐹‘𝑎) = (1st ‘𝑐)) ∧ 𝑏 ∈ 𝑌) ∧ (𝐺‘𝑏) = (2nd ‘𝑐)) → 𝑏 ∈ 𝐵)
30	2, 27, 29	fvproj 29227	. . . . . . . 8 ⊢ ((((((𝜑 ∧ 𝑐 ∈ ((𝐹 “ 𝑋) × (𝐺 “ 𝑌))) ∧ 𝑎 ∈ 𝑋) ∧ (𝐹‘𝑎) = (1st ‘𝑐)) ∧ 𝑏 ∈ 𝑌) ∧ (𝐺‘𝑏) = (2nd ‘𝑐)) → (𝐻‘⟨𝑎, 𝑏⟩) = ⟨(𝐹‘𝑎), (𝐺‘𝑏)⟩)
31		1st2nd2 7096	. . . . . . . . 9 ⊢ (𝑐 ∈ ((𝐹 “ 𝑋) × (𝐺 “ 𝑌)) → 𝑐 = ⟨(1st ‘𝑐), (2nd ‘𝑐)⟩)
32	31	ad5antlr 767	. . . . . . . 8 ⊢ ((((((𝜑 ∧ 𝑐 ∈ ((𝐹 “ 𝑋) × (𝐺 “ 𝑌))) ∧ 𝑎 ∈ 𝑋) ∧ (𝐹‘𝑎) = (1st ‘𝑐)) ∧ 𝑏 ∈ 𝑌) ∧ (𝐺‘𝑏) = (2nd ‘𝑐)) → 𝑐 = ⟨(1st ‘𝑐), (2nd ‘𝑐)⟩)
33	25, 30, 32	3eqtr4d 2654	. . . . . . 7 ⊢ ((((((𝜑 ∧ 𝑐 ∈ ((𝐹 “ 𝑋) × (𝐺 “ 𝑌))) ∧ 𝑎 ∈ 𝑋) ∧ (𝐹‘𝑎) = (1st ‘𝑐)) ∧ 𝑏 ∈ 𝑌) ∧ (𝐺‘𝑏) = (2nd ‘𝑐)) → (𝐻‘⟨𝑎, 𝑏⟩) = 𝑐)
34		fveq2 6103	. . . . . . . . 9 ⊢ (𝑧 = ⟨𝑎, 𝑏⟩ → (𝐻‘𝑧) = (𝐻‘⟨𝑎, 𝑏⟩))
35	34	eqeq1d 2612	. . . . . . . 8 ⊢ (𝑧 = ⟨𝑎, 𝑏⟩ → ((𝐻‘𝑧) = 𝑐 ↔ (𝐻‘⟨𝑎, 𝑏⟩) = 𝑐))
36	35	rspcev 3282	. . . . . . 7 ⊢ ((⟨𝑎, 𝑏⟩ ∈ (𝑋 × 𝑌) ∧ (𝐻‘⟨𝑎, 𝑏⟩) = 𝑐) → ∃𝑧 ∈ (𝑋 × 𝑌)(𝐻‘𝑧) = 𝑐)
37	22, 33, 36	syl2anc 691	. . . . . 6 ⊢ ((((((𝜑 ∧ 𝑐 ∈ ((𝐹 “ 𝑋) × (𝐺 “ 𝑌))) ∧ 𝑎 ∈ 𝑋) ∧ (𝐹‘𝑎) = (1st ‘𝑐)) ∧ 𝑏 ∈ 𝑌) ∧ (𝐺‘𝑏) = (2nd ‘𝑐)) → ∃𝑧 ∈ (𝑋 × 𝑌)(𝐻‘𝑧) = 𝑐)
38		fimaproj.g	. . . . . . . . 9 ⊢ (𝜑 → 𝐺 Fn 𝐵)
39	38	ad3antrrr 762	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑐 ∈ ((𝐹 “ 𝑋) × (𝐺 “ 𝑌))) ∧ 𝑎 ∈ 𝑋) ∧ (𝐹‘𝑎) = (1st ‘𝑐)) → 𝐺 Fn 𝐵)
40		fnfun 5902	. . . . . . . 8 ⊢ (𝐺 Fn 𝐵 → Fun 𝐺)
41	39, 40	syl 17	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑐 ∈ ((𝐹 “ 𝑋) × (𝐺 “ 𝑌))) ∧ 𝑎 ∈ 𝑋) ∧ (𝐹‘𝑎) = (1st ‘𝑐)) → Fun 𝐺)
42		xp2nd 7090	. . . . . . . 8 ⊢ (𝑐 ∈ ((𝐹 “ 𝑋) × (𝐺 “ 𝑌)) → (2nd ‘𝑐) ∈ (𝐺 “ 𝑌))
43	42	ad3antlr 763	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑐 ∈ ((𝐹 “ 𝑋) × (𝐺 “ 𝑌))) ∧ 𝑎 ∈ 𝑋) ∧ (𝐹‘𝑎) = (1st ‘𝑐)) → (2nd ‘𝑐) ∈ (𝐺 “ 𝑌))
44		fvelima 6158	. . . . . . 7 ⊢ ((Fun 𝐺 ∧ (2nd ‘𝑐) ∈ (𝐺 “ 𝑌)) → ∃𝑏 ∈ 𝑌 (𝐺‘𝑏) = (2nd ‘𝑐))
45	41, 43, 44	syl2anc 691	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑐 ∈ ((𝐹 “ 𝑋) × (𝐺 “ 𝑌))) ∧ 𝑎 ∈ 𝑋) ∧ (𝐹‘𝑎) = (1st ‘𝑐)) → ∃𝑏 ∈ 𝑌 (𝐺‘𝑏) = (2nd ‘𝑐))
46	37, 45	r19.29a 3060	. . . . 5 ⊢ ((((𝜑 ∧ 𝑐 ∈ ((𝐹 “ 𝑋) × (𝐺 “ 𝑌))) ∧ 𝑎 ∈ 𝑋) ∧ (𝐹‘𝑎) = (1st ‘𝑐)) → ∃𝑧 ∈ (𝑋 × 𝑌)(𝐻‘𝑧) = 𝑐)
47		fimaproj.f	. . . . . . . 8 ⊢ (𝜑 → 𝐹 Fn 𝐴)
48	47	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐹 “ 𝑋) × (𝐺 “ 𝑌))) → 𝐹 Fn 𝐴)
49		fnfun 5902	. . . . . . 7 ⊢ (𝐹 Fn 𝐴 → Fun 𝐹)
50	48, 49	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐹 “ 𝑋) × (𝐺 “ 𝑌))) → Fun 𝐹)
51		xp1st 7089	. . . . . . 7 ⊢ (𝑐 ∈ ((𝐹 “ 𝑋) × (𝐺 “ 𝑌)) → (1st ‘𝑐) ∈ (𝐹 “ 𝑋))
52	51	adantl 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐹 “ 𝑋) × (𝐺 “ 𝑌))) → (1st ‘𝑐) ∈ (𝐹 “ 𝑋))
53		fvelima 6158	. . . . . 6 ⊢ ((Fun 𝐹 ∧ (1st ‘𝑐) ∈ (𝐹 “ 𝑋)) → ∃𝑎 ∈ 𝑋 (𝐹‘𝑎) = (1st ‘𝑐))
54	50, 52, 53	syl2anc 691	. . . . 5 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐹 “ 𝑋) × (𝐺 “ 𝑌))) → ∃𝑎 ∈ 𝑋 (𝐹‘𝑎) = (1st ‘𝑐))
55	46, 54	r19.29a 3060	. . . 4 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝐹 “ 𝑋) × (𝐺 “ 𝑌))) → ∃𝑧 ∈ (𝑋 × 𝑌)(𝐻‘𝑧) = 𝑐)
56		simpr 476	. . . . . 6 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝑋 × 𝑌)) ∧ (𝐻‘𝑧) = 𝑐) → (𝐻‘𝑧) = 𝑐)
57	16	ad2antrr 758	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝑋 × 𝑌)) ∧ (𝐻‘𝑧) = 𝑐) → (𝑋 × 𝑌) ⊆ (𝐴 × 𝐵))
58		simplr 788	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝑋 × 𝑌)) ∧ (𝐻‘𝑧) = 𝑐) → 𝑧 ∈ (𝑋 × 𝑌))
59	57, 58	sseldd 3569	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝑋 × 𝑌)) ∧ (𝐻‘𝑧) = 𝑐) → 𝑧 ∈ (𝐴 × 𝐵))
60	11	fvmpt2 6200	. . . . . . . 8 ⊢ ((𝑧 ∈ (𝐴 × 𝐵) ∧ ⟨(𝐹‘(1st ‘𝑧)), (𝐺‘(2nd ‘𝑧))⟩ ∈ V) → (𝐻‘𝑧) = ⟨(𝐹‘(1st ‘𝑧)), (𝐺‘(2nd ‘𝑧))⟩)
61	59, 1, 60	sylancl 693	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝑋 × 𝑌)) ∧ (𝐻‘𝑧) = 𝑐) → (𝐻‘𝑧) = ⟨(𝐹‘(1st ‘𝑧)), (𝐺‘(2nd ‘𝑧))⟩)
62	47	ad2antrr 758	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝑋 × 𝑌)) ∧ (𝐻‘𝑧) = 𝑐) → 𝐹 Fn 𝐴)
63	13	ad2antrr 758	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝑋 × 𝑌)) ∧ (𝐻‘𝑧) = 𝑐) → 𝑋 ⊆ 𝐴)
64		xp1st 7089	. . . . . . . . . 10 ⊢ (𝑧 ∈ (𝑋 × 𝑌) → (1st ‘𝑧) ∈ 𝑋)
65	58, 64	syl 17	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝑋 × 𝑌)) ∧ (𝐻‘𝑧) = 𝑐) → (1st ‘𝑧) ∈ 𝑋)
66		fnfvima 6400	. . . . . . . . 9 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑋 ⊆ 𝐴 ∧ (1st ‘𝑧) ∈ 𝑋) → (𝐹‘(1st ‘𝑧)) ∈ (𝐹 “ 𝑋))
67	62, 63, 65, 66	syl3anc 1318	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝑋 × 𝑌)) ∧ (𝐻‘𝑧) = 𝑐) → (𝐹‘(1st ‘𝑧)) ∈ (𝐹 “ 𝑋))
68	38	ad2antrr 758	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝑋 × 𝑌)) ∧ (𝐻‘𝑧) = 𝑐) → 𝐺 Fn 𝐵)
69	14	ad2antrr 758	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝑋 × 𝑌)) ∧ (𝐻‘𝑧) = 𝑐) → 𝑌 ⊆ 𝐵)
70		xp2nd 7090	. . . . . . . . . 10 ⊢ (𝑧 ∈ (𝑋 × 𝑌) → (2nd ‘𝑧) ∈ 𝑌)
71	58, 70	syl 17	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝑋 × 𝑌)) ∧ (𝐻‘𝑧) = 𝑐) → (2nd ‘𝑧) ∈ 𝑌)
72		fnfvima 6400	. . . . . . . . 9 ⊢ ((𝐺 Fn 𝐵 ∧ 𝑌 ⊆ 𝐵 ∧ (2nd ‘𝑧) ∈ 𝑌) → (𝐺‘(2nd ‘𝑧)) ∈ (𝐺 “ 𝑌))
73	68, 69, 71, 72	syl3anc 1318	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝑋 × 𝑌)) ∧ (𝐻‘𝑧) = 𝑐) → (𝐺‘(2nd ‘𝑧)) ∈ (𝐺 “ 𝑌))
74		opelxpi 5072	. . . . . . . 8 ⊢ (((𝐹‘(1st ‘𝑧)) ∈ (𝐹 “ 𝑋) ∧ (𝐺‘(2nd ‘𝑧)) ∈ (𝐺 “ 𝑌)) → ⟨(𝐹‘(1st ‘𝑧)), (𝐺‘(2nd ‘𝑧))⟩ ∈ ((𝐹 “ 𝑋) × (𝐺 “ 𝑌)))
75	67, 73, 74	syl2anc 691	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝑋 × 𝑌)) ∧ (𝐻‘𝑧) = 𝑐) → ⟨(𝐹‘(1st ‘𝑧)), (𝐺‘(2nd ‘𝑧))⟩ ∈ ((𝐹 “ 𝑋) × (𝐺 “ 𝑌)))
76	61, 75	eqeltrd 2688	. . . . . 6 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝑋 × 𝑌)) ∧ (𝐻‘𝑧) = 𝑐) → (𝐻‘𝑧) ∈ ((𝐹 “ 𝑋) × (𝐺 “ 𝑌)))
77	56, 76	eqeltrrd 2689	. . . . 5 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝑋 × 𝑌)) ∧ (𝐻‘𝑧) = 𝑐) → 𝑐 ∈ ((𝐹 “ 𝑋) × (𝐺 “ 𝑌)))
78	77	r19.29an 3059	. . . 4 ⊢ ((𝜑 ∧ ∃𝑧 ∈ (𝑋 × 𝑌)(𝐻‘𝑧) = 𝑐) → 𝑐 ∈ ((𝐹 “ 𝑋) × (𝐺 “ 𝑌)))
79	55, 78	impbida 873	. . 3 ⊢ (𝜑 → (𝑐 ∈ ((𝐹 “ 𝑋) × (𝐺 “ 𝑌)) ↔ ∃𝑧 ∈ (𝑋 × 𝑌)(𝐻‘𝑧) = 𝑐))
80	18, 79	bitr4d 270	. 2 ⊢ (𝜑 → (𝑐 ∈ (𝐻 “ (𝑋 × 𝑌)) ↔ 𝑐 ∈ ((𝐹 “ 𝑋) × (𝐺 “ 𝑌))))
81	80	eqrdv 2608	1 ⊢ (𝜑 → (𝐻 “ (𝑋 × 𝑌)) = ((𝐹 “ 𝑋) × (𝐺 “ 𝑌)))

Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   = wceq 1475   ∈ wcel 1977  ∃wrex 2897  Vcvv 3173   ⊆ wss 3540  ⟨cop 4131   ↦ cmpt 4643   × cxp 5036   “ cima 5041  Fun wfun 5798   Fn wfn 5799  ‘cfv 5804   ↦ cmpt2 6551  1^st c1st 7057  2^nd c2nd 7058

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-id 4953  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-iota 5768  df-fun 5806  df-fn 5807  df-fv 5812  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-1st 7059  df-2nd 7060

This theorem is referenced by:  txomap  29229