imasaddfnlem - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > imasaddfnlem		Structured version Visualization version GIF version

Theorem imasaddfnlem 17582

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 5446	. . . . . . . . 9 ⊢ ⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩ ∈ V
2		fvex 6895	. . . . . . . . 9 ⊢ (𝐹‘(𝑝 · 𝑞)) ∈ V
3	1, 2	relsnop 5793	. . . . . . . 8 ⊢ Rel {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩}
4	3	rgenw 3089	. . . . . . 7 ⊢ ∀𝑞 ∈ 𝑉 Rel {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩}
5		reliun 5804	. . . . . . 7 ⊢ (Rel ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ↔ ∀𝑞 ∈ 𝑉 Rel {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩})
6	4, 5	mpbir 234	. . . . . 6 ⊢ Rel ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩}
7	6	rgenw 3089	. . . . 5 ⊢ ∀𝑝 ∈ 𝑉 Rel ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩}
8		reliun 5804	. . . . 5 ⊢ (Rel ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ↔ ∀𝑝 ∈ 𝑉 Rel ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩})
9	7, 8	mpbir 234	. . . 4 ⊢ Rel ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩}
10		imasaddflem.a	. . . . 5 ⊢ (𝜑 → ∙ = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩})
11	10	releqd 5766	. . . 4 ⊢ (𝜑 → (Rel ∙ ↔ Rel ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩}))
12	9, 11	mpbiri 261	. . 3 ⊢ (𝜑 → Rel ∙ )
13		imasaddf.f	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐹:𝑉–onto→𝐵)
14		fof 6793	. . . . . . . . . . . . . . . 16 ⊢ (𝐹:𝑉–onto→𝐵 → 𝐹:𝑉⟶𝐵)
15	13, 14	syl 18	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐹:𝑉⟶𝐵)
16		ffvelcdm 7077	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹:𝑉⟶𝐵 ∧ 𝑝 ∈ 𝑉) → (𝐹‘𝑝) ∈ 𝐵)
17		ffvelcdm 7077	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹:𝑉⟶𝐵 ∧ 𝑞 ∈ 𝑉) → (𝐹‘𝑞) ∈ 𝐵)
18	16, 17	anim12dan 630	. . . . . . . . . . . . . . 15 ⊢ ((𝐹:𝑉⟶𝐵 ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → ((𝐹‘𝑝) ∈ 𝐵 ∧ (𝐹‘𝑞) ∈ 𝐵))
19	15, 18	sylan 591	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → ((𝐹‘𝑝) ∈ 𝐵 ∧ (𝐹‘𝑞) ∈ 𝐵))
20		opelxpi 5699	. . . . . . . . . . . . . 14 ⊢ (((𝐹‘𝑝) ∈ 𝐵 ∧ (𝐹‘𝑞) ∈ 𝐵) → ⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩ ∈ (𝐵 × 𝐵))
21	19, 20	syl 18	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → ⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩ ∈ (𝐵 × 𝐵))
22		opelxpi 5699	. . . . . . . . . . . . 13 ⊢ ((⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩ ∈ (𝐵 × 𝐵) ∧ (𝐹‘(𝑝 · 𝑞)) ∈ V) → ⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩ ∈ ((𝐵 × 𝐵) × V))
23	21, 2, 22	sylancl 597	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → ⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩ ∈ ((𝐵 × 𝐵) × V))
24	23	snssd 4757	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ ((𝐵 × 𝐵) × V))
25	24	anassrs 472	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑉) ∧ 𝑞 ∈ 𝑉) → {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ ((𝐵 × 𝐵) × V))
26	25	iunssd 5019	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑉) → ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ ((𝐵 × 𝐵) × V))
27	26	iunssd 5019	. . . . . . . 8 ⊢ (𝜑 → ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ ((𝐵 × 𝐵) × V))
28	10, 27	eqsstrd 3979	. . . . . . 7 ⊢ (𝜑 → ∙ ⊆ ((𝐵 × 𝐵) × V))
29		dmss 5893	. . . . . . 7 ⊢ ( ∙ ⊆ ((𝐵 × 𝐵) × V) → dom ∙ ⊆ dom ((𝐵 × 𝐵) × V))
30	28, 29	syl 18	. . . . . 6 ⊢ (𝜑 → dom ∙ ⊆ dom ((𝐵 × 𝐵) × V))
31		vn0 4306	. . . . . . 7 ⊢ V ≠ ∅
32		dmxp 5920	. . . . . . 7 ⊢ (V ≠ ∅ → dom ((𝐵 × 𝐵) × V) = (𝐵 × 𝐵))
33	31, 32	ax-mp 5	. . . . . 6 ⊢ dom ((𝐵 × 𝐵) × V) = (𝐵 × 𝐵)
34	30, 33	sseqtrdi 3985	. . . . 5 ⊢ (𝜑 → dom ∙ ⊆ (𝐵 × 𝐵))
35		forn 6796	. . . . . . 7 ⊢ (𝐹:𝑉–onto→𝐵 → ran 𝐹 = 𝐵)
36	13, 35	syl 18	. . . . . 6 ⊢ (𝜑 → ran 𝐹 = 𝐵)
37	36	sqxpeqd 5694	. . . . 5 ⊢ (𝜑 → (ran 𝐹 × ran 𝐹) = (𝐵 × 𝐵))
38	34, 37	sseqtrrd 3982	. . . 4 ⊢ (𝜑 → dom ∙ ⊆ (ran 𝐹 × ran 𝐹))
39	10	eleq2d 2855	. . . . . . . . . . . . 13 ⊢ (𝜑 → (⟨⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩, 𝑤⟩ ∈ ∙ ↔ ⟨⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩, 𝑤⟩ ∈ ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩}))
40	39	adantr 485	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → (⟨⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩, 𝑤⟩ ∈ ∙ ↔ ⟨⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩, 𝑤⟩ ∈ ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩}))
41		df-br 5114	. . . . . . . . . . . 12 ⊢ (⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩ ∙ 𝑤 ↔ ⟨⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩, 𝑤⟩ ∈ ∙ )
42		eliun 4964	. . . . . . . . . . . . 13 ⊢ (⟨⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩, 𝑤⟩ ∈ ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ↔ ∃𝑝 ∈ 𝑉 ⟨⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩, 𝑤⟩ ∈ ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩})
43		eliun 4964	. . . . . . . . . . . . . 14 ⊢ (⟨⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩, 𝑤⟩ ∈ ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ↔ ∃𝑞 ∈ 𝑉 ⟨⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩, 𝑤⟩ ∈ {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩})
44	43	rexbii 3118	. . . . . . . . . . . . 13 ⊢ (∃𝑝 ∈ 𝑉 ⟨⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩, 𝑤⟩ ∈ ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ↔ ∃𝑝 ∈ 𝑉 ∃𝑞 ∈ 𝑉 ⟨⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩, 𝑤⟩ ∈ {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩})
45	42, 44	bitr2i 279	. . . . . . . . . . . 12 ⊢ (∃𝑝 ∈ 𝑉 ∃𝑞 ∈ 𝑉 ⟨⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩, 𝑤⟩ ∈ {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ↔ ⟨⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩, 𝑤⟩ ∈ ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩})
46	40, 41, 45	3bitr4g 317	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → (⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩ ∙ 𝑤 ↔ ∃𝑝 ∈ 𝑉 ∃𝑞 ∈ 𝑉 ⟨⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩, 𝑤⟩ ∈ {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩}))
47		opex 5446	. . . . . . . . . . . . . . 15 ⊢ ⟨⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩, 𝑤⟩ ∈ V
48	47	elsn 4609	. . . . . . . . . . . . . 14 ⊢ (⟨⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩, 𝑤⟩ ∈ {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ↔ ⟨⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩, 𝑤⟩ = ⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩)
49		opex 5446	. . . . . . . . . . . . . . . 16 ⊢ ⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩ ∈ V
50		vex 3467	. . . . . . . . . . . . . . . 16 ⊢ 𝑤 ∈ V
51	49, 50	opth 5459	. . . . . . . . . . . . . . 15 ⊢ (⟨⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩, 𝑤⟩ = ⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩ ↔ (⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩ = ⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩ ∧ 𝑤 = (𝐹‘(𝑝 · 𝑞))))
52		fvex 6895	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐹‘𝑎) ∈ V
53		fvex 6895	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐹‘𝑏) ∈ V
54	52, 53	opth 5459	. . . . . . . . . . . . . . . . . 18 ⊢ (⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩ = ⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩ ↔ ((𝐹‘𝑎) = (𝐹‘𝑝) ∧ (𝐹‘𝑏) = (𝐹‘𝑞)))
55		imasaddf.e	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (((𝐹‘𝑎) = (𝐹‘𝑝) ∧ (𝐹‘𝑏) = (𝐹‘𝑞)) → (𝐹‘(𝑎 · 𝑏)) = (𝐹‘(𝑝 · 𝑞))))
56	54, 55	biimtrid 245	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩ = ⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩ → (𝐹‘(𝑎 · 𝑏)) = (𝐹‘(𝑝 · 𝑞))))
57		eqeq2 2781	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹‘(𝑎 · 𝑏)) = (𝐹‘(𝑝 · 𝑞)) → (𝑤 = (𝐹‘(𝑎 · 𝑏)) ↔ 𝑤 = (𝐹‘(𝑝 · 𝑞))))
58	57	biimprd 251	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹‘(𝑎 · 𝑏)) = (𝐹‘(𝑝 · 𝑞)) → (𝑤 = (𝐹‘(𝑝 · 𝑞)) → 𝑤 = (𝐹‘(𝑎 · 𝑏))))
59	56, 58	syl6 36	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩ = ⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩ → (𝑤 = (𝐹‘(𝑝 · 𝑞)) → 𝑤 = (𝐹‘(𝑎 · 𝑏)))))
60	59	impd 415	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → ((⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩ = ⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩ ∧ 𝑤 = (𝐹‘(𝑝 · 𝑞))) → 𝑤 = (𝐹‘(𝑎 · 𝑏))))
61	51, 60	biimtrid 245	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (⟨⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩, 𝑤⟩ = ⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩ → 𝑤 = (𝐹‘(𝑎 · 𝑏))))
62	48, 61	biimtrid 245	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (⟨⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩, 𝑤⟩ ∈ {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} → 𝑤 = (𝐹‘(𝑎 · 𝑏))))
63	62	3expa 1134	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (⟨⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩, 𝑤⟩ ∈ {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} → 𝑤 = (𝐹‘(𝑎 · 𝑏))))
64	63	rexlimdvva 3228	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → (∃𝑝 ∈ 𝑉 ∃𝑞 ∈ 𝑉 ⟨⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩, 𝑤⟩ ∈ {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} → 𝑤 = (𝐹‘(𝑎 · 𝑏))))
65	46, 64	sylbid 243	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → (⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩ ∙ 𝑤 → 𝑤 = (𝐹‘(𝑎 · 𝑏))))
66	65	alrimiv 1954	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → ∀𝑤(⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩ ∙ 𝑤 → 𝑤 = (𝐹‘(𝑎 · 𝑏))))
67		mo2icl 3686	. . . . . . . . 9 ⊢ (∀𝑤(⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩ ∙ 𝑤 → 𝑤 = (𝐹‘(𝑎 · 𝑏))) → ∃*𝑤⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩ ∙ 𝑤)
68	66, 67	syl 18	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → ∃*𝑤⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩ ∙ 𝑤)
69	68	ralrimivva 3214	. . . . . . 7 ⊢ (𝜑 → ∀𝑎 ∈ 𝑉 ∀𝑏 ∈ 𝑉 ∃*𝑤⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩ ∙ 𝑤)
70		fofn 6795	. . . . . . . . . 10 ⊢ (𝐹:𝑉–onto→𝐵 → 𝐹 Fn 𝑉)
71	13, 70	syl 18	. . . . . . . . 9 ⊢ (𝜑 → 𝐹 Fn 𝑉)
72		opeq2 4843	. . . . . . . . . . . 12 ⊢ (𝑧 = (𝐹‘𝑏) → ⟨(𝐹‘𝑎), 𝑧⟩ = ⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩)
73	72	breq1d 5123	. . . . . . . . . . 11 ⊢ (𝑧 = (𝐹‘𝑏) → (⟨(𝐹‘𝑎), 𝑧⟩ ∙ 𝑤 ↔ ⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩ ∙ 𝑤))
74	73	mobidv 2583	. . . . . . . . . 10 ⊢ (𝑧 = (𝐹‘𝑏) → (∃𝑤⟨(𝐹‘𝑎), 𝑧⟩ ∙ 𝑤 ↔ ∃𝑤⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩ ∙ 𝑤))
75	74	ralrn 7084	. . . . . . . . 9 ⊢ (𝐹 Fn 𝑉 → (∀𝑧 ∈ ran 𝐹∃𝑤⟨(𝐹‘𝑎), 𝑧⟩ ∙ 𝑤 ↔ ∀𝑏 ∈ 𝑉 ∃𝑤⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩ ∙ 𝑤))
76	71, 75	syl 18	. . . . . . . 8 ⊢ (𝜑 → (∀𝑧 ∈ ran 𝐹∃𝑤⟨(𝐹‘𝑎), 𝑧⟩ ∙ 𝑤 ↔ ∀𝑏 ∈ 𝑉 ∃𝑤⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩ ∙ 𝑤))
77	76	ralbidv 3194	. . . . . . 7 ⊢ (𝜑 → (∀𝑎 ∈ 𝑉 ∀𝑧 ∈ ran 𝐹∃𝑤⟨(𝐹‘𝑎), 𝑧⟩ ∙ 𝑤 ↔ ∀𝑎 ∈ 𝑉 ∀𝑏 ∈ 𝑉 ∃𝑤⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩ ∙ 𝑤))
78	69, 77	mpbird 260	. . . . . 6 ⊢ (𝜑 → ∀𝑎 ∈ 𝑉 ∀𝑧 ∈ ran 𝐹∃*𝑤⟨(𝐹‘𝑎), 𝑧⟩ ∙ 𝑤)
79		opeq1 4842	. . . . . . . . . . 11 ⊢ (𝑦 = (𝐹‘𝑎) → ⟨𝑦, 𝑧⟩ = ⟨(𝐹‘𝑎), 𝑧⟩)
80	79	breq1d 5123	. . . . . . . . . 10 ⊢ (𝑦 = (𝐹‘𝑎) → (⟨𝑦, 𝑧⟩ ∙ 𝑤 ↔ ⟨(𝐹‘𝑎), 𝑧⟩ ∙ 𝑤))
81	80	mobidv 2583	. . . . . . . . 9 ⊢ (𝑦 = (𝐹‘𝑎) → (∃𝑤⟨𝑦, 𝑧⟩ ∙ 𝑤 ↔ ∃𝑤⟨(𝐹‘𝑎), 𝑧⟩ ∙ 𝑤))
82	81	ralbidv 3194	. . . . . . . 8 ⊢ (𝑦 = (𝐹‘𝑎) → (∀𝑧 ∈ ran 𝐹∃𝑤⟨𝑦, 𝑧⟩ ∙ 𝑤 ↔ ∀𝑧 ∈ ran 𝐹∃𝑤⟨(𝐹‘𝑎), 𝑧⟩ ∙ 𝑤))
83	82	ralrn 7084	. . . . . . 7 ⊢ (𝐹 Fn 𝑉 → (∀𝑦 ∈ ran 𝐹∀𝑧 ∈ ran 𝐹∃𝑤⟨𝑦, 𝑧⟩ ∙ 𝑤 ↔ ∀𝑎 ∈ 𝑉 ∀𝑧 ∈ ran 𝐹∃𝑤⟨(𝐹‘𝑎), 𝑧⟩ ∙ 𝑤))
84	71, 83	syl 18	. . . . . 6 ⊢ (𝜑 → (∀𝑦 ∈ ran 𝐹∀𝑧 ∈ ran 𝐹∃𝑤⟨𝑦, 𝑧⟩ ∙ 𝑤 ↔ ∀𝑎 ∈ 𝑉 ∀𝑧 ∈ ran 𝐹∃𝑤⟨(𝐹‘𝑎), 𝑧⟩ ∙ 𝑤))
85	78, 84	mpbird 260	. . . . 5 ⊢ (𝜑 → ∀𝑦 ∈ ran 𝐹∀𝑧 ∈ ran 𝐹∃*𝑤⟨𝑦, 𝑧⟩ ∙ 𝑤)
86		breq1 5116	. . . . . . 7 ⊢ (𝑥 = ⟨𝑦, 𝑧⟩ → (𝑥 ∙ 𝑤 ↔ ⟨𝑦, 𝑧⟩ ∙ 𝑤))
87	86	mobidv 2583	. . . . . 6 ⊢ (𝑥 = ⟨𝑦, 𝑧⟩ → (∃𝑤 𝑥 ∙ 𝑤 ↔ ∃𝑤⟨𝑦, 𝑧⟩ ∙ 𝑤))
88	87	ralxp 5828	. . . . 5 ⊢ (∀𝑥 ∈ (ran 𝐹 × ran 𝐹)∃𝑤 𝑥 ∙ 𝑤 ↔ ∀𝑦 ∈ ran 𝐹∀𝑧 ∈ ran 𝐹∃𝑤⟨𝑦, 𝑧⟩ ∙ 𝑤)
89	85, 88	sylibr 237	. . . 4 ⊢ (𝜑 → ∀𝑥 ∈ (ran 𝐹 × ran 𝐹)∃*𝑤 𝑥 ∙ 𝑤)
90		ssralv 4014	. . . 4 ⊢ (dom ∙ ⊆ (ran 𝐹 × ran 𝐹) → (∀𝑥 ∈ (ran 𝐹 × ran 𝐹)∃𝑤 𝑥 ∙ 𝑤 → ∀𝑥 ∈ dom ∙ ∃𝑤 𝑥 ∙ 𝑤))
91	38, 89, 90	sylc 66	. . 3 ⊢ (𝜑 → ∀𝑥 ∈ dom ∙ ∃*𝑤 𝑥 ∙ 𝑤)
92		dffun7 6564	. . 3 ⊢ (Fun ∙ ↔ (Rel ∙ ∧ ∀𝑥 ∈ dom ∙ ∃*𝑤 𝑥 ∙ 𝑤))
93	12, 91, 92	sylanbrc 594	. 2 ⊢ (𝜑 → Fun ∙ )
94		eqimss2 4004	. . . . . . . . . . 11 ⊢ ( ∙ = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} → ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ ∙ )
95	10, 94	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ ∙ )
96		iunss 5013	. . . . . . . . . 10 ⊢ (∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ ∙ ↔ ∀𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ ∙ )
97	95, 96	sylib 221	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ ∙ )
98		iunss 5013	. . . . . . . . . . 11 ⊢ (∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ ∙ ↔ ∀𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ ∙ )
99		opex 5446	. . . . . . . . . . . . . 14 ⊢ ⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩ ∈ V
100	99	snss 4755	. . . . . . . . . . . . 13 ⊢ (⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩ ∈ ∙ ↔ {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ ∙ )
101	1, 2	opeldm 5898	. . . . . . . . . . . . 13 ⊢ (⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩ ∈ ∙ → ⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩ ∈ dom ∙ )
102	100, 101	sylbir 238	. . . . . . . . . . . 12 ⊢ ({⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ ∙ → ⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩ ∈ dom ∙ )
103	102	ralimi 3108	. . . . . . . . . . 11 ⊢ (∀𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ ∙ → ∀𝑞 ∈ 𝑉 ⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩ ∈ dom ∙ )
104	98, 103	sylbi 220	. . . . . . . . . 10 ⊢ (∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ ∙ → ∀𝑞 ∈ 𝑉 ⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩ ∈ dom ∙ )
105	104	ralimi 3108	. . . . . . . . 9 ⊢ (∀𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ ∙ → ∀𝑝 ∈ 𝑉 ∀𝑞 ∈ 𝑉 ⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩ ∈ dom ∙ )
106	97, 105	syl 18	. . . . . . . 8 ⊢ (𝜑 → ∀𝑝 ∈ 𝑉 ∀𝑞 ∈ 𝑉 ⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩ ∈ dom ∙ )
107		opeq2 4843	. . . . . . . . . . . 12 ⊢ (𝑧 = (𝐹‘𝑞) → ⟨(𝐹‘𝑝), 𝑧⟩ = ⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩)
108	107	eleq1d 2854	. . . . . . . . . . 11 ⊢ (𝑧 = (𝐹‘𝑞) → (⟨(𝐹‘𝑝), 𝑧⟩ ∈ dom ∙ ↔ ⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩ ∈ dom ∙ ))
109	108	ralrn 7084	. . . . . . . . . 10 ⊢ (𝐹 Fn 𝑉 → (∀𝑧 ∈ ran 𝐹⟨(𝐹‘𝑝), 𝑧⟩ ∈ dom ∙ ↔ ∀𝑞 ∈ 𝑉 ⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩ ∈ dom ∙ ))
110	71, 109	syl 18	. . . . . . . . 9 ⊢ (𝜑 → (∀𝑧 ∈ ran 𝐹⟨(𝐹‘𝑝), 𝑧⟩ ∈ dom ∙ ↔ ∀𝑞 ∈ 𝑉 ⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩ ∈ dom ∙ ))
111	110	ralbidv 3194	. . . . . . . 8 ⊢ (𝜑 → (∀𝑝 ∈ 𝑉 ∀𝑧 ∈ ran 𝐹⟨(𝐹‘𝑝), 𝑧⟩ ∈ dom ∙ ↔ ∀𝑝 ∈ 𝑉 ∀𝑞 ∈ 𝑉 ⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩ ∈ dom ∙ ))
112	106, 111	mpbird 260	. . . . . . 7 ⊢ (𝜑 → ∀𝑝 ∈ 𝑉 ∀𝑧 ∈ ran 𝐹⟨(𝐹‘𝑝), 𝑧⟩ ∈ dom ∙ )
113		opeq1 4842	. . . . . . . . . . 11 ⊢ (𝑦 = (𝐹‘𝑝) → ⟨𝑦, 𝑧⟩ = ⟨(𝐹‘𝑝), 𝑧⟩)
114	113	eleq1d 2854	. . . . . . . . . 10 ⊢ (𝑦 = (𝐹‘𝑝) → (⟨𝑦, 𝑧⟩ ∈ dom ∙ ↔ ⟨(𝐹‘𝑝), 𝑧⟩ ∈ dom ∙ ))
115	114	ralbidv 3194	. . . . . . . . 9 ⊢ (𝑦 = (𝐹‘𝑝) → (∀𝑧 ∈ ran 𝐹⟨𝑦, 𝑧⟩ ∈ dom ∙ ↔ ∀𝑧 ∈ ran 𝐹⟨(𝐹‘𝑝), 𝑧⟩ ∈ dom ∙ ))
116	115	ralrn 7084	. . . . . . . 8 ⊢ (𝐹 Fn 𝑉 → (∀𝑦 ∈ ran 𝐹∀𝑧 ∈ ran 𝐹⟨𝑦, 𝑧⟩ ∈ dom ∙ ↔ ∀𝑝 ∈ 𝑉 ∀𝑧 ∈ ran 𝐹⟨(𝐹‘𝑝), 𝑧⟩ ∈ dom ∙ ))
117	71, 116	syl 18	. . . . . . 7 ⊢ (𝜑 → (∀𝑦 ∈ ran 𝐹∀𝑧 ∈ ran 𝐹⟨𝑦, 𝑧⟩ ∈ dom ∙ ↔ ∀𝑝 ∈ 𝑉 ∀𝑧 ∈ ran 𝐹⟨(𝐹‘𝑝), 𝑧⟩ ∈ dom ∙ ))
118	112, 117	mpbird 260	. . . . . 6 ⊢ (𝜑 → ∀𝑦 ∈ ran 𝐹∀𝑧 ∈ ran 𝐹⟨𝑦, 𝑧⟩ ∈ dom ∙ )
119		eleq1 2857	. . . . . . 7 ⊢ (𝑥 = ⟨𝑦, 𝑧⟩ → (𝑥 ∈ dom ∙ ↔ ⟨𝑦, 𝑧⟩ ∈ dom ∙ ))
120	119	ralxp 5828	. . . . . 6 ⊢ (∀𝑥 ∈ (ran 𝐹 × ran 𝐹)𝑥 ∈ dom ∙ ↔ ∀𝑦 ∈ ran 𝐹∀𝑧 ∈ ran 𝐹⟨𝑦, 𝑧⟩ ∈ dom ∙ )
121	118, 120	sylibr 237	. . . . 5 ⊢ (𝜑 → ∀𝑥 ∈ (ran 𝐹 × ran 𝐹)𝑥 ∈ dom ∙ )
122		dfss3 3934	. . . . 5 ⊢ ((ran 𝐹 × ran 𝐹) ⊆ dom ∙ ↔ ∀𝑥 ∈ (ran 𝐹 × ran 𝐹)𝑥 ∈ dom ∙ )
123	121, 122	sylibr 237	. . . 4 ⊢ (𝜑 → (ran 𝐹 × ran 𝐹) ⊆ dom ∙ )
124	37, 123	eqsstrrd 3980	. . 3 ⊢ (𝜑 → (𝐵 × 𝐵) ⊆ dom ∙ )
125	34, 124	eqssd 3962	. 2 ⊢ (𝜑 → dom ∙ = (𝐵 × 𝐵))
126		df-fn 6540	. 2 ⊢ ( ∙ Fn (𝐵 × 𝐵) ↔ (Fun ∙ ∧ dom ∙ = (𝐵 × 𝐵)))
127	93, 125, 126	sylanbrc 594	1 ⊢ (𝜑 → ∙ Fn (𝐵 × 𝐵))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 209 ∧ wa 400 ∧ w3a 1101 ∀wal 1565 = wceq 1567 ∈ wcel 2149 ∃*wmo 2571 ≠ wne 2964 ∀wral 3085 ∃wrex 3095 Vcvv 3463 ⊆ wss 3913 ∅c0 4294 {csn 4594 ⟨cop 4600 ∪ ciun 4960 class class class wbr 5113 × cxp 5660 dom cdm 5662 ran crn 5663 Rel wrel 5667 Fun wfun 6531 Fn wfn 6532 ⟶wf 6533 –onto→wfo 6535 ‘cfv 6537 (class class class)co 7411

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1822 ax-4 1836 ax-5 1937 ax-6 1994 ax-7 2035 ax-8 2151 ax-9 2159 ax-10 2182 ax-11 2198 ax-12 2219 ax-ext 2741 ax-sep 5261 ax-nul 5271 ax-pr 5405

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3an 1103 df-tru 1570 df-fal 1580 df-ex 1807 df-nf 1811 df-sb 2098 df-mo 2573 df-eu 2603 df-clab 2748 df-cleq 2761 df-clel 2844 df-nfc 2918 df-ne 2965 df-ral 3086 df-rex 3096 df-rab 3424 df-v 3465 df-sbc 3754 df-csb 3862 df-dif 3916 df-un 3918 df-in 3920 df-ss 3930 df-nul 4295 df-if 4493 df-sn 4595 df-pr 4597 df-op 4601 df-uni 4877 df-iun 4962 df-br 5114 df-opab 5178 df-mpt 5197 df-id 5557 df-xp 5668 df-rel 5669 df-cnv 5670 df-co 5671 df-dm 5672 df-rn 5673 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-fo 6543 df-fv 6545

This theorem is referenced by: imasaddvallem 17583 imasaddflem 17584 imasaddfn 17585 imasmulfn 17588

W3C validator