Theorem imasaddfnlemg 13231

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 5515	. . . . . . . . . . . . 13 ⊢ (𝐹:𝑉–onto→𝐵 → 𝐹:𝑉⟶𝐵)
3	1, 2	syl 14	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐹:𝑉⟶𝐵)
4		imasaddfnlemg.v	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑉 ∈ 𝑊)
5	3, 4	fexd 5832	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹 ∈ V)
6		vex 2776	. . . . . . . . . . 11 ⊢ 𝑝 ∈ V
7		fvexg 5613	. . . . . . . . . . 11 ⊢ ((𝐹 ∈ V ∧ 𝑝 ∈ V) → (𝐹‘𝑝) ∈ V)
8	5, 6, 7	sylancl 413	. . . . . . . . . 10 ⊢ (𝜑 → (𝐹‘𝑝) ∈ V)
9		vex 2776	. . . . . . . . . . 11 ⊢ 𝑞 ∈ V
10		fvexg 5613	. . . . . . . . . . 11 ⊢ ((𝐹 ∈ V ∧ 𝑞 ∈ V) → (𝐹‘𝑞) ∈ V)
11	5, 9, 10	sylancl 413	. . . . . . . . . 10 ⊢ (𝜑 → (𝐹‘𝑞) ∈ V)
12		opexg 4285	. . . . . . . . . 10 ⊢ (((𝐹‘𝑝) ∈ V ∧ (𝐹‘𝑞) ∈ V) → ⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩ ∈ V)
13	8, 11, 12	syl2anc 411	. . . . . . . . 9 ⊢ (𝜑 → ⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩ ∈ V)
14		imasaddfnlemg.x	. . . . . . . . . . 11 ⊢ (𝜑 → · ∈ 𝐶)
15	9	a1i 9	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑞 ∈ V)
16		ovexg 5996	. . . . . . . . . . 11 ⊢ ((𝑝 ∈ V ∧ · ∈ 𝐶 ∧ 𝑞 ∈ V) → (𝑝 · 𝑞) ∈ V)
17	6, 14, 15, 16	mp3an2i 1355	. . . . . . . . . 10 ⊢ (𝜑 → (𝑝 · 𝑞) ∈ V)
18		fvexg 5613	. . . . . . . . . 10 ⊢ ((𝐹 ∈ V ∧ (𝑝 · 𝑞) ∈ V) → (𝐹‘(𝑝 · 𝑞)) ∈ V)
19	5, 17, 18	syl2anc 411	. . . . . . . . 9 ⊢ (𝜑 → (𝐹‘(𝑝 · 𝑞)) ∈ V)
20		relsnopg 4792	. . . . . . . . 9 ⊢ ((⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩ ∈ V ∧ (𝐹‘(𝑝 · 𝑞)) ∈ V) → Rel {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩})
21	13, 19, 20	syl2anc 411	. . . . . . . 8 ⊢ (𝜑 → Rel {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩})
22	21	ralrimivw 2581	. . . . . . 7 ⊢ (𝜑 → ∀𝑞 ∈ 𝑉 Rel {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩})
23		reliun 4809	. . . . . . 7 ⊢ (Rel ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ↔ ∀𝑞 ∈ 𝑉 Rel {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩})
24	22, 23	sylibr 134	. . . . . 6 ⊢ (𝜑 → Rel ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩})
25	24	ralrimivw 2581	. . . . 5 ⊢ (𝜑 → ∀𝑝 ∈ 𝑉 Rel ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩})
26		reliun 4809	. . . . 5 ⊢ (Rel ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ↔ ∀𝑝 ∈ 𝑉 Rel ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩})
27	25, 26	sylibr 134	. . . 4 ⊢ (𝜑 → Rel ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩})
28		imasaddflem.a	. . . . 5 ⊢ (𝜑 → ∙ = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩})
29	28	releqd 4772	. . . 4 ⊢ (𝜑 → (Rel ∙ ↔ Rel ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩}))
30	27, 29	mpbird 167	. . 3 ⊢ (𝜑 → Rel ∙ )
31		ffvelcdm 5731	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹:𝑉⟶𝐵 ∧ 𝑝 ∈ 𝑉) → (𝐹‘𝑝) ∈ 𝐵)
32		ffvelcdm 5731	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹:𝑉⟶𝐵 ∧ 𝑞 ∈ 𝑉) → (𝐹‘𝑞) ∈ 𝐵)
33	31, 32	anim12dan 600	. . . . . . . . . . . . . . 15 ⊢ ((𝐹:𝑉⟶𝐵 ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → ((𝐹‘𝑝) ∈ 𝐵 ∧ (𝐹‘𝑞) ∈ 𝐵))
34	3, 33	sylan 283	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → ((𝐹‘𝑝) ∈ 𝐵 ∧ (𝐹‘𝑞) ∈ 𝐵))
35		opelxpi 4720	. . . . . . . . . . . . . 14 ⊢ (((𝐹‘𝑝) ∈ 𝐵 ∧ (𝐹‘𝑞) ∈ 𝐵) → ⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩ ∈ (𝐵 × 𝐵))
36	34, 35	syl 14	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → ⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩ ∈ (𝐵 × 𝐵))
37	19	adantr 276	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (𝐹‘(𝑝 · 𝑞)) ∈ V)
38	36, 37	opelxpd 4721	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → ⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩ ∈ ((𝐵 × 𝐵) × V))
39	38	snssd 3784	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ ((𝐵 × 𝐵) × V))
40	39	anassrs 400	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑉) ∧ 𝑞 ∈ 𝑉) → {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ ((𝐵 × 𝐵) × V))
41	40	iunssd 3982	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑉) → ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ ((𝐵 × 𝐵) × V))
42	41	iunssd 3982	. . . . . . . 8 ⊢ (𝜑 → ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ ((𝐵 × 𝐵) × V))
43	28, 42	eqsstrd 3233	. . . . . . 7 ⊢ (𝜑 → ∙ ⊆ ((𝐵 × 𝐵) × V))
44		dmss 4891	. . . . . . 7 ⊢ ( ∙ ⊆ ((𝐵 × 𝐵) × V) → dom ∙ ⊆ dom ((𝐵 × 𝐵) × V))
45	43, 44	syl 14	. . . . . 6 ⊢ (𝜑 → dom ∙ ⊆ dom ((𝐵 × 𝐵) × V))
46		vn0m 3476	. . . . . . 7 ⊢ ∃𝑤 𝑤 ∈ V
47		dmxpm 4912	. . . . . . 7 ⊢ (∃𝑤 𝑤 ∈ V → dom ((𝐵 × 𝐵) × V) = (𝐵 × 𝐵))
48	46, 47	ax-mp 5	. . . . . 6 ⊢ dom ((𝐵 × 𝐵) × V) = (𝐵 × 𝐵)
49	45, 48	sseqtrdi 3245	. . . . 5 ⊢ (𝜑 → dom ∙ ⊆ (𝐵 × 𝐵))
50		forn 5518	. . . . . . 7 ⊢ (𝐹:𝑉–onto→𝐵 → ran 𝐹 = 𝐵)
51	1, 50	syl 14	. . . . . 6 ⊢ (𝜑 → ran 𝐹 = 𝐵)
52	51	sqxpeqd 4714	. . . . 5 ⊢ (𝜑 → (ran 𝐹 × ran 𝐹) = (𝐵 × 𝐵))
53	49, 52	sseqtrrd 3236	. . . 4 ⊢ (𝜑 → dom ∙ ⊆ (ran 𝐹 × ran 𝐹))
54	28	eleq2d 2276	. . . . . . . . . . . . 13 ⊢ (𝜑 → (⟨⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩, 𝑤⟩ ∈ ∙ ↔ ⟨⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩, 𝑤⟩ ∈ ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩}))
55	54	adantr 276	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → (⟨⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩, 𝑤⟩ ∈ ∙ ↔ ⟨⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩, 𝑤⟩ ∈ ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩}))
56		df-br 4055	. . . . . . . . . . . 12 ⊢ (⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩ ∙ 𝑤 ↔ ⟨⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩, 𝑤⟩ ∈ ∙ )
57		eliun 3940	. . . . . . . . . . . . 13 ⊢ (⟨⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩, 𝑤⟩ ∈ ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ↔ ∃𝑝 ∈ 𝑉 ⟨⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩, 𝑤⟩ ∈ ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩})
58		eliun 3940	. . . . . . . . . . . . . 14 ⊢ (⟨⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩, 𝑤⟩ ∈ ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ↔ ∃𝑞 ∈ 𝑉 ⟨⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩, 𝑤⟩ ∈ {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩})
59	58	rexbii 2514	. . . . . . . . . . . . 13 ⊢ (∃𝑝 ∈ 𝑉 ⟨⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩, 𝑤⟩ ∈ ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ↔ ∃𝑝 ∈ 𝑉 ∃𝑞 ∈ 𝑉 ⟨⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩, 𝑤⟩ ∈ {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩})
60	57, 59	bitr2i 185	. . . . . . . . . . . 12 ⊢ (∃𝑝 ∈ 𝑉 ∃𝑞 ∈ 𝑉 ⟨⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩, 𝑤⟩ ∈ {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ↔ ⟨⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩, 𝑤⟩ ∈ ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩})
61	55, 56, 60	3bitr4g 223	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → (⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩ ∙ 𝑤 ↔ ∃𝑝 ∈ 𝑉 ∃𝑞 ∈ 𝑉 ⟨⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩, 𝑤⟩ ∈ {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩}))
62		vex 2776	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑎 ∈ V
63		fvexg 5613	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐹 ∈ V ∧ 𝑎 ∈ V) → (𝐹‘𝑎) ∈ V)
64	5, 62, 63	sylancl 413	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐹‘𝑎) ∈ V)
65		vex 2776	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑏 ∈ V
66		fvexg 5613	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐹 ∈ V ∧ 𝑏 ∈ V) → (𝐹‘𝑏) ∈ V)
67	5, 65, 66	sylancl 413	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐹‘𝑏) ∈ V)
68		opexg 4285	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐹‘𝑎) ∈ V ∧ (𝐹‘𝑏) ∈ V) → ⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩ ∈ V)
69	64, 67, 68	syl2anc 411	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩ ∈ V)
70		vex 2776	. . . . . . . . . . . . . . . . 17 ⊢ 𝑤 ∈ V
71		opexg 4285	. . . . . . . . . . . . . . . . 17 ⊢ ((⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩ ∈ V ∧ 𝑤 ∈ V) → ⟨⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩, 𝑤⟩ ∈ V)
72	69, 70, 71	sylancl 413	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ⟨⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩, 𝑤⟩ ∈ V)
73		elsng 3653	. . . . . . . . . . . . . . . 16 ⊢ (⟨⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩, 𝑤⟩ ∈ V → (⟨⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩, 𝑤⟩ ∈ {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ↔ ⟨⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩, 𝑤⟩ = ⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩))
74	72, 73	syl 14	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (⟨⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩, 𝑤⟩ ∈ {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ↔ ⟨⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩, 𝑤⟩ = ⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩))
75	74	3ad2ant1 1021	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (⟨⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩, 𝑤⟩ ∈ {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ↔ ⟨⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩, 𝑤⟩ = ⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩))
76		opthg 4295	. . . . . . . . . . . . . . . . 17 ⊢ ((⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩ ∈ V ∧ 𝑤 ∈ V) → (⟨⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩, 𝑤⟩ = ⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩ ↔ (⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩ = ⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩ ∧ 𝑤 = (𝐹‘(𝑝 · 𝑞)))))
77	69, 70, 76	sylancl 413	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (⟨⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩, 𝑤⟩ = ⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩ ↔ (⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩ = ⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩ ∧ 𝑤 = (𝐹‘(𝑝 · 𝑞)))))
78	77	3ad2ant1 1021	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (⟨⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩, 𝑤⟩ = ⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩ ↔ (⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩ = ⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩ ∧ 𝑤 = (𝐹‘(𝑝 · 𝑞)))))
79		opthg 4295	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐹‘𝑎) ∈ V ∧ (𝐹‘𝑏) ∈ V) → (⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩ = ⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩ ↔ ((𝐹‘𝑎) = (𝐹‘𝑝) ∧ (𝐹‘𝑏) = (𝐹‘𝑞))))
80	64, 67, 79	syl2anc 411	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩ = ⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩ ↔ ((𝐹‘𝑎) = (𝐹‘𝑝) ∧ (𝐹‘𝑏) = (𝐹‘𝑞))))
81	80	3ad2ant1 1021	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩ = ⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩ ↔ ((𝐹‘𝑎) = (𝐹‘𝑝) ∧ (𝐹‘𝑏) = (𝐹‘𝑞))))
82		imasaddf.e	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (((𝐹‘𝑎) = (𝐹‘𝑝) ∧ (𝐹‘𝑏) = (𝐹‘𝑞)) → (𝐹‘(𝑎 · 𝑏)) = (𝐹‘(𝑝 · 𝑞))))
83	81, 82	sylbid 150	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩ = ⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩ → (𝐹‘(𝑎 · 𝑏)) = (𝐹‘(𝑝 · 𝑞))))
84		eqeq2 2216	. . . . . . . . . . . . . . . . . 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 1206	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (⟨⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩, 𝑤⟩ ∈ {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} → 𝑤 = (𝐹‘(𝑎 · 𝑏))))
91	90	rexlimdvva 2632	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → (∃𝑝 ∈ 𝑉 ∃𝑞 ∈ 𝑉 ⟨⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩, 𝑤⟩ ∈ {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} → 𝑤 = (𝐹‘(𝑎 · 𝑏))))
92	61, 91	sylbid 150	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → (⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩ ∙ 𝑤 → 𝑤 = (𝐹‘(𝑎 · 𝑏))))
93	92	alrimiv 1898	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → ∀𝑤(⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩ ∙ 𝑤 → 𝑤 = (𝐹‘(𝑎 · 𝑏))))
94		mo2icl 2956	. . . . . . . . 9 ⊢ (∀𝑤(⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩ ∙ 𝑤 → 𝑤 = (𝐹‘(𝑎 · 𝑏))) → ∃*𝑤⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩ ∙ 𝑤)
95	93, 94	syl 14	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → ∃*𝑤⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩ ∙ 𝑤)
96	95	ralrimivva 2589	. . . . . . 7 ⊢ (𝜑 → ∀𝑎 ∈ 𝑉 ∀𝑏 ∈ 𝑉 ∃*𝑤⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩ ∙ 𝑤)
97		fofn 5517	. . . . . . . . . 10 ⊢ (𝐹:𝑉–onto→𝐵 → 𝐹 Fn 𝑉)
98	1, 97	syl 14	. . . . . . . . 9 ⊢ (𝜑 → 𝐹 Fn 𝑉)
99		opeq2 3829	. . . . . . . . . . . 12 ⊢ (𝑧 = (𝐹‘𝑏) → ⟨(𝐹‘𝑎), 𝑧⟩ = ⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩)
100	99	breq1d 4064	. . . . . . . . . . 11 ⊢ (𝑧 = (𝐹‘𝑏) → (⟨(𝐹‘𝑎), 𝑧⟩ ∙ 𝑤 ↔ ⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩ ∙ 𝑤))
101	100	mobidv 2091	. . . . . . . . . 10 ⊢ (𝑧 = (𝐹‘𝑏) → (∃*𝑤⟨(𝐹‘𝑎), 𝑧⟩ ∙ 𝑤 ↔ ∃*𝑤⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩ ∙ 𝑤))
102	101	ralrn 5736	. . . . . . . . 9 ⊢ (𝐹 Fn 𝑉 → (∀𝑧 ∈ ran 𝐹∃*𝑤⟨(𝐹‘𝑎), 𝑧⟩ ∙ 𝑤 ↔ ∀𝑏 ∈ 𝑉 ∃*𝑤⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩ ∙ 𝑤))
103	98, 102	syl 14	. . . . . . . 8 ⊢ (𝜑 → (∀𝑧 ∈ ran 𝐹∃*𝑤⟨(𝐹‘𝑎), 𝑧⟩ ∙ 𝑤 ↔ ∀𝑏 ∈ 𝑉 ∃*𝑤⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩ ∙ 𝑤))
104	103	ralbidv 2507	. . . . . . 7 ⊢ (𝜑 → (∀𝑎 ∈ 𝑉 ∀𝑧 ∈ ran 𝐹∃*𝑤⟨(𝐹‘𝑎), 𝑧⟩ ∙ 𝑤 ↔ ∀𝑎 ∈ 𝑉 ∀𝑏 ∈ 𝑉 ∃*𝑤⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩ ∙ 𝑤))
105	96, 104	mpbird 167	. . . . . 6 ⊢ (𝜑 → ∀𝑎 ∈ 𝑉 ∀𝑧 ∈ ran 𝐹∃*𝑤⟨(𝐹‘𝑎), 𝑧⟩ ∙ 𝑤)
106		opeq1 3828	. . . . . . . . . . 11 ⊢ (𝑦 = (𝐹‘𝑎) → ⟨𝑦, 𝑧⟩ = ⟨(𝐹‘𝑎), 𝑧⟩)
107	106	breq1d 4064	. . . . . . . . . 10 ⊢ (𝑦 = (𝐹‘𝑎) → (⟨𝑦, 𝑧⟩ ∙ 𝑤 ↔ ⟨(𝐹‘𝑎), 𝑧⟩ ∙ 𝑤))
108	107	mobidv 2091	. . . . . . . . 9 ⊢ (𝑦 = (𝐹‘𝑎) → (∃*𝑤⟨𝑦, 𝑧⟩ ∙ 𝑤 ↔ ∃*𝑤⟨(𝐹‘𝑎), 𝑧⟩ ∙ 𝑤))
109	108	ralbidv 2507	. . . . . . . 8 ⊢ (𝑦 = (𝐹‘𝑎) → (∀𝑧 ∈ ran 𝐹∃*𝑤⟨𝑦, 𝑧⟩ ∙ 𝑤 ↔ ∀𝑧 ∈ ran 𝐹∃*𝑤⟨(𝐹‘𝑎), 𝑧⟩ ∙ 𝑤))
110	109	ralrn 5736	. . . . . . 7 ⊢ (𝐹 Fn 𝑉 → (∀𝑦 ∈ ran 𝐹∀𝑧 ∈ ran 𝐹∃*𝑤⟨𝑦, 𝑧⟩ ∙ 𝑤 ↔ ∀𝑎 ∈ 𝑉 ∀𝑧 ∈ ran 𝐹∃*𝑤⟨(𝐹‘𝑎), 𝑧⟩ ∙ 𝑤))
111	98, 110	syl 14	. . . . . 6 ⊢ (𝜑 → (∀𝑦 ∈ ran 𝐹∀𝑧 ∈ ran 𝐹∃*𝑤⟨𝑦, 𝑧⟩ ∙ 𝑤 ↔ ∀𝑎 ∈ 𝑉 ∀𝑧 ∈ ran 𝐹∃*𝑤⟨(𝐹‘𝑎), 𝑧⟩ ∙ 𝑤))
112	105, 111	mpbird 167	. . . . 5 ⊢ (𝜑 → ∀𝑦 ∈ ran 𝐹∀𝑧 ∈ ran 𝐹∃*𝑤⟨𝑦, 𝑧⟩ ∙ 𝑤)
113		breq1 4057	. . . . . . 7 ⊢ (𝑥 = ⟨𝑦, 𝑧⟩ → (𝑥 ∙ 𝑤 ↔ ⟨𝑦, 𝑧⟩ ∙ 𝑤))
114	113	mobidv 2091	. . . . . 6 ⊢ (𝑥 = ⟨𝑦, 𝑧⟩ → (∃*𝑤 𝑥 ∙ 𝑤 ↔ ∃*𝑤⟨𝑦, 𝑧⟩ ∙ 𝑤))
115	114	ralxp 4834	. . . . 5 ⊢ (∀𝑥 ∈ (ran 𝐹 × ran 𝐹)∃*𝑤 𝑥 ∙ 𝑤 ↔ ∀𝑦 ∈ ran 𝐹∀𝑧 ∈ ran 𝐹∃*𝑤⟨𝑦, 𝑧⟩ ∙ 𝑤)
116	112, 115	sylibr 134	. . . 4 ⊢ (𝜑 → ∀𝑥 ∈ (ran 𝐹 × ran 𝐹)∃*𝑤 𝑥 ∙ 𝑤)
117		ssralv 3261	. . . 4 ⊢ (dom ∙ ⊆ (ran 𝐹 × ran 𝐹) → (∀𝑥 ∈ (ran 𝐹 × ran 𝐹)∃*𝑤 𝑥 ∙ 𝑤 → ∀𝑥 ∈ dom ∙ ∃*𝑤 𝑥 ∙ 𝑤))
118	53, 116, 117	sylc 62	. . 3 ⊢ (𝜑 → ∀𝑥 ∈ dom ∙ ∃*𝑤 𝑥 ∙ 𝑤)
119		dffun7 5312	. . 3 ⊢ (Fun ∙ ↔ (Rel ∙ ∧ ∀𝑥 ∈ dom ∙ ∃*𝑤 𝑥 ∙ 𝑤))
120	30, 118, 119	sylanbrc 417	. 2 ⊢ (𝜑 → Fun ∙ )
121		eqimss2 3252	. . . . . . . . . . 11 ⊢ ( ∙ = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} → ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ ∙ )
122	28, 121	syl 14	. . . . . . . . . 10 ⊢ (𝜑 → ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ ∙ )
123		iunss 3977	. . . . . . . . . 10 ⊢ (∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ ∙ ↔ ∀𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ ∙ )
124	122, 123	sylib 122	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ ∙ )
125		iunss 3977	. . . . . . . . . . 11 ⊢ (∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ ∙ ↔ ∀𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ ∙ )
126		opexg 4285	. . . . . . . . . . . . . . 15 ⊢ ((⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩ ∈ V ∧ (𝐹‘(𝑝 · 𝑞)) ∈ V) → ⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩ ∈ V)
127	13, 19, 126	syl2anc 411	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩ ∈ V)
128		snssg 3773	. . . . . . . . . . . . . 14 ⊢ (⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩ ∈ V → (⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩ ∈ ∙ ↔ {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ ∙ ))
129	127, 128	syl 14	. . . . . . . . . . . . 13 ⊢ (𝜑 → (⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩ ∈ ∙ ↔ {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ ∙ ))
130		opeldmg 4897	. . . . . . . . . . . . . 14 ⊢ ((⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩ ∈ V ∧ (𝐹‘(𝑝 · 𝑞)) ∈ V) → (⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩ ∈ ∙ → ⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩ ∈ dom ∙ ))
131	13, 19, 130	syl2anc 411	. . . . . . . . . . . . 13 ⊢ (𝜑 → (⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩ ∈ ∙ → ⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩ ∈ dom ∙ ))
132	129, 131	sylbird 170	. . . . . . . . . . . 12 ⊢ (𝜑 → ({⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ ∙ → ⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩ ∈ dom ∙ ))
133	132	ralimdv 2575	. . . . . . . . . . 11 ⊢ (𝜑 → (∀𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ ∙ → ∀𝑞 ∈ 𝑉 ⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩ ∈ dom ∙ ))
134	125, 133	biimtrid 152	. . . . . . . . . 10 ⊢ (𝜑 → (∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ ∙ → ∀𝑞 ∈ 𝑉 ⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩ ∈ dom ∙ ))
135	134	ralimdv 2575	. . . . . . . . 9 ⊢ (𝜑 → (∀𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ ∙ → ∀𝑝 ∈ 𝑉 ∀𝑞 ∈ 𝑉 ⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩ ∈ dom ∙ ))
136	124, 135	mpd 13	. . . . . . . 8 ⊢ (𝜑 → ∀𝑝 ∈ 𝑉 ∀𝑞 ∈ 𝑉 ⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩ ∈ dom ∙ )
137		opeq2 3829	. . . . . . . . . . . 12 ⊢ (𝑧 = (𝐹‘𝑞) → ⟨(𝐹‘𝑝), 𝑧⟩ = ⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩)
138	137	eleq1d 2275	. . . . . . . . . . 11 ⊢ (𝑧 = (𝐹‘𝑞) → (⟨(𝐹‘𝑝), 𝑧⟩ ∈ dom ∙ ↔ ⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩ ∈ dom ∙ ))
139	138	ralrn 5736	. . . . . . . . . 10 ⊢ (𝐹 Fn 𝑉 → (∀𝑧 ∈ ran 𝐹⟨(𝐹‘𝑝), 𝑧⟩ ∈ dom ∙ ↔ ∀𝑞 ∈ 𝑉 ⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩ ∈ dom ∙ ))
140	98, 139	syl 14	. . . . . . . . 9 ⊢ (𝜑 → (∀𝑧 ∈ ran 𝐹⟨(𝐹‘𝑝), 𝑧⟩ ∈ dom ∙ ↔ ∀𝑞 ∈ 𝑉 ⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩ ∈ dom ∙ ))
141	140	ralbidv 2507	. . . . . . . 8 ⊢ (𝜑 → (∀𝑝 ∈ 𝑉 ∀𝑧 ∈ ran 𝐹⟨(𝐹‘𝑝), 𝑧⟩ ∈ dom ∙ ↔ ∀𝑝 ∈ 𝑉 ∀𝑞 ∈ 𝑉 ⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩ ∈ dom ∙ ))
142	136, 141	mpbird 167	. . . . . . 7 ⊢ (𝜑 → ∀𝑝 ∈ 𝑉 ∀𝑧 ∈ ran 𝐹⟨(𝐹‘𝑝), 𝑧⟩ ∈ dom ∙ )
143		opeq1 3828	. . . . . . . . . . 11 ⊢ (𝑦 = (𝐹‘𝑝) → ⟨𝑦, 𝑧⟩ = ⟨(𝐹‘𝑝), 𝑧⟩)
144	143	eleq1d 2275	. . . . . . . . . 10 ⊢ (𝑦 = (𝐹‘𝑝) → (⟨𝑦, 𝑧⟩ ∈ dom ∙ ↔ ⟨(𝐹‘𝑝), 𝑧⟩ ∈ dom ∙ ))
145	144	ralbidv 2507	. . . . . . . . 9 ⊢ (𝑦 = (𝐹‘𝑝) → (∀𝑧 ∈ ran 𝐹⟨𝑦, 𝑧⟩ ∈ dom ∙ ↔ ∀𝑧 ∈ ran 𝐹⟨(𝐹‘𝑝), 𝑧⟩ ∈ dom ∙ ))
146	145	ralrn 5736	. . . . . . . 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 2269	. . . . . . 7 ⊢ (𝑥 = ⟨𝑦, 𝑧⟩ → (𝑥 ∈ dom ∙ ↔ ⟨𝑦, 𝑧⟩ ∈ dom ∙ ))
150	149	ralxp 4834	. . . . . 6 ⊢ (∀𝑥 ∈ (ran 𝐹 × ran 𝐹)𝑥 ∈ dom ∙ ↔ ∀𝑦 ∈ ran 𝐹∀𝑧 ∈ ran 𝐹⟨𝑦, 𝑧⟩ ∈ dom ∙ )
151	148, 150	sylibr 134	. . . . 5 ⊢ (𝜑 → ∀𝑥 ∈ (ran 𝐹 × ran 𝐹)𝑥 ∈ dom ∙ )
152		dfss3 3186	. . . . 5 ⊢ ((ran 𝐹 × ran 𝐹) ⊆ dom ∙ ↔ ∀𝑥 ∈ (ran 𝐹 × ran 𝐹)𝑥 ∈ dom ∙ )
153	151, 152	sylibr 134	. . . 4 ⊢ (𝜑 → (ran 𝐹 × ran 𝐹) ⊆ dom ∙ )
154	52, 153	eqsstrrd 3234	. . 3 ⊢ (𝜑 → (𝐵 × 𝐵) ⊆ dom ∙ )
155	49, 154	eqssd 3214	. 2 ⊢ (𝜑 → dom ∙ = (𝐵 × 𝐵))
156		df-fn 5288	. 2 ⊢ ( ∙ Fn (𝐵 × 𝐵) ↔ (Fun ∙ ∧ dom ∙ = (𝐵 × 𝐵)))
157	120, 155, 156	sylanbrc 417	1 ⊢ (𝜑 → ∙ Fn (𝐵 × 𝐵))

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105   ∧ w3a 981  ∀wal 1371   = wceq 1373  ∃wex 1516  ∃*wmo 2056   ∈ wcel 2177  ∀wral 2485  ∃wrex 2486  Vcvv 2773   ⊆ wss 3170  {csn 3638  ⟨cop 3641  ∪ ciun 3936   class class class wbr 4054   × cxp 4686  dom cdm 4688  ran crn 4689  Rel wrel 4693  Fun wfun 5279   Fn wfn 5280  ⟶wf 5281  –onto→wfo 5283  ‘cfv 5285  (class class class)co 5962

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-13 2179  ax-14 2180  ax-ext 2188  ax-coll 4170  ax-sep 4173  ax-pow 4229  ax-pr 4264  ax-un 4493

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1485  df-sb 1787  df-eu 2058  df-mo 2059  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-ral 2490  df-rex 2491  df-reu 2492  df-rab 2494  df-v 2775  df-sbc 3003  df-csb 3098  df-un 3174  df-in 3176  df-ss 3183  df-pw 3623  df-sn 3644  df-pr 3645  df-op 3647  df-uni 3860  df-iun 3938  df-br 4055  df-opab 4117  df-mpt 4118  df-id 4353  df-xp 4694  df-rel 4695  df-cnv 4696  df-co 4697  df-dm 4698  df-rn 4699  df-res 4700  df-ima 4701  df-iota 5246  df-fun 5287  df-fn 5288  df-f 5289  df-f1 5290  df-fo 5291  df-f1o 5292  df-fv 5293  df-ov 5965

This theorem is referenced by:  imasaddvallemg  13232  imasaddflemg  13233  imasaddfn  13234  imasmulfn  13237