Theorem imasaddfnlemg 12763

Description: The image structure operation is a function if the original operation is compatible with the function. (Contributed by Mario Carneiro, 23-Feb-2015.)

Hypotheses

Ref	Expression
imasaddf.f	⊢ (𝜑 → 𝐹:𝑉–onto→𝐵)
imasaddf.e	⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (((𝐹‘𝑎) = (𝐹‘𝑝) ∧ (𝐹‘𝑏) = (𝐹‘𝑞)) → (𝐹‘(𝑎 · 𝑏)) = (𝐹‘(𝑝 · 𝑞))))
imasaddflem.a	⊢ (𝜑 → ∙ = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩})
imasaddfnlemg.v	⊢ (𝜑 → 𝑉 ∈ 𝑊)
imasaddfnlemg.x	⊢ (𝜑 → · ∈ 𝐶)

Assertion

Ref	Expression
imasaddfnlemg	⊢ (𝜑 → ∙ Fn (𝐵 × 𝐵))

Distinct variable groups:   𝑞,𝑝,𝐵   𝑎,𝑏,𝑝,𝑞,𝑉   · ,𝑝,𝑞   𝐹,𝑎,𝑏,𝑝,𝑞   𝜑,𝑎,𝑏,𝑝,𝑞   ∙ ,𝑎,𝑏,𝑝,𝑞

Allowed substitution hints:   𝐵(𝑎,𝑏)   𝐶(𝑞,𝑝,𝑎,𝑏)   · (𝑎,𝑏)   𝑊(𝑞,𝑝,𝑎,𝑏)

Proof of Theorem imasaddfnlemg

