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 16188

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 4932	. . . . . . . . 9 ⊢ ⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩ ∈ V
2		fvex 6201	. . . . . . . . 9 ⊢ (𝐹‘(𝑝 · 𝑞)) ∈ V
3	1, 2	relsnop 5224	. . . . . . . 8 ⊢ Rel {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩}
4	3	rgenw 2924	. . . . . . 7 ⊢ ∀𝑞 ∈ 𝑉 Rel {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩}
5		reliun 5239	. . . . . . 7 ⊢ (Rel ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ↔ ∀𝑞 ∈ 𝑉 Rel {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩})
6	4, 5	mpbir 221	. . . . . 6 ⊢ Rel ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩}
7	6	rgenw 2924	. . . . 5 ⊢ ∀𝑝 ∈ 𝑉 Rel ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩}
8		reliun 5239	. . . . 5 ⊢ (Rel ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ↔ ∀𝑝 ∈ 𝑉 Rel ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩})
9	7, 8	mpbir 221	. . . 4 ⊢ Rel ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩}
10		imasaddflem.a	. . . . 5 ⊢ (𝜑 → ∙ = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩})
11	10	releqd 5203	. . . 4 ⊢ (𝜑 → (Rel ∙ ↔ Rel ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩}))
12	9, 11	mpbiri 248	. . 3 ⊢ (𝜑 → Rel ∙ )
13		imasaddf.f	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐹:𝑉–onto→𝐵)
14		fof 6115	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐹:𝑉–onto→𝐵 → 𝐹:𝑉⟶𝐵)
15	13, 14	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐹:𝑉⟶𝐵)
16		ffvelrn 6357	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹:𝑉⟶𝐵 ∧ 𝑝 ∈ 𝑉) → (𝐹‘𝑝) ∈ 𝐵)
17		ffvelrn 6357	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹:𝑉⟶𝐵 ∧ 𝑞 ∈ 𝑉) → (𝐹‘𝑞) ∈ 𝐵)
18	16, 17	anim12dan 882	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹:𝑉⟶𝐵 ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → ((𝐹‘𝑝) ∈ 𝐵 ∧ (𝐹‘𝑞) ∈ 𝐵))
19	15, 18	sylan 488	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → ((𝐹‘𝑝) ∈ 𝐵 ∧ (𝐹‘𝑞) ∈ 𝐵))
20		opelxpi 5148	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹‘𝑝) ∈ 𝐵 ∧ (𝐹‘𝑞) ∈ 𝐵) → ⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩ ∈ (𝐵 × 𝐵))
21	19, 20	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → ⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩ ∈ (𝐵 × 𝐵))
22		opelxpi 5148	. . . . . . . . . . . . . . 15 ⊢ ((⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩ ∈ (𝐵 × 𝐵) ∧ (𝐹‘(𝑝 · 𝑞)) ∈ V) → ⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩ ∈ ((𝐵 × 𝐵) × V))
23	21, 2, 22	sylancl 694	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → ⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩ ∈ ((𝐵 × 𝐵) × V))
24	23	snssd 4340	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ ((𝐵 × 𝐵) × V))
25	24	anassrs 680	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑉) ∧ 𝑞 ∈ 𝑉) → {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ ((𝐵 × 𝐵) × V))
26	25	ralrimiva 2966	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑉) → ∀𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ ((𝐵 × 𝐵) × V))
27		iunss 4561	. . . . . . . . . . 11 ⊢ (∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ ((𝐵 × 𝐵) × V) ↔ ∀𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ ((𝐵 × 𝐵) × V))
28	26, 27	sylibr 224	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑉) → ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ ((𝐵 × 𝐵) × V))
29	28	ralrimiva 2966	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ ((𝐵 × 𝐵) × V))
30		iunss 4561	. . . . . . . . 9 ⊢ (∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ ((𝐵 × 𝐵) × V) ↔ ∀𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ ((𝐵 × 𝐵) × V))
31	29, 30	sylibr 224	. . . . . . . 8 ⊢ (𝜑 → ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ ((𝐵 × 𝐵) × V))
32	10, 31	eqsstrd 3639	. . . . . . 7 ⊢ (𝜑 → ∙ ⊆ ((𝐵 × 𝐵) × V))
33		dmss 5323	. . . . . . 7 ⊢ ( ∙ ⊆ ((𝐵 × 𝐵) × V) → dom ∙ ⊆ dom ((𝐵 × 𝐵) × V))
34	32, 33	syl 17	. . . . . 6 ⊢ (𝜑 → dom ∙ ⊆ dom ((𝐵 × 𝐵) × V))
35		vn0 3924	. . . . . . 7 ⊢ V ≠ ∅
36		dmxp 5344	. . . . . . 7 ⊢ (V ≠ ∅ → dom ((𝐵 × 𝐵) × V) = (𝐵 × 𝐵))
37	35, 36	ax-mp 5	. . . . . 6 ⊢ dom ((𝐵 × 𝐵) × V) = (𝐵 × 𝐵)
38	34, 37	syl6sseq 3651	. . . . 5 ⊢ (𝜑 → dom ∙ ⊆ (𝐵 × 𝐵))
39		forn 6118	. . . . . . 7 ⊢ (𝐹:𝑉–onto→𝐵 → ran 𝐹 = 𝐵)
40	13, 39	syl 17	. . . . . 6 ⊢ (𝜑 → ran 𝐹 = 𝐵)
41	40	sqxpeqd 5141	. . . . 5 ⊢ (𝜑 → (ran 𝐹 × ran 𝐹) = (𝐵 × 𝐵))
42	38, 41	sseqtr4d 3642	. . . 4 ⊢ (𝜑 → dom ∙ ⊆ (ran 𝐹 × ran 𝐹))
43	10	eleq2d 2687	. . . . . . . . . . . . 13 ⊢ (𝜑 → (⟨⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩, 𝑤⟩ ∈ ∙ ↔ ⟨⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩, 𝑤⟩ ∈ ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩}))
44	43	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → (⟨⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩, 𝑤⟩ ∈ ∙ ↔ ⟨⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩, 𝑤⟩ ∈ ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩}))
45		df-br 4654	. . . . . . . . . . . 12 ⊢ (⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩ ∙ 𝑤 ↔ ⟨⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩, 𝑤⟩ ∈ ∙ )
46		eliun 4524	. . . . . . . . . . . . 13 ⊢ (⟨⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩, 𝑤⟩ ∈ ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ↔ ∃𝑝 ∈ 𝑉 ⟨⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩, 𝑤⟩ ∈ ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩})
47		eliun 4524	. . . . . . . . . . . . . 14 ⊢ (⟨⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩, 𝑤⟩ ∈ ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ↔ ∃𝑞 ∈ 𝑉 ⟨⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩, 𝑤⟩ ∈ {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩})
48	47	rexbii 3041	. . . . . . . . . . . . 13 ⊢ (∃𝑝 ∈ 𝑉 ⟨⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩, 𝑤⟩ ∈ ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ↔ ∃𝑝 ∈ 𝑉 ∃𝑞 ∈ 𝑉 ⟨⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩, 𝑤⟩ ∈ {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩})
49	46, 48	bitr2i 265	. . . . . . . . . . . 12 ⊢ (∃𝑝 ∈ 𝑉 ∃𝑞 ∈ 𝑉 ⟨⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩, 𝑤⟩ ∈ {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ↔ ⟨⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩, 𝑤⟩ ∈ ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩})
50	44, 45, 49	3bitr4g 303	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → (⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩ ∙ 𝑤 ↔ ∃𝑝 ∈ 𝑉 ∃𝑞 ∈ 𝑉 ⟨⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩, 𝑤⟩ ∈ {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩}))
51		opex 4932	. . . . . . . . . . . . . . 15 ⊢ ⟨⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩, 𝑤⟩ ∈ V
52	51	elsn 4192	. . . . . . . . . . . . . 14 ⊢ (⟨⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩, 𝑤⟩ ∈ {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ↔ ⟨⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩, 𝑤⟩ = ⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩)
53		opex 4932	. . . . . . . . . . . . . . . 16 ⊢ ⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩ ∈ V
54		vex 3203	. . . . . . . . . . . . . . . 16 ⊢ 𝑤 ∈ V
55	53, 54	opth 4945	. . . . . . . . . . . . . . 15 ⊢ (⟨⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩, 𝑤⟩ = ⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩ ↔ (⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩ = ⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩ ∧ 𝑤 = (𝐹‘(𝑝 · 𝑞))))
56		fvex 6201	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐹‘𝑎) ∈ V
57		fvex 6201	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐹‘𝑏) ∈ V
58	56, 57	opth 4945	. . . . . . . . . . . . . . . . . 18 ⊢ (⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩ = ⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩ ↔ ((𝐹‘𝑎) = (𝐹‘𝑝) ∧ (𝐹‘𝑏) = (𝐹‘𝑞)))
59		imasaddf.e	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (((𝐹‘𝑎) = (𝐹‘𝑝) ∧ (𝐹‘𝑏) = (𝐹‘𝑞)) → (𝐹‘(𝑎 · 𝑏)) = (𝐹‘(𝑝 · 𝑞))))
60	58, 59	syl5bi 232	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩ = ⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩ → (𝐹‘(𝑎 · 𝑏)) = (𝐹‘(𝑝 · 𝑞))))
61		eqeq2 2633	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹‘(𝑎 · 𝑏)) = (𝐹‘(𝑝 · 𝑞)) → (𝑤 = (𝐹‘(𝑎 · 𝑏)) ↔ 𝑤 = (𝐹‘(𝑝 · 𝑞))))
62	61	biimprd 238	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹‘(𝑎 · 𝑏)) = (𝐹‘(𝑝 · 𝑞)) → (𝑤 = (𝐹‘(𝑝 · 𝑞)) → 𝑤 = (𝐹‘(𝑎 · 𝑏))))
63	60, 62	syl6 35	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩ = ⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩ → (𝑤 = (𝐹‘(𝑝 · 𝑞)) → 𝑤 = (𝐹‘(𝑎 · 𝑏)))))
64	63	impd 447	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → ((⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩ = ⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩ ∧ 𝑤 = (𝐹‘(𝑝 · 𝑞))) → 𝑤 = (𝐹‘(𝑎 · 𝑏))))
65	55, 64	syl5bi 232	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (⟨⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩, 𝑤⟩ = ⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩ → 𝑤 = (𝐹‘(𝑎 · 𝑏))))
66	52, 65	syl5bi 232	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (⟨⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩, 𝑤⟩ ∈ {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} → 𝑤 = (𝐹‘(𝑎 · 𝑏))))
67	66	3expa 1265	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (⟨⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩, 𝑤⟩ ∈ {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} → 𝑤 = (𝐹‘(𝑎 · 𝑏))))
68	67	rexlimdvva 3038	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → (∃𝑝 ∈ 𝑉 ∃𝑞 ∈ 𝑉 ⟨⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩, 𝑤⟩ ∈ {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} → 𝑤 = (𝐹‘(𝑎 · 𝑏))))
69	50, 68	sylbid 230	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → (⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩ ∙ 𝑤 → 𝑤 = (𝐹‘(𝑎 · 𝑏))))
70	69	alrimiv 1855	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → ∀𝑤(⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩ ∙ 𝑤 → 𝑤 = (𝐹‘(𝑎 · 𝑏))))
71		mo2icl 3385	. . . . . . . . 9 ⊢ (∀𝑤(⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩ ∙ 𝑤 → 𝑤 = (𝐹‘(𝑎 · 𝑏))) → ∃*𝑤⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩ ∙ 𝑤)
72	70, 71	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → ∃*𝑤⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩ ∙ 𝑤)
73	72	ralrimivva 2971	. . . . . . 7 ⊢ (𝜑 → ∀𝑎 ∈ 𝑉 ∀𝑏 ∈ 𝑉 ∃*𝑤⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩ ∙ 𝑤)
74		fofn 6117	. . . . . . . . . 10 ⊢ (𝐹:𝑉–onto→𝐵 → 𝐹 Fn 𝑉)
75	13, 74	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝐹 Fn 𝑉)
76		opeq2 4403	. . . . . . . . . . . 12 ⊢ (𝑧 = (𝐹‘𝑏) → ⟨(𝐹‘𝑎), 𝑧⟩ = ⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩)
77	76	breq1d 4663	. . . . . . . . . . 11 ⊢ (𝑧 = (𝐹‘𝑏) → (⟨(𝐹‘𝑎), 𝑧⟩ ∙ 𝑤 ↔ ⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩ ∙ 𝑤))
78	77	mobidv 2491	. . . . . . . . . 10 ⊢ (𝑧 = (𝐹‘𝑏) → (∃𝑤⟨(𝐹‘𝑎), 𝑧⟩ ∙ 𝑤 ↔ ∃𝑤⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩ ∙ 𝑤))
79	78	ralrn 6362	. . . . . . . . 9 ⊢ (𝐹 Fn 𝑉 → (∀𝑧 ∈ ran 𝐹∃𝑤⟨(𝐹‘𝑎), 𝑧⟩ ∙ 𝑤 ↔ ∀𝑏 ∈ 𝑉 ∃𝑤⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩ ∙ 𝑤))
80	75, 79	syl 17	. . . . . . . 8 ⊢ (𝜑 → (∀𝑧 ∈ ran 𝐹∃𝑤⟨(𝐹‘𝑎), 𝑧⟩ ∙ 𝑤 ↔ ∀𝑏 ∈ 𝑉 ∃𝑤⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩ ∙ 𝑤))
81	80	ralbidv 2986	. . . . . . 7 ⊢ (𝜑 → (∀𝑎 ∈ 𝑉 ∀𝑧 ∈ ran 𝐹∃𝑤⟨(𝐹‘𝑎), 𝑧⟩ ∙ 𝑤 ↔ ∀𝑎 ∈ 𝑉 ∀𝑏 ∈ 𝑉 ∃𝑤⟨(𝐹‘𝑎), (𝐹‘𝑏)⟩ ∙ 𝑤))
82	73, 81	mpbird 247	. . . . . 6 ⊢ (𝜑 → ∀𝑎 ∈ 𝑉 ∀𝑧 ∈ ran 𝐹∃*𝑤⟨(𝐹‘𝑎), 𝑧⟩ ∙ 𝑤)
83		opeq1 4402	. . . . . . . . . . 11 ⊢ (𝑦 = (𝐹‘𝑎) → ⟨𝑦, 𝑧⟩ = ⟨(𝐹‘𝑎), 𝑧⟩)
84	83	breq1d 4663	. . . . . . . . . 10 ⊢ (𝑦 = (𝐹‘𝑎) → (⟨𝑦, 𝑧⟩ ∙ 𝑤 ↔ ⟨(𝐹‘𝑎), 𝑧⟩ ∙ 𝑤))
85	84	mobidv 2491	. . . . . . . . 9 ⊢ (𝑦 = (𝐹‘𝑎) → (∃𝑤⟨𝑦, 𝑧⟩ ∙ 𝑤 ↔ ∃𝑤⟨(𝐹‘𝑎), 𝑧⟩ ∙ 𝑤))
86	85	ralbidv 2986	. . . . . . . 8 ⊢ (𝑦 = (𝐹‘𝑎) → (∀𝑧 ∈ ran 𝐹∃𝑤⟨𝑦, 𝑧⟩ ∙ 𝑤 ↔ ∀𝑧 ∈ ran 𝐹∃𝑤⟨(𝐹‘𝑎), 𝑧⟩ ∙ 𝑤))
87	86	ralrn 6362	. . . . . . 7 ⊢ (𝐹 Fn 𝑉 → (∀𝑦 ∈ ran 𝐹∀𝑧 ∈ ran 𝐹∃𝑤⟨𝑦, 𝑧⟩ ∙ 𝑤 ↔ ∀𝑎 ∈ 𝑉 ∀𝑧 ∈ ran 𝐹∃𝑤⟨(𝐹‘𝑎), 𝑧⟩ ∙ 𝑤))
88	75, 87	syl 17	. . . . . 6 ⊢ (𝜑 → (∀𝑦 ∈ ran 𝐹∀𝑧 ∈ ran 𝐹∃𝑤⟨𝑦, 𝑧⟩ ∙ 𝑤 ↔ ∀𝑎 ∈ 𝑉 ∀𝑧 ∈ ran 𝐹∃𝑤⟨(𝐹‘𝑎), 𝑧⟩ ∙ 𝑤))
89	82, 88	mpbird 247	. . . . 5 ⊢ (𝜑 → ∀𝑦 ∈ ran 𝐹∀𝑧 ∈ ran 𝐹∃*𝑤⟨𝑦, 𝑧⟩ ∙ 𝑤)
90		breq1 4656	. . . . . . 7 ⊢ (𝑥 = ⟨𝑦, 𝑧⟩ → (𝑥 ∙ 𝑤 ↔ ⟨𝑦, 𝑧⟩ ∙ 𝑤))
91	90	mobidv 2491	. . . . . 6 ⊢ (𝑥 = ⟨𝑦, 𝑧⟩ → (∃𝑤 𝑥 ∙ 𝑤 ↔ ∃𝑤⟨𝑦, 𝑧⟩ ∙ 𝑤))
92	91	ralxp 5263	. . . . 5 ⊢ (∀𝑥 ∈ (ran 𝐹 × ran 𝐹)∃𝑤 𝑥 ∙ 𝑤 ↔ ∀𝑦 ∈ ran 𝐹∀𝑧 ∈ ran 𝐹∃𝑤⟨𝑦, 𝑧⟩ ∙ 𝑤)
93	89, 92	sylibr 224	. . . 4 ⊢ (𝜑 → ∀𝑥 ∈ (ran 𝐹 × ran 𝐹)∃*𝑤 𝑥 ∙ 𝑤)
94		ssralv 3666	. . . 4 ⊢ (dom ∙ ⊆ (ran 𝐹 × ran 𝐹) → (∀𝑥 ∈ (ran 𝐹 × ran 𝐹)∃𝑤 𝑥 ∙ 𝑤 → ∀𝑥 ∈ dom ∙ ∃𝑤 𝑥 ∙ 𝑤))
95	42, 93, 94	sylc 65	. . 3 ⊢ (𝜑 → ∀𝑥 ∈ dom ∙ ∃*𝑤 𝑥 ∙ 𝑤)
96		dffun7 5915	. . 3 ⊢ (Fun ∙ ↔ (Rel ∙ ∧ ∀𝑥 ∈ dom ∙ ∃*𝑤 𝑥 ∙ 𝑤))
97	12, 95, 96	sylanbrc 698	. 2 ⊢ (𝜑 → Fun ∙ )
98		eqimss2 3658	. . . . . . . . . . 11 ⊢ ( ∙ = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} → ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ ∙ )
99	10, 98	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ ∙ )
100		iunss 4561	. . . . . . . . . 10 ⊢ (∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ ∙ ↔ ∀𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ ∙ )
101	99, 100	sylib 208	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ ∙ )
102		iunss 4561	. . . . . . . . . . 11 ⊢ (∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ ∙ ↔ ∀𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ ∙ )
103		opex 4932	. . . . . . . . . . . . . 14 ⊢ ⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩ ∈ V
104	103	snss 4316	. . . . . . . . . . . . 13 ⊢ (⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩ ∈ ∙ ↔ {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ ∙ )
105	1, 2	opeldm 5328	. . . . . . . . . . . . 13 ⊢ (⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩ ∈ ∙ → ⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩ ∈ dom ∙ )
106	104, 105	sylbir 225	. . . . . . . . . . . 12 ⊢ ({⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ ∙ → ⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩ ∈ dom ∙ )
107	106	ralimi 2952	. . . . . . . . . . 11 ⊢ (∀𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ ∙ → ∀𝑞 ∈ 𝑉 ⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩ ∈ dom ∙ )
108	102, 107	sylbi 207	. . . . . . . . . 10 ⊢ (∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ ∙ → ∀𝑞 ∈ 𝑉 ⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩ ∈ dom ∙ )
109	108	ralimi 2952	. . . . . . . . 9 ⊢ (∀𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ ∙ → ∀𝑝 ∈ 𝑉 ∀𝑞 ∈ 𝑉 ⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩ ∈ dom ∙ )
110	101, 109	syl 17	. . . . . . . 8 ⊢ (𝜑 → ∀𝑝 ∈ 𝑉 ∀𝑞 ∈ 𝑉 ⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩ ∈ dom ∙ )
111		opeq2 4403	. . . . . . . . . . . 12 ⊢ (𝑧 = (𝐹‘𝑞) → ⟨(𝐹‘𝑝), 𝑧⟩ = ⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩)
112	111	eleq1d 2686	. . . . . . . . . . 11 ⊢ (𝑧 = (𝐹‘𝑞) → (⟨(𝐹‘𝑝), 𝑧⟩ ∈ dom ∙ ↔ ⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩ ∈ dom ∙ ))
113	112	ralrn 6362	. . . . . . . . . 10 ⊢ (𝐹 Fn 𝑉 → (∀𝑧 ∈ ran 𝐹⟨(𝐹‘𝑝), 𝑧⟩ ∈ dom ∙ ↔ ∀𝑞 ∈ 𝑉 ⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩ ∈ dom ∙ ))
114	75, 113	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (∀𝑧 ∈ ran 𝐹⟨(𝐹‘𝑝), 𝑧⟩ ∈ dom ∙ ↔ ∀𝑞 ∈ 𝑉 ⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩ ∈ dom ∙ ))
115	114	ralbidv 2986	. . . . . . . 8 ⊢ (𝜑 → (∀𝑝 ∈ 𝑉 ∀𝑧 ∈ ran 𝐹⟨(𝐹‘𝑝), 𝑧⟩ ∈ dom ∙ ↔ ∀𝑝 ∈ 𝑉 ∀𝑞 ∈ 𝑉 ⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩ ∈ dom ∙ ))
116	110, 115	mpbird 247	. . . . . . 7 ⊢ (𝜑 → ∀𝑝 ∈ 𝑉 ∀𝑧 ∈ ran 𝐹⟨(𝐹‘𝑝), 𝑧⟩ ∈ dom ∙ )
117		opeq1 4402	. . . . . . . . . . 11 ⊢ (𝑦 = (𝐹‘𝑝) → ⟨𝑦, 𝑧⟩ = ⟨(𝐹‘𝑝), 𝑧⟩)
118	117	eleq1d 2686	. . . . . . . . . 10 ⊢ (𝑦 = (𝐹‘𝑝) → (⟨𝑦, 𝑧⟩ ∈ dom ∙ ↔ ⟨(𝐹‘𝑝), 𝑧⟩ ∈ dom ∙ ))
119	118	ralbidv 2986	. . . . . . . . 9 ⊢ (𝑦 = (𝐹‘𝑝) → (∀𝑧 ∈ ran 𝐹⟨𝑦, 𝑧⟩ ∈ dom ∙ ↔ ∀𝑧 ∈ ran 𝐹⟨(𝐹‘𝑝), 𝑧⟩ ∈ dom ∙ ))
120	119	ralrn 6362	. . . . . . . 8 ⊢ (𝐹 Fn 𝑉 → (∀𝑦 ∈ ran 𝐹∀𝑧 ∈ ran 𝐹⟨𝑦, 𝑧⟩ ∈ dom ∙ ↔ ∀𝑝 ∈ 𝑉 ∀𝑧 ∈ ran 𝐹⟨(𝐹‘𝑝), 𝑧⟩ ∈ dom ∙ ))
121	75, 120	syl 17	. . . . . . 7 ⊢ (𝜑 → (∀𝑦 ∈ ran 𝐹∀𝑧 ∈ ran 𝐹⟨𝑦, 𝑧⟩ ∈ dom ∙ ↔ ∀𝑝 ∈ 𝑉 ∀𝑧 ∈ ran 𝐹⟨(𝐹‘𝑝), 𝑧⟩ ∈ dom ∙ ))
122	116, 121	mpbird 247	. . . . . 6 ⊢ (𝜑 → ∀𝑦 ∈ ran 𝐹∀𝑧 ∈ ran 𝐹⟨𝑦, 𝑧⟩ ∈ dom ∙ )
123		eleq1 2689	. . . . . . 7 ⊢ (𝑥 = ⟨𝑦, 𝑧⟩ → (𝑥 ∈ dom ∙ ↔ ⟨𝑦, 𝑧⟩ ∈ dom ∙ ))
124	123	ralxp 5263	. . . . . 6 ⊢ (∀𝑥 ∈ (ran 𝐹 × ran 𝐹)𝑥 ∈ dom ∙ ↔ ∀𝑦 ∈ ran 𝐹∀𝑧 ∈ ran 𝐹⟨𝑦, 𝑧⟩ ∈ dom ∙ )
125	122, 124	sylibr 224	. . . . 5 ⊢ (𝜑 → ∀𝑥 ∈ (ran 𝐹 × ran 𝐹)𝑥 ∈ dom ∙ )
126		dfss3 3592	. . . . 5 ⊢ ((ran 𝐹 × ran 𝐹) ⊆ dom ∙ ↔ ∀𝑥 ∈ (ran 𝐹 × ran 𝐹)𝑥 ∈ dom ∙ )
127	125, 126	sylibr 224	. . . 4 ⊢ (𝜑 → (ran 𝐹 × ran 𝐹) ⊆ dom ∙ )
128	41, 127	eqsstr3d 3640	. . 3 ⊢ (𝜑 → (𝐵 × 𝐵) ⊆ dom ∙ )
129	38, 128	eqssd 3620	. 2 ⊢ (𝜑 → dom ∙ = (𝐵 × 𝐵))
130		df-fn 5891	. 2 ⊢ ( ∙ Fn (𝐵 × 𝐵) ↔ (Fun ∙ ∧ dom ∙ = (𝐵 × 𝐵)))
131	97, 129, 130	sylanbrc 698	1 ⊢ (𝜑 → ∙ Fn (𝐵 × 𝐵))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 196 ∧ wa 384 ∧ w3a 1037 ∀wal 1481 = wceq 1483 ∈ wcel 1990 ∃*wmo 2471 ≠ wne 2794 ∀wral 2912 ∃wrex 2913 Vcvv 3200 ⊆ wss 3574 ∅c0 3915 {csn 4177 ⟨cop 4183 ∪ ciun 4520 class class class wbr 4653 × cxp 5112 dom cdm 5114 ran crn 5115 Rel wrel 5119 Fun wfun 5882 Fn wfn 5883 ⟶wf 5884 –onto→wfo 5886 ‘cfv 5888 (class class class)co 6650

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-sep 4781 ax-nul 4789 ax-pr 4906

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-ral 2917 df-rex 2918 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-nul 3916 df-if 4087 df-sn 4178 df-pr 4180 df-op 4184 df-uni 4437 df-iun 4522 df-br 4654 df-opab 4713 df-mpt 4730 df-id 5024 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-fo 5894 df-fv 5896

This theorem is referenced by: imasaddvallem 16189 imasaddflem 16190 imasaddfn 16191 imasmulfn 16194

W3C validator