Theorem iscau4 7897

Description: Express the property "F is a Cauchy sequence of metric D."

Hypothesis

Ref	Expression
lmbr.1	⊢ X = dom dom D

Assertion

Ref	Expression
iscau4	⊢ (D ∈ Met → (F ∈ (Cau ‘D) ↔ (F ⊆ (ℂ × X) ⋀ ∀x ∈ ℝ (0 < x → ∃j ∈ ℤ ∀k ∈ ℤ (j ≤ k → ((F ‘j) ∈ X ⋀ (F ‘k) ∈ X ⋀ ((F ‘j)D(F ‘k)) < x))))))

Distinct variable groups:   j,k,x,F   D,j,k,x   j,X,k,x

Proof of Theorem iscau4

Step	Hyp	Ref	Expression
1		lmbr.1	. . 3 ⊢ X = dom dom D
2	1	iscau 7893	. 2 ⊢ (D ∈ Met → (F ∈ (Cau ‘D) ↔ (F ⊆ (ℂ × X) ⋀ ∀x ∈ ℝ (0 < x → ∃m ∈ ℤ ∀j ∈ ℤ ∀k ∈ ℤ ((m ≤ j ⋀ m ≤ k) → ((F ‘j) ∈ X ⋀ (F ‘k) ∈ X ⋀ ((F ‘j)D(F ‘k)) < x))))))
3		fveq2 3722	. . . . . 6 ⊢ (k = m → (F ‘k) = (F ‘m))
4	3	eleq1d 1539	. . . . 5 ⊢ (k = m → ((F ‘k) ∈ X ↔ (F ‘m) ∈ X))
5	3	opreq2d 3974	. . . . . 6 ⊢ (k = m → ((F ‘j)D(F ‘k)) = ((F ‘j)D(F ‘m)))
6	5	breq1d 2627	. . . . 5 ⊢ (k = m → (((F ‘j)D(F ‘k)) < x ↔ ((F ‘j)D(F ‘m)) < x))
7	4, 6	3anbi23d 896	. . . 4 ⊢ (k = m → (((F ‘j) ∈ X ⋀ (F ‘k) ∈ X ⋀ ((F ‘j)D(F ‘k)) < x) ↔ ((F ‘j) ∈ X ⋀ (F ‘m) ∈ X ⋀ ((F ‘j)D(F ‘m)) < x)))
8		fveq2 3722	. . . . . 6 ⊢ (j = k → (F ‘j) = (F ‘k))
9	8	eleq1d 1539	. . . . 5 ⊢ (j = k → ((F ‘j) ∈ X ↔ (F ‘k) ∈ X))
10	8	opreq1d 3973	. . . . . 6 ⊢ (j = k → ((F ‘j)D(F ‘m)) = ((F ‘k)D(F ‘m)))
11	10	breq1d 2627	. . . . 5 ⊢ (j = k → (((F ‘j)D(F ‘m)) < x ↔ ((F ‘k)D(F ‘m)) < x))
12	9, 11	3anbi13d 895	. . . 4 ⊢ (j = k → (((F ‘j) ∈ X ⋀ (F ‘m) ∈ X ⋀ ((F ‘j)D(F ‘m)) < x) ↔ ((F ‘k) ∈ X ⋀ (F ‘m) ∈ X ⋀ ((F ‘k)D(F ‘m)) < x)))
13		breq2 2621	. . . . . 6 ⊢ (x = (y / 2) → (((F ‘j)D(F ‘k)) < x ↔ ((F ‘j)D(F ‘k)) < (y / 2)))
14	13	3anbi3d 899	. . . . 5 ⊢ (x = (y / 2) → (((F ‘j) ∈ X ⋀ (F ‘k) ∈ X ⋀ ((F ‘j)D(F ‘k)) < x) ↔ ((F ‘j) ∈ X ⋀ (F ‘k) ∈ X ⋀ ((F ‘j)D(F ‘k)) < (y / 2))))
15		breq2 2621	. . . . . 6 ⊢ (x = (y / 2) → (((F ‘j)D(F ‘m)) < x ↔ ((F ‘j)D(F ‘m)) < (y / 2)))
16	15	3anbi3d 899	. . . . 5 ⊢ (x = (y / 2) → (((F ‘j) ∈ X ⋀ (F ‘m) ∈ X ⋀ ((F ‘j)D(F ‘m)) < x) ↔ ((F ‘j) ∈ X ⋀ (F ‘m) ∈ X ⋀ ((F ‘j)D(F ‘m)) < (y / 2))))
17	14, 16	anbi12d 628	. . . 4 ⊢ (x = (y / 2) → ((((F ‘j) ∈ X ⋀ (F ‘k) ∈ X ⋀ ((F ‘j)D(F ‘k)) < x) ⋀ ((F ‘j) ∈ X ⋀ (F ‘m) ∈ X ⋀ ((F ‘j)D(F ‘m)) < x)) ↔ (((F ‘j) ∈ X ⋀ (F ‘k) ∈ X ⋀ ((F ‘j)D(F ‘k)) < (y / 2)) ⋀ ((F ‘j) ∈ X ⋀ (F ‘m) ∈ X ⋀ ((F ‘j)D(F ‘m)) < (y / 2)))))
18		breq2 2621	. . . . 5 ⊢ (x = y → (((F ‘k)D(F ‘m)) < x ↔ ((F ‘k)D(F ‘m)) < y))
19	18	3anbi3d 899	. . . 4 ⊢ (x = y → (((F ‘k) ∈ X ⋀ (F ‘m) ∈ X ⋀ ((F ‘k)D(F ‘m)) < x) ↔ ((F ‘k) ∈ X ⋀ (F ‘m) ∈ X ⋀ ((F ‘k)D(F ‘m)) < y)))
20		3simp2 789	. . . . . . . 8 ⊢ (((F ‘j) ∈ X ⋀ (F ‘k) ∈ X ⋀ ((F ‘j)D(F ‘k)) < (y / 2)) → (F ‘k) ∈ X)
21	20	adantr 389	. . . . . . 7 ⊢ ((((F ‘j) ∈ X ⋀ (F ‘k) ∈ X ⋀ ((F ‘j)D(F ‘k)) < (y / 2)) ⋀ ((F ‘j) ∈ X ⋀ (F ‘m) ∈ X ⋀ ((F ‘j)D(F ‘m)) < (y / 2))) → (F ‘k) ∈ X)
22	21	a1i 8	. . . . . 6 ⊢ ((D ∈ Met ⋀ y ∈ ℝ) → ((((F ‘j) ∈ X ⋀ (F ‘k) ∈ X ⋀ ((F ‘j)D(F ‘k)) < (y / 2)) ⋀ ((F ‘j) ∈ X ⋀ (F ‘m) ∈ X ⋀ ((F ‘j)D(F ‘m)) < (y / 2))) → (F ‘k) ∈ X))
23		3simp2 789	. . . . . . . 8 ⊢ (((F ‘j) ∈ X ⋀ (F ‘m) ∈ X ⋀ ((F ‘j)D(F ‘m)) < (y / 2)) → (F ‘m) ∈ X)
24	23	adantl 388	. . . . . . 7 ⊢ ((((F ‘j) ∈ X ⋀ (F ‘k) ∈ X ⋀ ((F ‘j)D(F ‘k)) < (y / 2)) ⋀ ((F ‘j) ∈ X ⋀ (F ‘m) ∈ X ⋀ ((F ‘j)D(F ‘m)) < (y / 2))) → (F ‘m) ∈ X)
25	24	a1i 8	. . . . . 6 ⊢ ((D ∈ Met ⋀ y ∈ ℝ) → ((((F ‘j) ∈ X ⋀ (F ‘k) ∈ X ⋀ ((F ‘j)D(F ‘k)) < (y / 2)) ⋀ ((F ‘j) ∈ X ⋀ (F ‘m) ∈ X ⋀ ((F ‘j)D(F ‘m)) < (y / 2))) → (F ‘m) ∈ X))
26		lt2halvest 6010	. . . . . . . . . . . 12 ⊢ ((((F ‘j)D(F ‘k)) ∈ ℝ ⋀ ((F ‘j)D(F ‘m)) ∈ ℝ ⋀ y ∈ ℝ) → ((((F ‘j)D(F ‘k)) < (y / 2) ⋀ ((F ‘j)D(F ‘m)) < (y / 2)) → (((F ‘j)D(F ‘k)) + ((F ‘j)D(F ‘m))) < y))
27	1	metcl 7768	. . . . . . . . . . . . . . 15 ⊢ ((D ∈ Met ⋀ (F ‘j) ∈ X ⋀ (F ‘k) ∈ X) → ((F ‘j)D(F ‘k)) ∈ ℝ)
28	27	3expb 834	. . . . . . . . . . . . . 14 ⊢ ((D ∈ Met ⋀ ((F ‘j) ∈ X ⋀ (F ‘k) ∈ X)) → ((F ‘j)D(F ‘k)) ∈ ℝ)
29	28	adantlr 393	. . . . . . . . . . . . 13 ⊢ (((D ∈ Met ⋀ y ∈ ℝ) ⋀ ((F ‘j) ∈ X ⋀ (F ‘k) ∈ X)) → ((F ‘j)D(F ‘k)) ∈ ℝ)
30	29	adantrrr 403	. . . . . . . . . . . 12 ⊢ (((D ∈ Met ⋀ y ∈ ℝ) ⋀ ((F ‘j) ∈ X ⋀ ((F ‘k) ∈ X ⋀ (F ‘m) ∈ X))) → ((F ‘j)D(F ‘k)) ∈ ℝ)
31	1	metcl 7768	. . . . . . . . . . . . . . 15 ⊢ ((D ∈ Met ⋀ (F ‘j) ∈ X ⋀ (F ‘m) ∈ X) → ((F ‘j)D(F ‘m)) ∈ ℝ)
32	31	3expb 834	. . . . . . . . . . . . . 14 ⊢ ((D ∈ Met ⋀ ((F ‘j) ∈ X ⋀ (F ‘m) ∈ X)) → ((F ‘j)D(F ‘m)) ∈ ℝ)
33	32	adantlr 393	. . . . . . . . . . . . 13 ⊢ (((D ∈ Met ⋀ y ∈ ℝ) ⋀ ((F ‘j) ∈ X ⋀ (F ‘m) ∈ X)) → ((F ‘j)D(F ‘m)) ∈ ℝ)
34	33	adantrrl 402	. . . . . . . . . . . 12 ⊢ (((D ∈ Met ⋀ y ∈ ℝ) ⋀ ((F ‘j) ∈ X ⋀ ((F ‘k) ∈ X ⋀ (F ‘m) ∈ X))) → ((F ‘j)D(F ‘m)) ∈ ℝ)
35		simplr 413	. . . . . . . . . . . 12 ⊢ (((D ∈ Met ⋀ y ∈ ℝ) ⋀ ((F ‘j) ∈ X ⋀ ((F ‘k) ∈ X ⋀ (F ‘m) ∈ X))) → y ∈ ℝ)
36	26, 30, 34, 35	syl3anc 858	. . . . . . . . . . 11 ⊢ (((D ∈ Met ⋀ y ∈ ℝ) ⋀ ((F ‘j) ∈ X ⋀ ((F ‘k) ∈ X ⋀ (F ‘m) ∈ X))) → ((((F ‘j)D(F ‘k)) < (y / 2) ⋀ ((F ‘j)D(F ‘m)) < (y / 2)) → (((F ‘j)D(F ‘k)) + ((F ‘j)D(F ‘m))) < y))
37	1	mettri4 7771	. . . . . . . . . . . . . . . 16 ⊢ (((D ∈ Met ⋀ (F ‘k) ∈ X) ⋀ ((F ‘m) ∈ X ⋀ (F ‘j) ∈ X)) → ((F ‘k)D(F ‘m)) ≤ (((F ‘j)D(F ‘k)) + ((F ‘j)D(F ‘m))))
38	37	exp43 384	. . . . . . . . . . . . . . 15 ⊢ (D ∈ Met → ((F ‘k) ∈ X → ((F ‘m) ∈ X → ((F ‘j) ∈ X → ((F ‘k)D(F ‘m)) ≤ (((F ‘j)D(F ‘k)) + ((F ‘j)D(F ‘m)))))))
39	38	imp44 371	. . . . . . . . . . . . . 14 ⊢ ((D ∈ Met ⋀ (((F ‘k) ∈ X ⋀ (F ‘m) ∈ X) ⋀ (F ‘j) ∈ X)) → ((F ‘k)D(F ‘m)) ≤ (((F ‘j)D(F ‘k)) + ((F ‘j)D(F ‘m))))
40	39	ancom2s 487	. . . . . . . . . . . . 13 ⊢ ((D ∈ Met ⋀ ((F ‘j) ∈ X ⋀ ((F ‘k) ∈ X ⋀ (F ‘m) ∈ X))) → ((F ‘k)D(F ‘m)) ≤ (((F ‘j)D(F ‘k)) + ((F ‘j)D(F ‘m))))
41	40	adantlr 393	. . . . . . . . . . . 12 ⊢ (((D ∈ Met ⋀ y ∈ ℝ) ⋀ ((F ‘j) ∈ X ⋀ ((F ‘k) ∈ X ⋀ (F ‘m) ∈ X))) → ((F ‘k)D(F ‘m)) ≤ (((F ‘j)D(F ‘k)) + ((F ‘j)D(F ‘m))))
42		lelttrt 5511	. . . . . . . . . . . . 13 ⊢ ((((F ‘k)D(F ‘m)) ∈ ℝ ⋀ (((F ‘j)D(F ‘k)) + ((F ‘j)D(F ‘m))) ∈ ℝ ⋀ y ∈ ℝ) → ((((F ‘k)D(F ‘m)) ≤ (((F ‘j)D(F ‘k)) + ((F ‘j)D(F ‘m))) ⋀ (((F ‘j)D(F ‘k)) + ((F ‘j)D(F ‘m))) < y) → ((F ‘k)D(F ‘m)) < y))
43	1	metcl 7768	. . . . . . . . . . . . . . 15 ⊢ ((D ∈ Met ⋀ (F ‘k) ∈ X ⋀ (F ‘m) ∈ X) → ((F ‘k)D(F ‘m)) ∈ ℝ)
44	43	3expb 834	. . . . . . . . . . . . . 14 ⊢ ((D ∈ Met ⋀ ((F ‘k) ∈ X ⋀ (F ‘m) ∈ X)) → ((F ‘k)D(F ‘m)) ∈ ℝ)
45	44	ad2ant2rl 411	. . . . . . . . . . . . 13 ⊢ (((D ∈ Met ⋀ y ∈ ℝ) ⋀ ((F ‘j) ∈ X ⋀ ((F ‘k) ∈ X ⋀ (F ‘m) ∈ X))) → ((F ‘k)D(F ‘m)) ∈ ℝ)
46		axaddrcl 5260	. . . . . . . . . . . . . . 15 ⊢ ((((F ‘j)D(F ‘k)) ∈ ℝ ⋀ ((F ‘j)D(F ‘m)) ∈ ℝ) → (((F ‘j)D(F ‘k)) + ((F ‘j)D(F ‘m))) ∈ ℝ)
47	28	adantrrr 403	. . . . . . . . . . . . . . 15 ⊢ ((D ∈ Met ⋀ ((F ‘j) ∈ X ⋀ ((F ‘k) ∈ X ⋀ (F ‘m) ∈ X))) → ((F ‘j)D(F ‘k)) ∈ ℝ)
48	32	adantrrl 402	. . . . . . . . . . . . . . 15 ⊢ ((D ∈ Met ⋀ ((F ‘j) ∈ X ⋀ ((F ‘k) ∈ X ⋀ (F ‘m) ∈ X))) → ((F ‘j)D(F ‘m)) ∈ ℝ)
49	46, 47, 48	sylanc 471	. . . . . . . . . . . . . 14 ⊢ ((D ∈ Met ⋀ ((F ‘j) ∈ X ⋀ ((F ‘k) ∈ X ⋀ (F ‘m) ∈ X))) → (((F ‘j)D(F ‘k)) + ((F ‘j)D(F ‘m))) ∈ ℝ)
50	49	adantlr 393	. . . . . . . . . . . . 13 ⊢ (((D ∈ Met ⋀ y ∈ ℝ) ⋀ ((F ‘j) ∈ X ⋀ ((F ‘k) ∈ X ⋀ (F ‘m) ∈ X))) → (((F ‘j)D(F ‘k)) + ((F ‘j)D(F ‘m))) ∈ ℝ)
51	42, 45, 50, 35	syl3anc 858	. . . . . . . . . . . 12 ⊢ (((D ∈ Met ⋀ y ∈ ℝ) ⋀ ((F ‘j) ∈ X ⋀ ((F ‘k) ∈ X ⋀ (F ‘m) ∈ X))) → ((((F ‘k)D(F ‘m)) ≤ (((F ‘j)D(F ‘k)) + ((F ‘j)D(F ‘m))) ⋀ (((F ‘j)D(F ‘k)) + ((F ‘j)D(F ‘m))) < y) → ((F ‘k)D(F ‘m)) < y))
52	41, 51	mpand 701	. . . . . . . . . . 11 ⊢ (((D ∈ Met ⋀ y ∈ ℝ) ⋀ ((F ‘j) ∈ X ⋀ ((F ‘k) ∈ X ⋀ (F ‘m) ∈ X))) → ((((F ‘j)D(F ‘k)) + ((F ‘j)D(F ‘m))) < y → ((F ‘k)D(F ‘m)) < y))
53	36, 52	syld 27	. . . . . . . . . 10 ⊢ (((D ∈ Met ⋀ y ∈ ℝ) ⋀ ((F ‘j) ∈ X ⋀ ((F ‘k) ∈ X ⋀ (F ‘m) ∈ X))) → ((((F ‘j)D(F ‘k)) < (y / 2) ⋀ ((F ‘j)D(F ‘m)) < (y / 2)) → ((F ‘k)D(F ‘m)) < y))
54	53	exp32 377	. . . . . . . . 9 ⊢ ((D ∈ Met ⋀ y ∈ ℝ) → ((F ‘j) ∈ X → (((F ‘k) ∈ X ⋀ (F ‘m) ∈ X) → ((((F ‘j)D(F ‘k)) < (y / 2) ⋀ ((F ‘j)D(F ‘m)) < (y / 2)) → ((F ‘k)D(F ‘m)) < y))))
55	54	adantld 390	. . . . . . . 8 ⊢ ((D ∈ Met ⋀ y ∈ ℝ) → (((F ‘j) ∈ X ⋀ (F ‘j) ∈ X) → (((F ‘k) ∈ X ⋀ (F ‘m) ∈ X) → ((((F ‘j)D(F ‘k)) < (y / 2) ⋀ ((F ‘j)D(F ‘m)) < (y / 2)) → ((F ‘k)D(F ‘m)) < y))))
56	55	3impd 847	. . . . . . 7 ⊢ ((D ∈ Met ⋀ y ∈ ℝ) → ((((F ‘j) ∈ X ⋀ (F ‘j) ∈ X) ⋀ ((F ‘k) ∈ X ⋀ (F ‘m) ∈ X) ⋀ (((F ‘j)D(F ‘k)) < (y / 2) ⋀ ((F ‘j)D(F ‘m)) < (y / 2))) → ((F ‘k)D(F ‘m)) < y))
57		an6 902	. . . . . . 7 ⊢ ((((F ‘j) ∈ X ⋀ (F ‘k) ∈ X ⋀ ((F ‘j)D(F ‘k)) < (y / 2)) ⋀ ((F ‘j) ∈ X ⋀ (F ‘m) ∈ X ⋀ ((F ‘j)D(F ‘m)) < (y / 2))) ↔ (((F ‘j) ∈ X ⋀ (F ‘j) ∈ X) ⋀ ((F ‘k) ∈ X ⋀ (F ‘m) ∈ X) ⋀ (((F ‘j)D(F ‘k)) < (y / 2) ⋀ ((F ‘j)D(F ‘m)) < (y / 2))))
58	56, 57	syl5ib 206	. . . . . 6 ⊢ ((D ∈ Met ⋀ y ∈ ℝ) → ((((F ‘j) ∈ X ⋀ (F ‘k) ∈ X ⋀ ((F ‘j)D(F ‘k)) < (y / 2)) ⋀ ((F ‘j) ∈ X ⋀ (F ‘m) ∈ X ⋀ ((F ‘j)D(F ‘m)) < (y / 2))) → ((F ‘k)D(F ‘m)) < y))
59	22, 25, 58	3jcad 820	. . . . 5 ⊢ ((D ∈ Met ⋀ y ∈ ℝ) → ((((F ‘j) ∈ X ⋀ (F ‘k) ∈ X ⋀ ((F ‘j)D(F ‘k)) < (y / 2)) ⋀ ((F ‘j) ∈ X ⋀ (F ‘m) ∈ X ⋀ ((F ‘j)D(F ‘m)) < (y / 2))) → ((F ‘k) ∈ X ⋀ (F ‘m) ∈ X ⋀ ((F ‘k)D(F ‘m)) < y)))
60	59	adantr 389	. . . 4 ⊢ (((D ∈ Met ⋀ y ∈ ℝ) ⋀ (j ∈ ℤ ⋀ k ∈ ℤ ⋀ m ∈ ℤ)) → ((((F ‘j) ∈ X ⋀ (F ‘k) ∈ X ⋀ ((F ‘j)D(F ‘k)) < (y / 2)) ⋀ ((F ‘j) ∈ X ⋀ (F ‘m) ∈ X ⋀ ((F ‘j)D(F ‘m)) < (y / 2))) → ((F ‘k) ∈ X ⋀ (F ‘m) ∈ X ⋀ ((F ‘k)D(F ‘m)) < y)))
61		ssid 2078	. . . 4 ⊢ ℤ ⊆ ℤ
62	7, 12, 17, 19, 60, 61	cau3 6874	. . 3 ⊢ (D ∈ Met → (∀x ∈ ℝ (0 < x → ∃j ∈ ℤ ∀k ∈ ℤ (j ≤ k → ((F ‘j) ∈ X ⋀ (F ‘k) ∈ X ⋀ ((F ‘j)D(F ‘k)) < x))) ↔ ∀x ∈ ℝ (0 < x → ∃m ∈ ℤ ∀j ∈ ℤ ∀k ∈ ℤ ((m ≤ j ⋀ m ≤ k) → ((F ‘j) ∈ X ⋀ (F ‘k) ∈ X ⋀ ((F ‘j)D(F ‘k)) < x)))))
63	62	anbi2d 616	. 2 ⊢ (D ∈ Met → ((F ⊆ (ℂ × X) ⋀ ∀x ∈ ℝ (0 < x → ∃j ∈ ℤ ∀k ∈ ℤ (j ≤ k → ((F ‘j) ∈ X ⋀ (F ‘k) ∈ X ⋀ ((F ‘j)D(F ‘k)) < x)))) ↔ (F ⊆ (ℂ × X) ⋀ ∀x ∈ ℝ (0 < x → ∃m ∈ ℤ ∀j ∈ ℤ ∀k ∈ ℤ ((m ≤ j ⋀ m ≤ k) → ((F ‘j) ∈ X ⋀ (F ‘k) ∈ X ⋀ ((F ‘j)D(F ‘k)) < x))))))
64	2, 63	bitr4d 531	1 ⊢ (D ∈ Met → (F ∈ (Cau ‘D) ↔ (F ⊆ (ℂ × X) ⋀ ∀x ∈ ℝ (0 < x → ∃j ∈ ℤ ∀k ∈ ℤ (j ≤ k → ((F ‘j) ∈ X ⋀ (F ‘k) ∈ X ⋀ ((F ‘j)D(F ‘k)) < x))))))