Dummy variables 𝑤 𝑦 𝑧 𝑥 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		imasaddf.f	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐹:𝑉–onto→𝐵)
2		fof 5453	. . . . . . . . . . . . 13 ⊢ (𝐹:𝑉–onto→𝐵 → 𝐹:𝑉⟶𝐵)
3	1, 2	syl 14	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐹:𝑉⟶𝐵)
4		imasaddfnlemg.v	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑉 ∈ 𝑊)
5	3, 4	fexd 5762	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹 ∈ V)
6		vex 2755	. . . . . . . . . . 11 ⊢ 𝑝 ∈ V
7		fvexg 5549	. . . . . . . . . . 11 ⊢ ((𝐹 ∈ V ∧ 𝑝 ∈ V) → (𝐹‘𝑝) ∈ V)
8	5, 6, 7	sylancl 413	. . . . . . . . . 10 ⊢ (𝜑 → (𝐹‘𝑝) ∈ V)
9		vex 2755	. . . . . . . . . . 11 ⊢ 𝑞 ∈ V
10		fvexg 5549	. . . . . . . . . . 11 ⊢ ((𝐹 ∈ V ∧ 𝑞 ∈ V) → (𝐹‘𝑞) ∈ V)
11	5, 9, 10	sylancl 413	. . . . . . . . . 10 ⊢ (𝜑 → (𝐹‘𝑞) ∈ V)
12		opexg 4243	. . . . . . . . . 10 ⊢ (((𝐹‘𝑝) ∈ V ∧ (𝐹‘𝑞) ∈ V) → ⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩ ∈ V)
13	8, 11, 12	syl2anc 411	. . . . . . . . 9 ⊢ (𝜑 → ⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩ ∈ V)
14		imasaddfnlemg.x	. . . . . . . . . . 11 ⊢ (𝜑 → · ∈ 𝐶)
15	9	a1i 9	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑞 ∈ V)
16		ovexg 5925	. . . . . . . . . . 11 ⊢ ((𝑝 ∈ V ∧ · ∈ 𝐶 ∧ 𝑞 ∈ V) → (𝑝 · 𝑞) ∈ V)
17	6, 14, 15, 16	mp3an2i 1353	. . . . . . . . . 10 ⊢ (𝜑 → (𝑝 · 𝑞) ∈ V)
18		fvexg 5549	. . . . . . . . . 10 ⊢ ((𝐹 ∈ V ∧ (𝑝 · 𝑞) ∈ V) → (𝐹‘(𝑝 · 𝑞)) ∈ V)
19	5, 17, 18	syl2anc 411	. . . . . . . . 9 ⊢ (𝜑 → (𝐹‘(𝑝 · 𝑞)) ∈ V)
20		relsnopg 4745	. . . . . . . . 9 ⊢ ((⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩ ∈ V ∧ (𝐹‘(𝑝 · 𝑞)) ∈ V) → Rel {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩})
21	13, 19, 20	syl2anc 411	. . . . . . . 8 ⊢ (𝜑 → Rel {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩})
22	21	ralrimivw 2564	. . . . . . 7 ⊢ (𝜑 → ∀𝑞 ∈ 𝑉 Rel {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩})
23		reliun 4762	. . . . . . 7 ⊢ (Rel ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ↔ ∀𝑞 ∈ 𝑉 Rel {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩})
24	22, 23	sylibr 134	. . . . . 6 ⊢ (𝜑 → Rel ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩})
25	24	ralrimivw 2564	. . . . 5 ⊢ (𝜑 → ∀𝑝 ∈ 𝑉 Rel ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩})
26		reliun 4762	. . . . 5 ⊢ (Rel ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ↔ ∀𝑝 ∈ 𝑉 Rel ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩})
27	25, 26	sylibr 134	. . . 4 ⊢ (𝜑 → Rel ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩})
28		imasaddflem.a	. . . . 5 ⊢ (𝜑 → ∙ = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩})
29	28	releqd 4725	. . . 4 ⊢ (𝜑 → (Rel ∙ ↔ Rel ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩}))
30	27, 29	mpbird 167	. . 3 ⊢ (𝜑 → Rel ∙ )
31		ffvelcdm 5665	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹:𝑉⟶𝐵 ∧ 𝑝 ∈ 𝑉) → (𝐹‘𝑝) ∈ 𝐵)
32		ffvelcdm 5665	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹:𝑉⟶𝐵 ∧ 𝑞 ∈ 𝑉) → (𝐹‘𝑞) ∈ 𝐵)
33	31, 32	anim12dan 600	. . . . . . . . . . . . . . 15 ⊢ ((𝐹:𝑉⟶𝐵 ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → ((𝐹‘𝑝) ∈ 𝐵 ∧ (𝐹‘𝑞) ∈ 𝐵))
34	3, 33	sylan 283	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → ((𝐹‘𝑝) ∈ 𝐵 ∧ (𝐹‘𝑞) ∈ 𝐵))
35		opelxpi 4673	. . . . . . . . . . . . . 14 ⊢ (((𝐹‘𝑝) ∈ 𝐵 ∧ (𝐹‘𝑞) ∈ 𝐵) → ⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩ ∈ (𝐵 × 𝐵))
36	34, 35	syl 14	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → ⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩ ∈ (𝐵 × 𝐵))
37	19	adantr 276	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (𝐹‘(𝑝 · 𝑞)) ∈ V)
38	36, 37	opelxpd 4674	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → ⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩ ∈ ((𝐵 × 𝐵) × V))
39	38	snssd 3752	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ ((𝐵 × 𝐵) × V))
40	39	anassrs 400	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑉) ∧ 𝑞 ∈ 𝑉) → {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ ((𝐵 × 𝐵) × V))
41	40	iunssd 3947	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑉) → ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ ((𝐵 × 𝐵) × V))
42	41	iunssd 3947	. . . . . . . 8 ⊢ (𝜑 → ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ ((𝐵 × 𝐵) × V))
43	28, 42	eqsstrd 3206	. . . . . . 7 ⊢ (𝜑 → ∙ ⊆ ((𝐵 × 𝐵) × V))
44		dmss 4841	. . . . . . 7 ⊢ ( ∙ ⊆ ((𝐵 × 𝐵) × V) → dom ∙ ⊆ dom ((𝐵 × 𝐵) × V))
45	43, 44	syl 14	. . . . . 6 ⊢ (𝜑 → dom ∙ ⊆ dom ((𝐵 × 𝐵) × V))
46		vn0m 3449	. . . . . . 7 ⊢ ∃𝑤 𝑤 ∈ V
47		dmxpm 4862	. . . . . . 7 ⊢ (∃𝑤 𝑤 ∈ V → dom ((𝐵 × 𝐵) × V) = (𝐵 × 𝐵))
48	46, 47	ax-mp 5	. . . . . 6 ⊢ dom ((𝐵 × 𝐵) × V) = (𝐵 × 𝐵)
49	45, 48	sseqtrdi 3218	. . . . 5 ⊢ (𝜑 → dom ∙ ⊆ (𝐵 × 𝐵))
50		forn 5456	. . . . . . 7 ⊢ (𝐹:𝑉–onto→𝐵 → ran 𝐹 = 𝐵)
51	1, 50	syl 14	. . . . . 6 ⊢ (𝜑 → ran 𝐹 = 𝐵)
52	51	sqxpeqd 4667	. . . . 5 ⊢ (𝜑 → (ran 𝐹 × ran 𝐹) = (𝐵 × 𝐵))
53	49, 52	sseqtrrd 3209	. . . 4 ⊢ (𝜑 → dom ∙ ⊆ (ran 𝐹 × ran 𝐹))
54	28	eleq2d 2259	. . . . . . . . . . . . 13 ⊢ (𝜑 → (⟨⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩, 𝑤⟩ ∈ ∙ ↔ ⟨⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩, 𝑤⟩ ∈ ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩}))
55	54	adantr 276	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → (⟨⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩, 𝑤⟩ ∈ ∙ ↔ ⟨⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩, 𝑤⟩ ∈ ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩}))
56		df-br 4019	. . . . . . . . . . . 12 ⊢ (⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩ ∙ 𝑤 ↔ ⟨⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩, 𝑤⟩ ∈ ∙ )
57		eliun 3905	. . . . . . . . . . . . 13 ⊢ (⟨⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩, 𝑤⟩ ∈ ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ↔ ∃𝑝 ∈ 𝑉 ⟨⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩, 𝑤⟩ ∈ ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩})
58		eliun 3905	. . . . . . . . . . . . . 14 ⊢ (⟨⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩, 𝑤⟩ ∈ ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ↔ ∃𝑞 ∈ 𝑉 ⟨⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩, 𝑤⟩ ∈ {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩})
59	58	rexbii 2497	. . . . . . . . . . . . 13 ⊢ (∃𝑝 ∈ 𝑉 ⟨⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩, 𝑤⟩ ∈ ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ↔ ∃𝑝 ∈ 𝑉 ∃𝑞 ∈ 𝑉 ⟨⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩, 𝑤⟩ ∈ {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩})
60	57, 59	bitr2i 185	. . . . . . . . . . . 12 ⊢ (∃𝑝 ∈ 𝑉 ∃𝑞 ∈ 𝑉 ⟨⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩, 𝑤⟩ ∈ {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ↔ ⟨⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩, 𝑤⟩ ∈ ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩})
61	55, 56, 60	3bitr4g 223	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → (⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩ ∙ 𝑤 ↔ ∃𝑝 ∈ 𝑉 ∃𝑞 ∈ 𝑉 ⟨⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩, 𝑤⟩ ∈ {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩}))
62		vex 2755	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑎 ∈ V
63		fvexg 5549	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐹 ∈ V ∧ 𝑎 ∈ V) → (𝐹‘𝑎) ∈ V)
64	5, 62, 63	sylancl 413	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐹‘𝑎) ∈ V)
65		vex 2755	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑏 ∈ V
66		fvexg 5549	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐹 ∈ V ∧ 𝑏 ∈ V) → (𝐹‘𝑏) ∈ V)
67	5, 65, 66	sylancl 413	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐹‘𝑏) ∈ V)
68		opexg 4243	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐹‘𝑎) ∈ V ∧ (𝐹‘𝑏) ∈ V) → ⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩ ∈ V)
69	64, 67, 68	syl2anc 411	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩ ∈ V)
70		vex 2755	. . . . . . . . . . . . . . . . 17 ⊢ 𝑤 ∈ V
71		opexg 4243	. . . . . . . . . . . . . . . . 17 ⊢ ((⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩ ∈ V ∧ 𝑤 ∈ V) → ⟨⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩, 𝑤⟩ ∈ V)
72	69, 70, 71	sylancl 413	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ⟨⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩, 𝑤⟩ ∈ V)
73		elsng 3622	. . . . . . . . . . . . . . . 16 ⊢ (⟨⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩, 𝑤⟩ ∈ V → (⟨⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩, 𝑤⟩ ∈ {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ↔ ⟨⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩, 𝑤⟩ = ⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩))
74	72, 73	syl 14	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (⟨⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩, 𝑤⟩ ∈ {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ↔ ⟨⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩, 𝑤⟩ = ⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩))
75	74	3ad2ant1 1020	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (⟨⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩, 𝑤⟩ ∈ {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ↔ ⟨⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩, 𝑤⟩ = ⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩))
76		opthg 4253	. . . . . . . . . . . . . . . . 17 ⊢ ((⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩ ∈ V ∧ 𝑤 ∈ V) → (⟨⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩, 𝑤⟩ = ⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩ ↔ (⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩ = ⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩ ∧ 𝑤 = (𝐹‘(𝑝 · 𝑞)))))
77	69, 70, 76	sylancl 413	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (⟨⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩, 𝑤⟩ = ⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩ ↔ (⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩ = ⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩ ∧ 𝑤 = (𝐹‘(𝑝 · 𝑞)))))
78	77	3ad2ant1 1020	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (⟨⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩, 𝑤⟩ = ⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩ ↔ (⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩ = ⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩ ∧ 𝑤 = (𝐹‘(𝑝 · 𝑞)))))
79		opthg 4253	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐹‘𝑎) ∈ V ∧ (𝐹‘𝑏) ∈ V) → (⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩ = ⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩ ↔ ((𝐹‘𝑎) = (𝐹‘𝑝) ∧ (𝐹‘𝑏) = (𝐹‘𝑞))))
80	64, 67, 79	syl2anc 411	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩ = ⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩ ↔ ((𝐹‘𝑎) = (𝐹‘𝑝) ∧ (𝐹‘𝑏) = (𝐹‘𝑞))))
81	80	3ad2ant1 1020	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩ = ⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩ ↔ ((𝐹‘𝑎) = (𝐹‘𝑝) ∧ (𝐹‘𝑏) = (𝐹‘𝑞))))
82		imasaddf.e	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (((𝐹‘𝑎) = (𝐹‘𝑝) ∧ (𝐹‘𝑏) = (𝐹‘𝑞)) → (𝐹‘(𝑎 · 𝑏)) = (𝐹‘(𝑝 · 𝑞))))
83	81, 82	sylbid 150	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩ = ⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩ → (𝐹‘(𝑎 · 𝑏)) = (𝐹‘(𝑝 · 𝑞))))
84		eqeq2 2199	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹‘(𝑎 · 𝑏)) = (𝐹‘(𝑝 · 𝑞)) → (𝑤 = (𝐹‘(𝑎 · 𝑏)) ↔ 𝑤 = (𝐹‘(𝑝 · 𝑞))))
85	84	biimprd 158	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹‘(𝑎 · 𝑏)) = (𝐹‘(𝑝 · 𝑞)) → (𝑤 = (𝐹‘(𝑝 · 𝑞)) → 𝑤 = (𝐹‘(𝑎 · 𝑏))))
86	83, 85	syl6 33	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩ = ⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩ → (𝑤 = (𝐹‘(𝑝 · 𝑞)) → 𝑤 = (𝐹‘(𝑎 · 𝑏)))))
87	86	impd 254	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → ((⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩ = ⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩ ∧ 𝑤 = (𝐹‘(𝑝 · 𝑞))) → 𝑤 = (𝐹‘(𝑎 · 𝑏))))
88	78, 87	sylbid 150	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (⟨⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩, 𝑤⟩ = ⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩ → 𝑤 = (𝐹‘(𝑎 · 𝑏))))
89	75, 88	sylbid 150	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (⟨⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩, 𝑤⟩ ∈ {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} → 𝑤 = (𝐹‘(𝑎 · 𝑏))))
90	89	3expa 1205	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (⟨⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩, 𝑤⟩ ∈ {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} → 𝑤 = (𝐹‘(𝑎 · 𝑏))))
91	90	rexlimdvva 2615	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → (∃𝑝 ∈ 𝑉 ∃𝑞 ∈ 𝑉 ⟨⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩, 𝑤⟩ ∈ {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} → 𝑤 = (𝐹‘(𝑎 · 𝑏))))
92	61, 91	sylbid 150	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → (⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩ ∙ 𝑤 → 𝑤 = (𝐹‘(𝑎 · 𝑏))))
93	92	alrimiv 1885	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → ∀𝑤(⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩ ∙ 𝑤 → 𝑤 = (𝐹‘(𝑎 · 𝑏))))
94		mo2icl 2931	. . . . . . . . 9 ⊢ (∀𝑤(⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩ ∙ 𝑤 → 𝑤 = (𝐹‘(𝑎 · 𝑏))) → ∃*𝑤⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩ ∙ 𝑤)
95	93, 94	syl 14	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → ∃*𝑤⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩ ∙ 𝑤)
96	95	ralrimivva 2572	. . . . . . 7 ⊢ (𝜑 → ∀𝑎 ∈ 𝑉 ∀𝑏 ∈ 𝑉 ∃*𝑤⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩ ∙ 𝑤)
97		fofn 5455	. . . . . . . . . 10 ⊢ (𝐹:𝑉–onto→𝐵 → 𝐹 Fn 𝑉)
98	1, 97	syl 14	. . . . . . . . 9 ⊢ (𝜑 → 𝐹 Fn 𝑉)
99		opeq2 3794	. . . . . . . . . . . 12 ⊢ (𝑧 = (𝐹‘𝑏) → ⟨(𝐹‘𝑎), 𝑧⟩ = ⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩)
100	99	breq1d 4028	. . . . . . . . . . 11 ⊢ (𝑧 = (𝐹‘𝑏) → (⟨(𝐹‘𝑎), 𝑧⟩ ∙ 𝑤 ↔ ⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩ ∙ 𝑤))
101	100	mobidv 2074	. . . . . . . . . 10 ⊢ (𝑧 = (𝐹‘𝑏) → (∃*𝑤⟨(𝐹‘𝑎), 𝑧⟩ ∙ 𝑤 ↔ ∃*𝑤⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩ ∙ 𝑤))
102	101	ralrn 5670	. . . . . . . . 9 ⊢ (𝐹 Fn 𝑉 → (∀𝑧 ∈ ran 𝐹∃*𝑤⟨(𝐹‘𝑎), 𝑧⟩ ∙ 𝑤 ↔ ∀𝑏 ∈ 𝑉 ∃*𝑤⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩ ∙ 𝑤))
103	98, 102	syl 14	. . . . . . . 8 ⊢ (𝜑 → (∀𝑧 ∈ ran 𝐹∃*𝑤⟨(𝐹‘𝑎), 𝑧⟩ ∙ 𝑤 ↔ ∀𝑏 ∈ 𝑉 ∃*𝑤⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩ ∙ 𝑤))
104	103	ralbidv 2490	. . . . . . 7 ⊢ (𝜑 → (∀𝑎 ∈ 𝑉 ∀𝑧 ∈ ran 𝐹∃*𝑤⟨(𝐹‘𝑎), 𝑧⟩ ∙ 𝑤 ↔ ∀𝑎 ∈ 𝑉 ∀𝑏 ∈ 𝑉 ∃*𝑤⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩ ∙ 𝑤))
105	96, 104	mpbird 167	. . . . . 6 ⊢ (𝜑 → ∀𝑎 ∈ 𝑉 ∀𝑧 ∈ ran 𝐹∃*𝑤⟨(𝐹‘𝑎), 𝑧⟩ ∙ 𝑤)
106		opeq1 3793	. . . . . . . . . . 11 ⊢ (𝑦 = (𝐹‘𝑎) → ⟨𝑦, 𝑧⟩ = ⟨(𝐹‘𝑎), 𝑧⟩)
107	106	breq1d 4028	. . . . . . . . . 10 ⊢ (𝑦 = (𝐹‘𝑎) → (⟨𝑦, 𝑧⟩ ∙ 𝑤 ↔ ⟨(𝐹‘𝑎), 𝑧⟩ ∙ 𝑤))
108	107	mobidv 2074	. . . . . . . . 9 ⊢ (𝑦 = (𝐹‘𝑎) → (∃*𝑤⟨𝑦, 𝑧⟩ ∙ 𝑤 ↔ ∃*𝑤⟨(𝐹‘𝑎), 𝑧⟩ ∙ 𝑤))
109	108	ralbidv 2490	. . . . . . . 8 ⊢ (𝑦 = (𝐹‘𝑎) → (∀𝑧 ∈ ran 𝐹∃*𝑤⟨𝑦, 𝑧⟩ ∙ 𝑤 ↔ ∀𝑧 ∈ ran 𝐹∃*𝑤⟨(𝐹‘𝑎), 𝑧⟩ ∙ 𝑤))
110	109	ralrn 5670	. . . . . . 7 ⊢ (𝐹 Fn 𝑉 → (∀𝑦 ∈ ran 𝐹∀𝑧 ∈ ran 𝐹∃*𝑤⟨𝑦, 𝑧⟩ ∙ 𝑤 ↔ ∀𝑎 ∈ 𝑉 ∀𝑧 ∈ ran 𝐹∃*𝑤⟨(𝐹‘𝑎), 𝑧⟩ ∙ 𝑤))
111	98, 110	syl 14	. . . . . 6 ⊢ (𝜑 → (∀𝑦 ∈ ran 𝐹∀𝑧 ∈ ran 𝐹∃*𝑤⟨𝑦, 𝑧⟩ ∙ 𝑤 ↔ ∀𝑎 ∈ 𝑉 ∀𝑧 ∈ ran 𝐹∃*𝑤⟨(𝐹‘𝑎), 𝑧⟩ ∙ 𝑤))
112	105, 111	mpbird 167	. . . . 5 ⊢ (𝜑 → ∀𝑦 ∈ ran 𝐹∀𝑧 ∈ ran 𝐹∃*𝑤⟨𝑦, 𝑧⟩ ∙ 𝑤)
113		breq1 4021	. . . . . . 7 ⊢ (𝑥 = ⟨𝑦, 𝑧⟩ → (𝑥 ∙ 𝑤 ↔ ⟨𝑦, 𝑧⟩ ∙ 𝑤))
114	113	mobidv 2074	. . . . . 6 ⊢ (𝑥 = ⟨𝑦, 𝑧⟩ → (∃*𝑤 𝑥 ∙ 𝑤 ↔ ∃*𝑤⟨𝑦, 𝑧⟩ ∙ 𝑤))
115	114	ralxp 4785	. . . . 5 ⊢ (∀𝑥 ∈ (ran 𝐹 × ran 𝐹)∃*𝑤 𝑥 ∙ 𝑤 ↔ ∀𝑦 ∈ ran 𝐹∀𝑧 ∈ ran 𝐹∃*𝑤⟨𝑦, 𝑧⟩ ∙ 𝑤)
116	112, 115	sylibr 134	. . . 4 ⊢ (𝜑 → ∀𝑥 ∈ (ran 𝐹 × ran 𝐹)∃*𝑤 𝑥 ∙ 𝑤)
117		ssralv 3234	. . . 4 ⊢ (dom ∙ ⊆ (ran 𝐹 × ran 𝐹) → (∀𝑥 ∈ (ran 𝐹 × ran 𝐹)∃*𝑤 𝑥 ∙ 𝑤 → ∀𝑥 ∈ dom ∙ ∃*𝑤 𝑥 ∙ 𝑤))
118	53, 116, 117	sylc 62	. . 3 ⊢ (𝜑 → ∀𝑥 ∈ dom ∙ ∃*𝑤 𝑥 ∙ 𝑤)
119		dffun7 5258	. . 3 ⊢ (Fun ∙ ↔ (Rel ∙ ∧ ∀𝑥 ∈ dom ∙ ∃*𝑤 𝑥 ∙ 𝑤))
120	30, 118, 119	sylanbrc 417	. 2 ⊢ (𝜑 → Fun ∙ )
121		eqimss2 3225	. . . . . . . . . . 11 ⊢ ( ∙ = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} → ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ ∙ )
122	28, 121	syl 14	. . . . . . . . . 10 ⊢ (𝜑 → ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ ∙ )
123		iunss 3942	. . . . . . . . . 10 ⊢ (∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ ∙ ↔ ∀𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ ∙ )
124	122, 123	sylib 122	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ ∙ )
125		iunss 3942	. . . . . . . . . . 11 ⊢ (∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ ∙ ↔ ∀𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ ∙ )
126		opexg 4243	. . . . . . . . . . . . . . 15 ⊢ ((⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩ ∈ V ∧ (𝐹‘(𝑝 · 𝑞)) ∈ V) → ⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩ ∈ V)
127	13, 19, 126	syl2anc 411	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩ ∈ V)
128		snssg 3741	. . . . . . . . . . . . . 14 ⊢ (⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩ ∈ V → (⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩ ∈ ∙ ↔ {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ ∙ ))
129	127, 128	syl 14	. . . . . . . . . . . . 13 ⊢ (𝜑 → (⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩ ∈ ∙ ↔ {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ ∙ ))
130		opeldmg 4847	. . . . . . . . . . . . . 14 ⊢ ((⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩ ∈ V ∧ (𝐹‘(𝑝 · 𝑞)) ∈ V) → (⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩ ∈ ∙ → ⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩ ∈ dom ∙ ))
131	13, 19, 130	syl2anc 411	. . . . . . . . . . . . 13 ⊢ (𝜑 → (⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩ ∈ ∙ → ⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩ ∈ dom ∙ ))
132	129, 131	sylbird 170	. . . . . . . . . . . 12 ⊢ (𝜑 → ({⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ ∙ → ⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩ ∈ dom ∙ ))
133	132	ralimdv 2558	. . . . . . . . . . 11 ⊢ (𝜑 → (∀𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ ∙ → ∀𝑞 ∈ 𝑉 ⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩ ∈ dom ∙ ))
134	125, 133	biimtrid 152	. . . . . . . . . 10 ⊢ (𝜑 → (∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ ∙ → ∀𝑞 ∈ 𝑉 ⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩ ∈ dom ∙ ))
135	134	ralimdv 2558	. . . . . . . . 9 ⊢ (𝜑 → (∀𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ ∙ → ∀𝑝 ∈ 𝑉 ∀𝑞 ∈ 𝑉 ⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩ ∈ dom ∙ ))
136	124, 135	mpd 13	. . . . . . . 8 ⊢ (𝜑 → ∀𝑝 ∈ 𝑉 ∀𝑞 ∈ 𝑉 ⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩ ∈ dom ∙ )
137		opeq2 3794	. . . . . . . . . . . 12 ⊢ (𝑧 = (𝐹‘𝑞) → ⟨(𝐹‘𝑝), 𝑧⟩ = ⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩)
138	137	eleq1d 2258	. . . . . . . . . . 11 ⊢ (𝑧 = (𝐹‘𝑞) → (⟨(𝐹‘𝑝), 𝑧⟩ ∈ dom ∙ ↔ ⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩ ∈ dom ∙ ))
139	138	ralrn 5670	. . . . . . . . . 10 ⊢ (𝐹 Fn 𝑉 → (∀𝑧 ∈ ran 𝐹⟨(𝐹‘𝑝), 𝑧⟩ ∈ dom ∙ ↔ ∀𝑞 ∈ 𝑉 ⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩ ∈ dom ∙ ))
140	98, 139	syl 14	. . . . . . . . 9 ⊢ (𝜑 → (∀𝑧 ∈ ran 𝐹⟨(𝐹‘𝑝), 𝑧⟩ ∈ dom ∙ ↔ ∀𝑞 ∈ 𝑉 ⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩ ∈ dom ∙ ))
141	140	ralbidv 2490	. . . . . . . 8 ⊢ (𝜑 → (∀𝑝 ∈ 𝑉 ∀𝑧 ∈ ran 𝐹⟨(𝐹‘𝑝), 𝑧⟩ ∈ dom ∙ ↔ ∀𝑝 ∈ 𝑉 ∀𝑞 ∈ 𝑉 ⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩ ∈ dom ∙ ))
142	136, 141	mpbird 167	. . . . . . 7 ⊢ (𝜑 → ∀𝑝 ∈ 𝑉 ∀𝑧 ∈ ran 𝐹⟨(𝐹‘𝑝), 𝑧⟩ ∈ dom ∙ )
143		opeq1 3793	. . . . . . . . . . 11 ⊢ (𝑦 = (𝐹‘𝑝) → ⟨𝑦, 𝑧⟩ = ⟨(𝐹‘𝑝), 𝑧⟩)
144	143	eleq1d 2258	. . . . . . . . . 10 ⊢ (𝑦 = (𝐹‘𝑝) → (⟨𝑦, 𝑧⟩ ∈ dom ∙ ↔ ⟨(𝐹‘𝑝), 𝑧⟩ ∈ dom ∙ ))
145	144	ralbidv 2490	. . . . . . . . 9 ⊢ (𝑦 = (𝐹‘𝑝) → (∀𝑧 ∈ ran 𝐹⟨𝑦, 𝑧⟩ ∈ dom ∙ ↔ ∀𝑧 ∈ ran 𝐹⟨(𝐹‘𝑝), 𝑧⟩ ∈ dom ∙ ))
146	145	ralrn 5670	. . . . . . . 8 ⊢ (𝐹 Fn 𝑉 → (∀𝑦 ∈ ran 𝐹∀𝑧 ∈ ran 𝐹⟨𝑦, 𝑧⟩ ∈ dom ∙ ↔ ∀𝑝 ∈ 𝑉 ∀𝑧 ∈ ran 𝐹⟨(𝐹‘𝑝), 𝑧⟩ ∈ dom ∙ ))
147	98, 146	syl 14	. . . . . . 7 ⊢ (𝜑 → (∀𝑦 ∈ ran 𝐹∀𝑧 ∈ ran 𝐹⟨𝑦, 𝑧⟩ ∈ dom ∙ ↔ ∀𝑝 ∈ 𝑉 ∀𝑧 ∈ ran 𝐹⟨(𝐹‘𝑝), 𝑧⟩ ∈ dom ∙ ))
148	142, 147	mpbird 167	. . . . . 6 ⊢ (𝜑 → ∀𝑦 ∈ ran 𝐹∀𝑧 ∈ ran 𝐹⟨𝑦, 𝑧⟩ ∈ dom ∙ )
149		eleq1 2252	. . . . . . 7 ⊢ (𝑥 = ⟨𝑦, 𝑧⟩ → (𝑥 ∈ dom ∙ ↔ ⟨𝑦, 𝑧⟩ ∈ dom ∙ ))
150	149	ralxp 4785	. . . . . 6 ⊢ (∀𝑥 ∈ (ran 𝐹 × ran 𝐹)𝑥 ∈ dom ∙ ↔ ∀𝑦 ∈ ran 𝐹∀𝑧 ∈ ran 𝐹⟨𝑦, 𝑧⟩ ∈ dom ∙ )
151	148, 150	sylibr 134	. . . . 5 ⊢ (𝜑 → ∀𝑥 ∈ (ran 𝐹 × ran 𝐹)𝑥 ∈ dom ∙ )
152		dfss3 3160	. . . . 5 ⊢ ((ran 𝐹 × ran 𝐹) ⊆ dom ∙ ↔ ∀𝑥 ∈ (ran 𝐹 × ran 𝐹)𝑥 ∈ dom ∙ )
153	151, 152	sylibr 134	. . . 4 ⊢ (𝜑 → (ran 𝐹 × ran 𝐹) ⊆ dom ∙ )
154	52, 153	eqsstrrd 3207	. . 3 ⊢ (𝜑 → (𝐵 × 𝐵) ⊆ dom ∙ )
155	49, 154	eqssd 3187	. 2 ⊢ (𝜑 → dom ∙ = (𝐵 × 𝐵))
156		df-fn 5234	. 2 ⊢ ( ∙ Fn (𝐵 × 𝐵) ↔ (Fun ∙ ∧ dom ∙ = (𝐵 × 𝐵)))
157	120, 155, 156	sylanbrc 417	1 ⊢ (𝜑 → ∙ Fn (𝐵 × 𝐵))

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105   ∧ w3a 980  ∀wal 1362   = wceq 1364  ∃wex 1503  ∃*wmo 2039   ∈ wcel 2160  ∀wral 2468  ∃wrex 2469  Vcvv 2752   ⊆ wss 3144  {csn 3607  ⟨cop 3610  ∪ ciun 3901   class class class wbr 4018   × cxp 4639  dom cdm 4641  ran crn 4642  Rel wrel 4646  Fun wfun 5225   Fn wfn 5226  ⟶wf 5227  –onto→wfo 5229  ‘cfv 5231  (class class class)co 5891

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-13 2162  ax-14 2163  ax-ext 2171  ax-coll 4133  ax-sep 4136  ax-pow 4189  ax-pr 4224  ax-un 4448

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-eu 2041  df-mo 2042  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-ral 2473  df-rex 2474  df-reu 2475  df-rab 2477  df-v 2754  df-sbc 2978  df-csb 3073  df-un 3148  df-in 3150  df-ss 3157  df-pw 3592  df-sn 3613  df-pr 3614  df-op 3616  df-uni 3825  df-iun 3903  df-br 4019  df-opab 4080  df-mpt 4081  df-id 4308  df-xp 4647  df-rel 4648  df-cnv 4649  df-co 4650  df-dm 4651  df-rn 4652  df-res 4653  df-ima 4654  df-iota 5193  df-fun 5233  df-fn 5234  df-f 5235  df-f1 5236  df-fo 5237  df-f1o 5238  df-fv 5239  df-ov 5894

This theorem is referenced by:  imasaddvallemg  12764  imasaddflemg  12765  imasaddfn  12766  imasmulfn  12769