Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
GIF version

Theorem seqval 4665

Description: Value of the infinite sequence builder operation.

**Hypotheses**
Ref	Expression
seqval.1	⊢ S ∈ V
seqval.2	⊢ F ∈ V
seqval.3	⊢ G = (rec({⟨z, w⟩∣w = (z + 1)}, 1) ↾ ω)
seqval.4	⊢ H = {⟨z, w⟩∣w = ⟨((1^st ‘z) + 1), ((2^nd ‘z)S(F ‘((1^st ‘z) + 1)))⟩}

**Assertion**
Ref	Expression
seqval	⊢ (SseqF) = {⟨x, y⟩∣(x ∈ ℕ ∧ y = (2^nd ‘((rec(H, ⟨1, (F ‘1)⟩) ∘ ^◡G) ‘x)))}

Distinct variable group(s): x,y,G x,H,y x,z,w,F,y x,S,y,z,w

**Proof of Theorem seqval**
Step	Hyp	Ref	Expression
1		seqval.1	. 2 ⊢ S ∈ V
2		seqval.2	. 2 ⊢ F ∈ V
3		nnex 4431	. . . 4 ⊢ ℕ ∈ V
4		moeq 1431	. . . . 5 ⊢ ∃*y y = (2^nd ‘((rec(H, ⟨1, (F ‘1)⟩) ∘ ^◡G) ‘x))
5	4	a1i 7	. . . 4 ⊢ (x ∈ ℕ → ∃*y y = (2^nd ‘((rec(H, ⟨1, (F ‘1)⟩) ∘ ^◡G) ‘x)))
6	3, 5	funopabex 2742	. . 3 ⊢ {⟨x, y⟩∣(x ∈ ℕ ∧ y = (2^nd ‘((rec(H, ⟨1, (F ‘1)⟩) ∘ ^◡G) ‘x)))} ∈ V
7		opreq 3005	. . . . . . . . . . . . . 14 ⊢ (f = S → ((2^nd ‘z)f(g ‘((1^st ‘z) + 1))) = ((2^nd ‘z)S(g ‘((1^st ‘z) + 1))))
8		opeq2 1877	. . . . . . . . . . . . . 14 ⊢ (((2^nd ‘z)f(g ‘((1^st ‘z) + 1))) = ((2^nd ‘z)S(g ‘((1^st ‘z) + 1))) → ⟨((1^st ‘z) + 1), ((2^nd ‘z)f(g ‘((1^st ‘z) + 1)))⟩ = ⟨((1^st ‘z) + 1), ((2^nd ‘z)S(g ‘((1^st ‘z) + 1)))⟩)
9	7, 8	syl 12	. . . . . . . . . . . . 13 ⊢ (f = S → ⟨((1^st ‘z) + 1), ((2^nd ‘z)f(g ‘((1^st ‘z) + 1)))⟩ = ⟨((1^st ‘z) + 1), ((2^nd ‘z)S(g ‘((1^st ‘z) + 1)))⟩)
10	9	cleq2d 1112	. . . . . . . . . . . 12 ⊢ (f = S → (w = ⟨((1^st ‘z) + 1), ((2^nd ‘z)f(g ‘((1^st ‘z) + 1)))⟩ ↔ w = ⟨((1^st ‘z) + 1), ((2^nd ‘z)S(g ‘((1^st ‘z) + 1)))⟩))
11	10	biopabdv 2102	. . . . . . . . . . 11 ⊢ (f = S → {⟨z, w⟩∣w = ⟨((1^st ‘z) + 1), ((2^nd ‘z)f(g ‘((1^st ‘z) + 1)))⟩} = {⟨z, w⟩∣w = ⟨((1^st ‘z) + 1), ((2^nd ‘z)S(g ‘((1^st ‘z) + 1)))⟩})
12		rdgeq1 2972	. . . . . . . . . . 11 ⊢ ({⟨z, w⟩∣w = ⟨((1^st ‘z) + 1), ((2^nd ‘z)f(g ‘((1^st ‘z) + 1)))⟩} = {⟨z, w⟩∣w = ⟨((1^st ‘z) + 1), ((2^nd ‘z)S(g ‘((1^st ‘z) + 1)))⟩} → rec({⟨z, w⟩∣w = ⟨((1^st ‘z) + 1), ((2^nd ‘z)f(g ‘((1^st ‘z) + 1)))⟩}, ⟨1, (g ‘1)⟩) = rec({⟨z, w⟩∣w = ⟨((1^st ‘z) + 1), ((2^nd ‘z)S(g ‘((1^st ‘z) + 1)))⟩}, ⟨1, (g ‘1)⟩))
13	11, 12	syl 12	. . . . . . . . . 10 ⊢ (f = S → rec({⟨z, w⟩∣w = ⟨((1^st ‘z) + 1), ((2^nd ‘z)f(g ‘((1^st ‘z) + 1)))⟩}, ⟨1, (g ‘1)⟩) = rec({⟨z, w⟩∣w = ⟨((1^st ‘z) + 1), ((2^nd ‘z)S(g ‘((1^st ‘z) + 1)))⟩}, ⟨1, (g ‘1)⟩))
14	13	coeq1d 2506	. . . . . . . . 9 ⊢ (f = S → (rec({⟨z, w⟩∣w = ⟨((1^st ‘z) + 1), ((2^nd ‘z)f(g ‘((1^st ‘z) + 1)))⟩}, ⟨1, (g ‘1)⟩) ∘ ^◡(rec({⟨z, w⟩∣w = (z + 1)}, 1) ↾ ω)) = (rec({⟨z, w⟩∣w = ⟨((1^st ‘z) + 1), ((2^nd ‘z)S(g ‘((1^st ‘z) + 1)))⟩}, ⟨1, (g ‘1)⟩) ∘ ^◡(rec({⟨z, w⟩∣w = (z + 1)}, 1) ↾ ω)))
15		seqval.3	. . . . . . . . . . 11 ⊢ G = (rec({⟨z, w⟩∣w = (z + 1)}, 1) ↾ ω)
16		cnveq 2513	. . . . . . . . . . 11 ⊢ (G = (rec({⟨z, w⟩∣w = (z + 1)}, 1) ↾ ω) → ^◡G = ^◡(rec({⟨z, w⟩∣w = (z + 1)}, 1) ↾ ω))
17	15, 16	ax-mp 6	. . . . . . . . . 10 ⊢ ^◡G = ^◡(rec({⟨z, w⟩∣w = (z + 1)}, 1) ↾ ω)
18	17	coeq2i 2505	. . . . . . . . 9 ⊢ (rec({⟨z, w⟩∣w = ⟨((1^st ‘z) + 1), ((2^nd ‘z)S(g ‘((1^st ‘z) + 1)))⟩}, ⟨1, (g ‘1)⟩) ∘ ^◡G) = (rec({⟨z, w⟩∣w = ⟨((1^st ‘z) + 1), ((2^nd ‘z)S(g ‘((1^st ‘z) + 1)))⟩}, ⟨1, (g ‘1)⟩) ∘ ^◡(rec({⟨z, w⟩∣w = (z + 1)}, 1) ↾ ω))
19	14, 18	syl6eqr 1142	. . . . . . . 8 ⊢ (f = S → (rec({⟨z, w⟩∣w = ⟨((1^st ‘z) + 1), ((2^nd ‘z)f(g ‘((1^st ‘z) + 1)))⟩}, ⟨1, (g ‘1)⟩) ∘ ^◡(rec({⟨z, w⟩∣w = (z + 1)}, 1) ↾ ω)) = (rec({⟨z, w⟩∣w = ⟨((1^st ‘z) + 1), ((2^nd ‘z)S(g ‘((1^st ‘z) + 1)))⟩}, ⟨1, (g ‘1)⟩) ∘ ^◡G))
20	19	fveq1d 2834	. . . . . . 7 ⊢ (f = S → ((rec({⟨z, w⟩∣w = ⟨((1^st ‘z) + 1), ((2^nd ‘z)f(g ‘((1^st ‘z) + 1)))⟩}, ⟨1, (g ‘1)⟩) ∘ ^◡(rec({⟨z, w⟩∣w = (z + 1)}, 1) ↾ ω)) ‘x) = ((rec({⟨z, w⟩∣w = ⟨((1^st ‘z) + 1), ((2^nd ‘z)S(g ‘((1^st ‘z) + 1)))⟩}, ⟨1, (g ‘1)⟩) ∘ ^◡G) ‘x))
21	20	fveq2d 2836	. . . . . 6 ⊢ (f = S → (2^nd ‘((rec({⟨z, w⟩∣w = ⟨((1^st ‘z) + 1), ((2^nd ‘z)f(g ‘((1^st ‘z) + 1)))⟩}, ⟨1, (g ‘1)⟩) ∘ ^◡(rec({⟨z, w⟩∣w = (z + 1)}, 1) ↾ ω)) ‘x)) = (2^nd ‘((rec({⟨z, w⟩∣w = ⟨((1^st ‘z) + 1), ((2^nd ‘z)S(g ‘((1^st ‘z) + 1)))⟩}, ⟨1, (g ‘1)⟩) ∘ ^◡G) ‘x)))
22	21	cleq2d 1112	. . . . 5 ⊢ (f = S → (y = (2^nd ‘((rec({⟨z, w⟩∣w = ⟨((1^st ‘z) + 1), ((2^nd ‘z)f(g ‘((1^st ‘z) + 1)))⟩}, ⟨1, (g ‘1)⟩) ∘ ^◡(rec({⟨z, w⟩∣w = (z + 1)}, 1) ↾ ω)) ‘x)) ↔ y = (2^nd ‘((rec({⟨z, w⟩∣w = ⟨((1^st ‘z) + 1), ((2^nd ‘z)S(g ‘((1^st ‘z) + 1)))⟩}, ⟨1, (g ‘1)⟩) ∘ ^◡G) ‘x))))
23	22	anbi2d 468	. . . 4 ⊢ (f = S → ((x ∈ ℕ ∧ y = (2^nd ‘((rec({⟨z, w⟩∣w = ⟨((1^st ‘z) + 1), ((2^nd ‘z)f(g ‘((1^st ‘z) + 1)))⟩}, ⟨1, (g ‘1)⟩) ∘ ^◡(rec({⟨z, w⟩∣w = (z + 1)}, 1) ↾ ω)) ‘x))) ↔ (x ∈ ℕ ∧ y = (2^nd ‘((rec({⟨z, w⟩∣w = ⟨((1^st ‘z) + 1), ((2^nd ‘z)S(g ‘((1^st ‘z) + 1)))⟩}, ⟨1, (g ‘1)⟩) ∘ ^◡G) ‘x)))))
24	23	biopabdv 2102	. . 3 ⊢ (f = S → {⟨x, y⟩∣(x ∈ ℕ ∧ y = (2^nd ‘((rec({⟨z, w⟩∣w = ⟨((1^st ‘z) + 1), ((2^nd ‘z)f(g ‘((1^st ‘z) + 1)))⟩}, ⟨1, (g ‘1)⟩) ∘ ^◡(rec({⟨z, w⟩∣w = (z + 1)}, 1) ↾ ω)) ‘x)))} = {⟨x, y⟩∣(x ∈ ℕ ∧ y = (2^nd ‘((rec({⟨z, w⟩∣w = ⟨((1^st ‘z) + 1), ((2^nd ‘z)S(g ‘((1^st ‘z) + 1)))⟩}, ⟨1, (g ‘1)⟩) ∘ ^◡G) ‘x)))})
25		fveq1 2831	. . . . . . . . . . . . . . . 16 ⊢ (g = F → (g ‘((1^st ‘z) + 1)) = (F ‘((1^st ‘z) + 1)))
26	25	opreq2d 3013	. . . . . . . . . . . . . . 15 ⊢ (g = F → ((2^nd ‘z)S(g ‘((1^st ‘z) + 1))) = ((2^nd ‘z)S(F ‘((1^st ‘z) + 1))))
27		opeq2 1877	. . . . . . . . . . . . . . 15 ⊢ (((2^nd ‘z)S(g ‘((1^st ‘z) + 1))) = ((2^nd ‘z)S(F ‘((1^st ‘z) + 1))) → ⟨((1^st ‘z) + 1), ((2^nd ‘z)S(g ‘((1^st ‘z) + 1)))⟩ = ⟨((1^st ‘z) + 1), ((2^nd ‘z)S(F ‘((1^st ‘z) + 1)))⟩)
28	26, 27	syl 12	. . . . . . . . . . . . . 14 ⊢ (g = F → ⟨((1^st ‘z) + 1), ((2^nd ‘z)S(g ‘((1^st ‘z) + 1)))⟩ = ⟨((1^st ‘z) + 1), ((2^nd ‘z)S(F ‘((1^st ‘z) + 1)))⟩)
29	28	cleq2d 1112	. . . . . . . . . . . . 13 ⊢ (g = F → (w = ⟨((1^st ‘z) + 1), ((2^nd ‘z)S(g ‘((1^st ‘z) + 1)))⟩ ↔ w = ⟨((1^st ‘z) + 1), ((2^nd ‘z)S(F ‘((1^st ‘z) + 1)))⟩))
30	29	biopabdv 2102	. . . . . . . . . . . 12 ⊢ (g = F → {⟨z, w⟩∣w = ⟨((1^st ‘z) + 1), ((2^nd ‘z)S(g ‘((1^st ‘z) + 1)))⟩} = {⟨z, w⟩∣w = ⟨((1^st ‘z) + 1), ((2^nd ‘z)S(F ‘((1^st ‘z) + 1)))⟩})
31		seqval.4	. . . . . . . . . . . 12 ⊢ H = {⟨z, w⟩∣w = ⟨((1^st ‘z) + 1), ((2^nd ‘z)S(F ‘((1^st ‘z) + 1)))⟩}
32	30, 31	syl6eqr 1142	. . . . . . . . . . 11 ⊢ (g = F → {⟨z, w⟩∣w = ⟨((1^st ‘z) + 1), ((2^nd ‘z)S(g ‘((1^st ‘z) + 1)))⟩} = H)
33		rdgeq1 2972	. . . . . . . . . . 11 ⊢ ({⟨z, w⟩∣w = ⟨((1^st ‘z) + 1), ((2^nd ‘z)S(g ‘((1^st ‘z) + 1)))⟩} = H → rec({⟨z, w⟩∣w = ⟨((1^st ‘z) + 1), ((2^nd ‘z)S(g ‘((1^st ‘z) + 1)))⟩}, ⟨1, (g ‘1)⟩) = rec(H, ⟨1, (g ‘1)⟩))
34	32, 33	syl 12	. . . . . . . . . 10 ⊢ (g = F → rec({⟨z, w⟩∣w = ⟨((1^st ‘z) + 1), ((2^nd ‘z)S(g ‘((1^st ‘z) + 1)))⟩}, ⟨1, (g ‘1)⟩) = rec(H, ⟨1, (g ‘1)⟩))
35		fveq1 2831	. . . . . . . . . . 11 ⊢ (g = F → (g ‘1) = (F ‘1))
36		opeq2 1877	. . . . . . . . . . 11 ⊢ ((g ‘1) = (F ‘1) → ⟨1, (g ‘1)⟩ = ⟨1, (F ‘1)⟩)
37		rdgeq2 2973	. . . . . . . . . . 11 ⊢ (⟨1, (g ‘1)⟩ = ⟨1, (F ‘1)⟩ → rec(H, ⟨1, (g ‘1)⟩) = rec(H, ⟨1, (F ‘1)⟩))
38	35, 36, 37	3syl 21	. . . . . . . . . 10 ⊢ (g = F → rec(H, ⟨1, (g ‘1)⟩) = rec(H, ⟨1, (F ‘1)⟩))
39	34, 38	eqtrd 1128	. . . . . . . . 9 ⊢ (g = F → rec({⟨z, w⟩∣w = ⟨((1^st ‘z) + 1), ((2^nd ‘z)S(g ‘((1^st ‘z) + 1)))⟩}, ⟨1, (g ‘1)⟩) = rec(H, ⟨1, (F ‘1)⟩))
40	39	coeq1d 2506	. . . . . . . 8 ⊢ (g = F → (rec({⟨z, w⟩∣w = ⟨((1^st ‘z) + 1), ((2^nd ‘z)S(g ‘((1^st ‘z) + 1)))⟩}, ⟨1, (g ‘1)⟩) ∘ ^◡G) = (rec(H, ⟨1, (F ‘1)⟩) ∘ ^◡G))
41	40	fveq1d 2834	. . . . . . 7 ⊢ (g = F → ((rec({⟨z, w⟩∣w = ⟨((1^st ‘z) + 1), ((2^nd ‘z)S(g ‘((1^st ‘z) + 1)))⟩}, ⟨1, (g ‘1)⟩) ∘ ^◡G) ‘x) = ((rec(H, ⟨1, (F ‘1)⟩) ∘ ^◡G) ‘x))
42	41	fveq2d 2836	. . . . . 6 ⊢ (g = F → (2^nd ‘((rec({⟨z, w⟩∣w = ⟨((1^st ‘z) + 1), ((2^nd ‘z)S(g ‘((1^st ‘z) + 1)))⟩}, ⟨1, (g ‘1)⟩) ∘ ^◡G) ‘x)) = (2^nd ‘((rec(H, ⟨1, (F ‘1)⟩) ∘ ^◡G) ‘x)))
43	42	cleq2d 1112	. . . . 5 ⊢ (g = F → (y = (2^nd ‘((rec({⟨z, w⟩∣w = ⟨((1^st ‘z) + 1), ((2^nd ‘z)S(g ‘((1^st ‘z) + 1)))⟩}, ⟨1, (g ‘1)⟩) ∘ ^◡G) ‘x)) ↔ y = (2^nd ‘((rec(H, ⟨1, (F ‘1)⟩) ∘ ^◡G) ‘x))))
44	43	anbi2d 468	. . . 4 ⊢ (g = F → ((x ∈ ℕ ∧ y = (2^nd ‘((rec({⟨z, w⟩∣w = ⟨((1^st ‘z) + 1), ((2^nd ‘z)S(g ‘((1^st ‘z) + 1)))⟩}, ⟨1, (g ‘1)⟩) ∘ ^◡G) ‘x))) ↔ (x ∈ ℕ ∧ y = (2^nd ‘((rec(H, ⟨1, (F ‘1)⟩) ∘ ^◡G) ‘x)))))
45	44	biopabdv 2102	. . 3 ⊢ (g = F → {⟨x, y⟩∣(x ∈ ℕ ∧ y = (2^nd ‘((rec({⟨z, w⟩∣w = ⟨((1^st ‘z) + 1), ((2^nd ‘z)S(g ‘((1^st ‘z) + 1)))⟩}, ⟨1, (g ‘1)⟩) ∘ ^◡G) ‘x)))} = {⟨x, y⟩∣(x ∈ ℕ ∧ y = (2^nd ‘((rec(H, ⟨1, (F ‘1)⟩) ∘ ^◡G) ‘x)))})
46		df-seq 4661	. . . 4 ⊢ seq = {⟨⟨f, g⟩, h⟩∣h = {⟨x, y⟩∣(x ∈ ℕ ∧ y = (2^nd ‘((rec({⟨z, w⟩∣w = ⟨((1^st ‘z) + 1), ((2^nd ‘z)f(g ‘((1^st ‘z) + 1)))⟩}, ⟨1, (g ‘1)⟩) ∘ ^◡(rec({⟨z, w⟩∣w = (z + 1)}, 1) ↾ ω)) ‘x)))}}
47		visset 1350	. . . . . . 7 ⊢ f ∈ V
48		visset 1350	. . . . . . 7 ⊢ g ∈ V
49	47, 48	pm3.2i 234	. . . . . 6 ⊢ (f ∈ V ∧ g ∈ V)
50	49	biantrur 544	. . . . 5 ⊢ (h = {⟨x, y⟩∣(x ∈ ℕ ∧ y = (2^nd ‘((rec({⟨z, w⟩∣w = ⟨((1^st ‘z) + 1), ((2^nd ‘z)f(g ‘((1^st ‘z) + 1)))⟩}, ⟨1, (g ‘1)⟩) ∘ ^◡(rec({⟨z, w⟩∣w = (z + 1)}, 1) ↾ ω)) ‘x)))} ↔ ((f ∈ V ∧ g ∈ V) ∧ h = {⟨x, y⟩∣(x ∈ ℕ ∧ y = (2^nd ‘((rec({⟨z, w⟩∣w = ⟨((1^st ‘z) + 1), ((2^nd ‘z)f(g ‘((1^st ‘z) + 1)))⟩}, ⟨1, (g ‘1)⟩) ∘ ^◡(rec({⟨z, w⟩∣w = (z + 1)}, 1) ↾ ω)) ‘x)))}))
51	50	bioprabi 3027	. . . 4 ⊢ {⟨⟨f, g⟩, h⟩∣h = {⟨x, y⟩∣(x ∈ ℕ ∧ y = (2^nd ‘((rec({⟨z, w⟩∣w = ⟨((1^st ‘z) + 1), ((2^nd ‘z)f(g ‘((1^st ‘z) + 1)))⟩}, ⟨1, (g ‘1)⟩) ∘ ^◡(rec({⟨z, w⟩∣w = (z + 1)}, 1) ↾ ω)) ‘x)))}} = {⟨⟨f, g⟩, h⟩∣((f ∈ V ∧ g ∈ V) ∧ h = {⟨x, y⟩∣(x ∈ ℕ ∧ y = (2^nd ‘((rec({⟨z, w⟩∣w = ⟨((1^st ‘z) + 1), ((2^nd ‘z)f(g ‘((1^st ‘z) + 1)))⟩}, ⟨1, (g ‘1)⟩) ∘ ^◡(rec({⟨z, w⟩∣w = (z + 1)}, 1) ↾ ω)) ‘x)))})}
52	46, 51	eqtr 1119	. . 3 ⊢ seq = {⟨⟨f, g⟩, h⟩∣((f ∈ V ∧ g ∈ V) ∧ h = {⟨x, y⟩∣(x ∈ ℕ ∧ y = (2^nd ‘((rec({⟨z, w⟩∣w = ⟨((1^st ‘z) + 1), ((2^nd ‘z)f(g ‘((1^st ‘z) + 1)))⟩}, ⟨1, (g ‘1)⟩) ∘ ^◡(rec({⟨z, w⟩∣w = (z + 1)}, 1) ↾ ω)) ‘x)))})}
53	6, 24, 45, 52	oprabval2 3051	. 2 ⊢ ((S ∈ V ∧ F ∈ V) → (SseqF) = {⟨x, y⟩∣(x ∈ ℕ ∧ y = (2^nd ‘((rec(H, ⟨1, (F ‘1)⟩) ∘ ^◡G) ‘x)))})
54	1, 2, 53	mp2an 520	1 ⊢ (SseqF) = {⟨x, y⟩∣(x ∈ ℕ ∧ y = (2^nd ‘((rec(H, ⟨1, (F ‘1)⟩) ∘ ^◡G) ‘x)))}