Syntax hints:   → wi 3   ↔ wb 146   ⋀ wa 223   ⋀ w3a 775   = wceq 956   ∈ wcel 958  ∀wral 1644  ∃wrex 1645   ⊆ wss 2045   class class class wbr 2617   × cxp 3166  dom cdm 3168   ‘cfv 3180  (class class class)co 3961  ℂcc 5220  ℝcr 5221  0cc0 5222   + caddc 5225   / cdiv 5282   ≤ cle 5283  ℤcz 5286   < clt 5474  2c2 5929  Metcme 7746  Caucca 7877

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-9 965  ax-10 966  ax-11 967  ax-12 968  ax-13 969  ax-14 970  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459  ax-rep 2691  ax-sep 2701  ax-nul 2708  ax-pow 2740  ax-pr 2777  ax-un 2864  ax-inf2 4613

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3or 776  df-3an 777  df-ex 981  df-sb 1172  df-eu 1382  df-mo 1383  df-clab 1464  df-cleq 1469  df-clel 1472  df-ne 1586  df-nel 1587  df-ral 1648  df-rex 1649  df-reu 1650  df-rab 1651  df-v 1810  df-sbc 1940  df-csb 2000  df-dif 2047  df-un 2048  df-in 2049  df-ss 2051  df-pss 2053  df-nul 2279  df-if 2360  df-pw 2400  df-sn 2410  df-pr 2411  df-tp 2413  df-op 2414  df-uni 2502  df-int 2532  df-iun 2566  df-br 2618  df-opab 2665  df-tr 2679  df-eprel 2830  df-id 2833  df-po 2838  df-so 2848  df-fr 2915  df-we 2932  df-ord 2949  df-on 2950  df-lim 2951  df-suc 2952  df-om 3130  df-xp 3182  df-rel 3183  df-cnv 3184  df-co 3185  df-dm 3186  df-rn 3187  df-res 3188  df-ima 3189  df-fun 3190  df-fn 3191  df-f 3192  df-f1 3193  df-fo 3194  df-f1o 3195  df-fv 3196  df-rdg 3930  df-opr 3963  df-oprab 3964  df-1st 4077  df-2nd 4078  df-1o 4131  df-oadd 4133  df-omul 4134  df-er 4259  df-ec 4261  df-qs 4264  df-en 4365  df-dom 4366  df-sdom 4367  df-ni 4988  df-pli 4989  df-mi 4990  df-lti 4991  df-plpq 5023  df-mpq 5024  df-enq 5025  df-nq 5026  df-plq 5027  df-mq 5028  df-rq 5029  df-ltq 5030  df-1q 5031  df-np 5074  df-1p 5075  df-plp 5076  df-mp 5077  df-ltp 5078  df-plpr 5152  df-mpr 5153  df-enr 5154  df-nr 5155  df-plr 5156  df-mr 5157  df-ltr 5158  df-0r 5159  df-1r 5160  df-m1r 5161  df-c 5228  df-0 5229  df-1 5230  df-i 5231  df-r 5232  df-plus 5233  df-mul 5234  df-lt 5235  df-sub 5344  df-neg 5346  df-pnf 5475  df-mnf 5476  df-xr 5477  df-ltxr 5478  df-le 5479  df-div 5686  df-2 5938  df-z 6104  df-met 7750  df-cau 7880

Copyright terms: Public domain