Theorem imasaddfnlem 17479

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	⊢ (𝜑 → ∙ = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩})

Assertion

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

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

Allowed substitution hints:   𝐵(𝑎,𝑏)   · (𝑎,𝑏)

Proof of Theorem imasaddfnlem

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

Step	Hyp	Ref	Expression
1		opex 5465	. . . . . . . . 9 ⊢ ⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩ ∈ V
2		fvex 6905	. . . . . . . . 9 ⊢ (𝐹‘(𝑝 · 𝑞)) ∈ V
3	1, 2	relsnop 5806	. . . . . . . 8 ⊢ Rel {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩}
4	3	rgenw 3064	. . . . . . 7 ⊢ ∀𝑞 ∈ 𝑉 Rel {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩}
5		reliun 5817	. . . . . . 7 ⊢ (Rel ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ↔ ∀𝑞 ∈ 𝑉 Rel {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩})
6	4, 5	mpbir 230	. . . . . 6 ⊢ Rel ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩}
7	6	rgenw 3064	. . . . 5 ⊢ ∀𝑝 ∈ 𝑉 Rel ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩}
8		reliun 5817	. . . . 5 ⊢ (Rel ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ↔ ∀𝑝 ∈ 𝑉 Rel ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩})
9	7, 8	mpbir 230	. . . 4 ⊢ Rel ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩}
10		imasaddflem.a	. . . . 5 ⊢ (𝜑 → ∙ = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩})
11	10	releqd 5779	. . . 4 ⊢ (𝜑 → (Rel ∙ ↔ Rel ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩}))
12	9, 11	mpbiri 257	. . 3 ⊢ (𝜑 → Rel ∙ )
13		imasaddf.f	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐹:𝑉–onto→𝐵)
14		fof 6806	. . . . . . . . . . . . . . . 16 ⊢ (𝐹:𝑉–onto→𝐵 → 𝐹:𝑉⟶𝐵)
15	13, 14	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐹:𝑉⟶𝐵)
16		ffvelcdm 7084	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹:𝑉⟶𝐵 ∧ 𝑝 ∈ 𝑉) → (𝐹‘𝑝) ∈ 𝐵)
17		ffvelcdm 7084	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹:𝑉⟶𝐵 ∧ 𝑞 ∈ 𝑉) → (𝐹‘𝑞) ∈ 𝐵)
18	16, 17	anim12dan 618	. . . . . . . . . . . . . . 15 ⊢ ((𝐹:𝑉⟶𝐵 ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → ((𝐹‘𝑝) ∈ 𝐵 ∧ (𝐹‘𝑞) ∈ 𝐵))
19	15, 18	sylan 579	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → ((𝐹‘𝑝) ∈ 𝐵 ∧ (𝐹‘𝑞) ∈ 𝐵))
20		opelxpi 5714	. . . . . . . . . . . . . 14 ⊢ (((𝐹‘𝑝) ∈ 𝐵 ∧ (𝐹‘𝑞) ∈ 𝐵) → ⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩ ∈ (𝐵 × 𝐵))
21	19, 20	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → ⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩ ∈ (𝐵 × 𝐵))
22		opelxpi 5714	. . . . . . . . . . . . 13 ⊢ ((⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩ ∈ (𝐵 × 𝐵) ∧ (𝐹‘(𝑝 · 𝑞)) ∈ V) → ⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩ ∈ ((𝐵 × 𝐵) × V))
23	21, 2, 22	sylancl 585	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → ⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩ ∈ ((𝐵 × 𝐵) × V))
24	23	snssd 4813	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ ((𝐵 × 𝐵) × V))
25	24	anassrs 467	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑉) ∧ 𝑞 ∈ 𝑉) → {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ ((𝐵 × 𝐵) × V))
26	25	iunssd 5054	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑉) → ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ ((𝐵 × 𝐵) × V))
27	26	iunssd 5054	. . . . . . . 8 ⊢ (𝜑 → ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ ((𝐵 × 𝐵) × V))
28	10, 27	eqsstrd 4021	. . . . . . 7 ⊢ (𝜑 → ∙ ⊆ ((𝐵 × 𝐵) × V))
29		dmss 5903	. . . . . . 7 ⊢ ( ∙ ⊆ ((𝐵 × 𝐵) × V) → dom ∙ ⊆ dom ((𝐵 × 𝐵) × V))
30	28, 29	syl 17	. . . . . 6 ⊢ (𝜑 → dom ∙ ⊆ dom ((𝐵 × 𝐵) × V))
31		vn0 4339	. . . . . . 7 ⊢ V ≠ ∅
32		dmxp 5929	. . . . . . 7 ⊢ (V ≠ ∅ → dom ((𝐵 × 𝐵) × V) = (𝐵 × 𝐵))
33	31, 32	ax-mp 5	. . . . . 6 ⊢ dom ((𝐵 × 𝐵) × V) = (𝐵 × 𝐵)
34	30, 33	sseqtrdi 4033	. . . . 5 ⊢ (𝜑 → dom ∙ ⊆ (𝐵 × 𝐵))
35		forn 6809	. . . . . . 7 ⊢ (𝐹:𝑉–onto→𝐵 → ran 𝐹 = 𝐵)
36	13, 35	syl 17	. . . . . 6 ⊢ (𝜑 → ran 𝐹 = 𝐵)
37	36	sqxpeqd 5709	. . . . 5 ⊢ (𝜑 → (ran 𝐹 × ran 𝐹) = (𝐵 × 𝐵))
38	34, 37	sseqtrrd 4024	. . . 4 ⊢ (𝜑 → dom ∙ ⊆ (ran 𝐹 × ran 𝐹))
39	10	eleq2d 2818	. . . . . . . . . . . . 13 ⊢ (𝜑 → (⟨⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩, 𝑤⟩ ∈ ∙ ↔ ⟨⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩, 𝑤⟩ ∈ ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩}))
40	39	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → (⟨⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩, 𝑤⟩ ∈ ∙ ↔ ⟨⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩, 𝑤⟩ ∈ ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩}))
41		df-br 5150	. . . . . . . . . . . 12 ⊢ (⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩ ∙ 𝑤 ↔ ⟨⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩, 𝑤⟩ ∈ ∙ )
42		eliun 5002	. . . . . . . . . . . . 13 ⊢ (⟨⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩, 𝑤⟩ ∈ ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ↔ ∃𝑝 ∈ 𝑉 ⟨⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩, 𝑤⟩ ∈ ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩})
43		eliun 5002	. . . . . . . . . . . . . 14 ⊢ (⟨⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩, 𝑤⟩ ∈ ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ↔ ∃𝑞 ∈ 𝑉 ⟨⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩, 𝑤⟩ ∈ {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩})
44	43	rexbii 3093	. . . . . . . . . . . . 13 ⊢ (∃𝑝 ∈ 𝑉 ⟨⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩, 𝑤⟩ ∈ ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ↔ ∃𝑝 ∈ 𝑉 ∃𝑞 ∈ 𝑉 ⟨⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩, 𝑤⟩ ∈ {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩})
45	42, 44	bitr2i 275	. . . . . . . . . . . 12 ⊢ (∃𝑝 ∈ 𝑉 ∃𝑞 ∈ 𝑉 ⟨⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩, 𝑤⟩ ∈ {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ↔ ⟨⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩, 𝑤⟩ ∈ ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩})
46	40, 41, 45	3bitr4g 313	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → (⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩ ∙ 𝑤 ↔ ∃𝑝 ∈ 𝑉 ∃𝑞 ∈ 𝑉 ⟨⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩, 𝑤⟩ ∈ {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩}))
47		opex 5465	. . . . . . . . . . . . . . 15 ⊢ ⟨⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩, 𝑤⟩ ∈ V
48	47	elsn 4644	. . . . . . . . . . . . . 14 ⊢ (⟨⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩, 𝑤⟩ ∈ {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ↔ ⟨⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩, 𝑤⟩ = ⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩)
49		opex 5465	. . . . . . . . . . . . . . . 16 ⊢ ⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩ ∈ V
50		vex 3477	. . . . . . . . . . . . . . . 16 ⊢ 𝑤 ∈ V
51	49, 50	opth 5477	. . . . . . . . . . . . . . 15 ⊢ (⟨⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩, 𝑤⟩ = ⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩ ↔ (⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩ = ⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩ ∧ 𝑤 = (𝐹‘(𝑝 · 𝑞))))
52		fvex 6905	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐹‘𝑎) ∈ V
53		fvex 6905	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐹‘𝑏) ∈ V
54	52, 53	opth 5477	. . . . . . . . . . . . . . . . . 18 ⊢ (⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩ = ⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩ ↔ ((𝐹‘𝑎) = (𝐹‘𝑝) ∧ (𝐹‘𝑏) = (𝐹‘𝑞)))
55		imasaddf.e	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (((𝐹‘𝑎) = (𝐹‘𝑝) ∧ (𝐹‘𝑏) = (𝐹‘𝑞)) → (𝐹‘(𝑎 · 𝑏)) = (𝐹‘(𝑝 · 𝑞))))
56	54, 55	biimtrid 241	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩ = ⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩ → (𝐹‘(𝑎 · 𝑏)) = (𝐹‘(𝑝 · 𝑞))))
57		eqeq2 2743	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹‘(𝑎 · 𝑏)) = (𝐹‘(𝑝 · 𝑞)) → (𝑤 = (𝐹‘(𝑎 · 𝑏)) ↔ 𝑤 = (𝐹‘(𝑝 · 𝑞))))
58	57	biimprd 247	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹‘(𝑎 · 𝑏)) = (𝐹‘(𝑝 · 𝑞)) → (𝑤 = (𝐹‘(𝑝 · 𝑞)) → 𝑤 = (𝐹‘(𝑎 · 𝑏))))
59	56, 58	syl6 35	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩ = ⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩ → (𝑤 = (𝐹‘(𝑝 · 𝑞)) → 𝑤 = (𝐹‘(𝑎 · 𝑏)))))
60	59	impd 410	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → ((⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩ = ⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩ ∧ 𝑤 = (𝐹‘(𝑝 · 𝑞))) → 𝑤 = (𝐹‘(𝑎 · 𝑏))))
61	51, 60	biimtrid 241	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (⟨⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩, 𝑤⟩ = ⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩ → 𝑤 = (𝐹‘(𝑎 · 𝑏))))
62	48, 61	biimtrid 241	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (⟨⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩, 𝑤⟩ ∈ {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} → 𝑤 = (𝐹‘(𝑎 · 𝑏))))
63	62	3expa 1117	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (⟨⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩, 𝑤⟩ ∈ {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} → 𝑤 = (𝐹‘(𝑎 · 𝑏))))
64	63	rexlimdvva 3210	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → (∃𝑝 ∈ 𝑉 ∃𝑞 ∈ 𝑉 ⟨⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩, 𝑤⟩ ∈ {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} → 𝑤 = (𝐹‘(𝑎 · 𝑏))))
65	46, 64	sylbid 239	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → (⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩ ∙ 𝑤 → 𝑤 = (𝐹‘(𝑎 · 𝑏))))
66	65	alrimiv 1929	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → ∀𝑤(⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩ ∙ 𝑤 → 𝑤 = (𝐹‘(𝑎 · 𝑏))))
67		mo2icl 3711	. . . . . . . . 9 ⊢ (∀𝑤(⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩ ∙ 𝑤 → 𝑤 = (𝐹‘(𝑎 · 𝑏))) → ∃*𝑤⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩ ∙ 𝑤)
68	66, 67	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → ∃*𝑤⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩ ∙ 𝑤)
69	68	ralrimivva 3199	. . . . . . 7 ⊢ (𝜑 → ∀𝑎 ∈ 𝑉 ∀𝑏 ∈ 𝑉 ∃*𝑤⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩ ∙ 𝑤)
70		fofn 6808	. . . . . . . . . 10 ⊢ (𝐹:𝑉–onto→𝐵 → 𝐹 Fn 𝑉)
71	13, 70	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝐹 Fn 𝑉)
72		opeq2 4875	. . . . . . . . . . . 12 ⊢ (𝑧 = (𝐹‘𝑏) → ⟨(𝐹‘𝑎), 𝑧⟩ = ⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩)
73	72	breq1d 5159	. . . . . . . . . . 11 ⊢ (𝑧 = (𝐹‘𝑏) → (⟨(𝐹‘𝑎), 𝑧⟩ ∙ 𝑤 ↔ ⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩ ∙ 𝑤))
74	73	mobidv 2542	. . . . . . . . . 10 ⊢ (𝑧 = (𝐹‘𝑏) → (∃*𝑤⟨(𝐹‘𝑎), 𝑧⟩ ∙ 𝑤 ↔ ∃*𝑤⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩ ∙ 𝑤))
75	74	ralrn 7090	. . . . . . . . 9 ⊢ (𝐹 Fn 𝑉 → (∀𝑧 ∈ ran 𝐹∃*𝑤⟨(𝐹‘𝑎), 𝑧⟩ ∙ 𝑤 ↔ ∀𝑏 ∈ 𝑉 ∃*𝑤⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩ ∙ 𝑤))
76	71, 75	syl 17	. . . . . . . 8 ⊢ (𝜑 → (∀𝑧 ∈ ran 𝐹∃*𝑤⟨(𝐹‘𝑎), 𝑧⟩ ∙ 𝑤 ↔ ∀𝑏 ∈ 𝑉 ∃*𝑤⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩ ∙ 𝑤))
77	76	ralbidv 3176	. . . . . . 7 ⊢ (𝜑 → (∀𝑎 ∈ 𝑉 ∀𝑧 ∈ ran 𝐹∃*𝑤⟨(𝐹‘𝑎), 𝑧⟩ ∙ 𝑤 ↔ ∀𝑎 ∈ 𝑉 ∀𝑏 ∈ 𝑉 ∃*𝑤⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩ ∙ 𝑤))
78	69, 77	mpbird 256	. . . . . 6 ⊢ (𝜑 → ∀𝑎 ∈ 𝑉 ∀𝑧 ∈ ran 𝐹∃*𝑤⟨(𝐹‘𝑎), 𝑧⟩ ∙ 𝑤)
79		opeq1 4874	. . . . . . . . . . 11 ⊢ (𝑦 = (𝐹‘𝑎) → ⟨𝑦, 𝑧⟩ = ⟨(𝐹‘𝑎), 𝑧⟩)
80	79	breq1d 5159	. . . . . . . . . 10 ⊢ (𝑦 = (𝐹‘𝑎) → (⟨𝑦, 𝑧⟩ ∙ 𝑤 ↔ ⟨(𝐹‘𝑎), 𝑧⟩ ∙ 𝑤))
81	80	mobidv 2542	. . . . . . . . 9 ⊢ (𝑦 = (𝐹‘𝑎) → (∃*𝑤⟨𝑦, 𝑧⟩ ∙ 𝑤 ↔ ∃*𝑤⟨(𝐹‘𝑎), 𝑧⟩ ∙ 𝑤))
82	81	ralbidv 3176	. . . . . . . 8 ⊢ (𝑦 = (𝐹‘𝑎) → (∀𝑧 ∈ ran 𝐹∃*𝑤⟨𝑦, 𝑧⟩ ∙ 𝑤 ↔ ∀𝑧 ∈ ran 𝐹∃*𝑤⟨(𝐹‘𝑎), 𝑧⟩ ∙ 𝑤))
83	82	ralrn 7090	. . . . . . 7 ⊢ (𝐹 Fn 𝑉 → (∀𝑦 ∈ ran 𝐹∀𝑧 ∈ ran 𝐹∃*𝑤⟨𝑦, 𝑧⟩ ∙ 𝑤 ↔ ∀𝑎 ∈ 𝑉 ∀𝑧 ∈ ran 𝐹∃*𝑤⟨(𝐹‘𝑎), 𝑧⟩ ∙ 𝑤))
84	71, 83	syl 17	. . . . . 6 ⊢ (𝜑 → (∀𝑦 ∈ ran 𝐹∀𝑧 ∈ ran 𝐹∃*𝑤⟨𝑦, 𝑧⟩ ∙ 𝑤 ↔ ∀𝑎 ∈ 𝑉 ∀𝑧 ∈ ran 𝐹∃*𝑤⟨(𝐹‘𝑎), 𝑧⟩ ∙ 𝑤))
85	78, 84	mpbird 256	. . . . 5 ⊢ (𝜑 → ∀𝑦 ∈ ran 𝐹∀𝑧 ∈ ran 𝐹∃*𝑤⟨𝑦, 𝑧⟩ ∙ 𝑤)
86		breq1 5152	. . . . . . 7 ⊢ (𝑥 = ⟨𝑦, 𝑧⟩ → (𝑥 ∙ 𝑤 ↔ ⟨𝑦, 𝑧⟩ ∙ 𝑤))
87	86	mobidv 2542	. . . . . 6 ⊢ (𝑥 = ⟨𝑦, 𝑧⟩ → (∃*𝑤 𝑥 ∙ 𝑤 ↔ ∃*𝑤⟨𝑦, 𝑧⟩ ∙ 𝑤))
88	87	ralxp 5842	. . . . 5 ⊢ (∀𝑥 ∈ (ran 𝐹 × ran 𝐹)∃*𝑤 𝑥 ∙ 𝑤 ↔ ∀𝑦 ∈ ran 𝐹∀𝑧 ∈ ran 𝐹∃*𝑤⟨𝑦, 𝑧⟩ ∙ 𝑤)
89	85, 88	sylibr 233	. . . 4 ⊢ (𝜑 → ∀𝑥 ∈ (ran 𝐹 × ran 𝐹)∃*𝑤 𝑥 ∙ 𝑤)
90		ssralv 4051	. . . 4 ⊢ (dom ∙ ⊆ (ran 𝐹 × ran 𝐹) → (∀𝑥 ∈ (ran 𝐹 × ran 𝐹)∃*𝑤 𝑥 ∙ 𝑤 → ∀𝑥 ∈ dom ∙ ∃*𝑤 𝑥 ∙ 𝑤))
91	38, 89, 90	sylc 65	. . 3 ⊢ (𝜑 → ∀𝑥 ∈ dom ∙ ∃*𝑤 𝑥 ∙ 𝑤)
92		dffun7 6576	. . 3 ⊢ (Fun ∙ ↔ (Rel ∙ ∧ ∀𝑥 ∈ dom ∙ ∃*𝑤 𝑥 ∙ 𝑤))
93	12, 91, 92	sylanbrc 582	. 2 ⊢ (𝜑 → Fun ∙ )
94		eqimss2 4042	. . . . . . . . . . 11 ⊢ ( ∙ = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} → ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ ∙ )
95	10, 94	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ ∙ )
96		iunss 5049	. . . . . . . . . 10 ⊢ (∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ ∙ ↔ ∀𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ ∙ )
97	95, 96	sylib 217	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ ∙ )
98		iunss 5049	. . . . . . . . . . 11 ⊢ (∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ ∙ ↔ ∀𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ ∙ )
99		opex 5465	. . . . . . . . . . . . . 14 ⊢ ⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩ ∈ V
100	99	snss 4790	. . . . . . . . . . . . 13 ⊢ (⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩ ∈ ∙ ↔ {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ ∙ )
101	1, 2	opeldm 5908	. . . . . . . . . . . . 13 ⊢ (⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩ ∈ ∙ → ⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩ ∈ dom ∙ )
102	100, 101	sylbir 234	. . . . . . . . . . . 12 ⊢ ({⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ ∙ → ⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩ ∈ dom ∙ )
103	102	ralimi 3082	. . . . . . . . . . 11 ⊢ (∀𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ ∙ → ∀𝑞 ∈ 𝑉 ⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩ ∈ dom ∙ )
104	98, 103	sylbi 216	. . . . . . . . . 10 ⊢ (∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ ∙ → ∀𝑞 ∈ 𝑉 ⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩ ∈ dom ∙ )
105	104	ralimi 3082	. . . . . . . . 9 ⊢ (∀𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ ∙ → ∀𝑝 ∈ 𝑉 ∀𝑞 ∈ 𝑉 ⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩ ∈ dom ∙ )
106	97, 105	syl 17	. . . . . . . 8 ⊢ (𝜑 → ∀𝑝 ∈ 𝑉 ∀𝑞 ∈ 𝑉 ⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩ ∈ dom ∙ )
107		opeq2 4875	. . . . . . . . . . . 12 ⊢ (𝑧 = (𝐹‘𝑞) → ⟨(𝐹‘𝑝), 𝑧⟩ = ⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩)
108	107	eleq1d 2817	. . . . . . . . . . 11 ⊢ (𝑧 = (𝐹‘𝑞) → (⟨(𝐹‘𝑝), 𝑧⟩ ∈ dom ∙ ↔ ⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩ ∈ dom ∙ ))
109	108	ralrn 7090	. . . . . . . . . 10 ⊢ (𝐹 Fn 𝑉 → (∀𝑧 ∈ ran 𝐹⟨(𝐹‘𝑝), 𝑧⟩ ∈ dom ∙ ↔ ∀𝑞 ∈ 𝑉 ⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩ ∈ dom ∙ ))
110	71, 109	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (∀𝑧 ∈ ran 𝐹⟨(𝐹‘𝑝), 𝑧⟩ ∈ dom ∙ ↔ ∀𝑞 ∈ 𝑉 ⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩ ∈ dom ∙ ))
111	110	ralbidv 3176	. . . . . . . 8 ⊢ (𝜑 → (∀𝑝 ∈ 𝑉 ∀𝑧 ∈ ran 𝐹⟨(𝐹‘𝑝), 𝑧⟩ ∈ dom ∙ ↔ ∀𝑝 ∈ 𝑉 ∀𝑞 ∈ 𝑉 ⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩ ∈ dom ∙ ))
112	106, 111	mpbird 256	. . . . . . 7 ⊢ (𝜑 → ∀𝑝 ∈ 𝑉 ∀𝑧 ∈ ran 𝐹⟨(𝐹‘𝑝), 𝑧⟩ ∈ dom ∙ )
113		opeq1 4874	. . . . . . . . . . 11 ⊢ (𝑦 = (𝐹‘𝑝) → ⟨𝑦, 𝑧⟩ = ⟨(𝐹‘𝑝), 𝑧⟩)
114	113	eleq1d 2817	. . . . . . . . . 10 ⊢ (𝑦 = (𝐹‘𝑝) → (⟨𝑦, 𝑧⟩ ∈ dom ∙ ↔ ⟨(𝐹‘𝑝), 𝑧⟩ ∈ dom ∙ ))
115	114	ralbidv 3176	. . . . . . . . 9 ⊢ (𝑦 = (𝐹‘𝑝) → (∀𝑧 ∈ ran 𝐹⟨𝑦, 𝑧⟩ ∈ dom ∙ ↔ ∀𝑧 ∈ ran 𝐹⟨(𝐹‘𝑝), 𝑧⟩ ∈ dom ∙ ))
116	115	ralrn 7090	. . . . . . . 8 ⊢ (𝐹 Fn 𝑉 → (∀𝑦 ∈ ran 𝐹∀𝑧 ∈ ran 𝐹⟨𝑦, 𝑧⟩ ∈ dom ∙ ↔ ∀𝑝 ∈ 𝑉 ∀𝑧 ∈ ran 𝐹⟨(𝐹‘𝑝), 𝑧⟩ ∈ dom ∙ ))
117	71, 116	syl 17	. . . . . . 7 ⊢ (𝜑 → (∀𝑦 ∈ ran 𝐹∀𝑧 ∈ ran 𝐹⟨𝑦, 𝑧⟩ ∈ dom ∙ ↔ ∀𝑝 ∈ 𝑉 ∀𝑧 ∈ ran 𝐹⟨(𝐹‘𝑝), 𝑧⟩ ∈ dom ∙ ))
118	112, 117	mpbird 256	. . . . . 6 ⊢ (𝜑 → ∀𝑦 ∈ ran 𝐹∀𝑧 ∈ ran 𝐹⟨𝑦, 𝑧⟩ ∈ dom ∙ )
119		eleq1 2820	. . . . . . 7 ⊢ (𝑥 = ⟨𝑦, 𝑧⟩ → (𝑥 ∈ dom ∙ ↔ ⟨𝑦, 𝑧⟩ ∈ dom ∙ ))
120	119	ralxp 5842	. . . . . 6 ⊢ (∀𝑥 ∈ (ran 𝐹 × ran 𝐹)𝑥 ∈ dom ∙ ↔ ∀𝑦 ∈ ran 𝐹∀𝑧 ∈ ran 𝐹⟨𝑦, 𝑧⟩ ∈ dom ∙ )
121	118, 120	sylibr 233	. . . . 5 ⊢ (𝜑 → ∀𝑥 ∈ (ran 𝐹 × ran 𝐹)𝑥 ∈ dom ∙ )
122		dfss3 3971	. . . . 5 ⊢ ((ran 𝐹 × ran 𝐹) ⊆ dom ∙ ↔ ∀𝑥 ∈ (ran 𝐹 × ran 𝐹)𝑥 ∈ dom ∙ )
123	121, 122	sylibr 233	. . . 4 ⊢ (𝜑 → (ran 𝐹 × ran 𝐹) ⊆ dom ∙ )
124	37, 123	eqsstrrd 4022	. . 3 ⊢ (𝜑 → (𝐵 × 𝐵) ⊆ dom ∙ )
125	34, 124	eqssd 4000	. 2 ⊢ (𝜑 → dom ∙ = (𝐵 × 𝐵))
126		df-fn 6547	. 2 ⊢ ( ∙ Fn (𝐵 × 𝐵) ↔ (Fun ∙ ∧ dom ∙ = (𝐵 × 𝐵)))
127	93, 125, 126	sylanbrc 582	1 ⊢ (𝜑 → ∙ Fn (𝐵 × 𝐵))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   ∧ w3a 1086  ∀wal 1538   = wceq 1540   ∈ wcel 2105  ∃*wmo 2531   ≠ wne 2939  ∀wral 3060  ∃wrex 3069  Vcvv 3473   ⊆ wss 3949  ∅c0 4323  {csn 4629  ⟨cop 4635  ∪ ciun 4998   class class class wbr 5149   × cxp 5675  dom cdm 5677  ran crn 5678  Rel wrel 5682  Fun wfun 6538   Fn wfn 6539  ⟶wf 6540  –onto→wfo 6542  ‘cfv 6544  (class class class)co 7412

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2702  ax-sep 5300  ax-nul 5307  ax-pr 5428

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-ral 3061  df-rex 3070  df-rab 3432  df-v 3475  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-iun 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5575  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-fo 6550  df-fv 6552

This theorem is referenced by:  imasaddvallem  17480  imasaddflem  17481  imasaddfn  17482  imasmulfn  17485