Colors of variables: wff set class

Syntax hints: ∧ wa 196 ∃*wmo 1008 = wceq 1091 ∈ wcel 1092 Vcvv 1348 ⟨cop 1810 {copab 2055 ωcom 2372 ^◡ccnv 2409 ↾ cres 2412 ∘ ccom 2414 ‘cfv 2422 reccrdg 2969 (class class class)co 3001 {copab2 3002 1^st c1st 3085 2^nd c2nd 3086 1c1 4029 + caddc 4031 ℕcn 4093 seqcseq 4660

This theorem is referenced by: seqfnlem 4666 seqval2 4667

This theorem was proved from axioms: ax-1 3 ax-2 4 ax-3 5 ax-mp 6 ax-4 673 ax-5 674 ax-6 675 ax-7 676 ax-gen 677 ax-8 798 ax-9 799 ax-10 800 ax-11 801 ax-12 802 ax-13 804 ax-14 805 ax-16 922 ax-17 925 ax-ext 1074 ax-rep 1075 ax-un 1076 ax-pow 1077 ax-reg 1078 ax-inf 1079

This theorem depends on definitions: df-bi 128 df-or 197 df-an 198 df-3or 582 df-3an 583 df-ex 679 df-sb 853 df-eu 1009 df-mo 1010 df-clab 1093 df-cleq 1097 df-clel 1099 df-ne 1192 df-ral 1205 df-rex 1206 df-reu 1207 df-rab 1208 df-v 1349 df-sbc 1441 df-dif 1489 df-un 1490 df-in 1491 df-ss 1492 df-pss 1494 df-nul 1708 df-if 1777 df-pw 1799 df-sn 1811 df-pr 1812 df-tp 1814 df-op 1815 df-uni 1920 df-int 1966 df-iun 1996 df-tr 2042 df-br 2063 df-opab 2098 df-eprel 2122 df-id 2125 df-po 2128 df-so 2138 df-fr 2169 df-we 2186 df-ord 2202 df-on 2203 df-lim 2204 df-suc 2205 df-om 2373 df-xp 2424 df-rel 2425 df-cnv 2426 df-co 2427 df-dm 2428 df-rn 2429 df-res 2430 df-ima 2431 df-fun 2432 df-fn 2433 df-f 2434 df-f1 2435 df-fv 2438 df-rdg 2970 df-opr 3003 df-oprab 3004 df-1o 3104 df-oadd 3106 df-omul 3107 df-er 3200 df-ec 3202 df-qs 3205 df-ni 3794 df-pli 3795 df-mi 3796 df-lti 3797 df-plpq 3829 df-mpq 3830 df-enq 3831 df-nq 3832 df-plq 3833 df-mq 3834 df-rq 3835 df-ltq 3836 df-1q 3837 df-np 3880 df-1p 3881 df-plp 3882 df-ltp 3884 df-plpr 3958 df-enr 3960 df-nr 3961 df-plr 3962 df-0r 3965 df-1r 3966 df-c 4034 df-1 4036 df-r 4038 df-plus 4039 df-n 4423 df-seq 4661

metamath.org