Theorem iscaunns 7927

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

Hypotheses

Ref	Expression
lmbrnns.1	|- X = dom dom D
lmbrnns.2	|- (k e. NN -> A = (F` k))

Assertion

Ref	Expression
iscaunns	|- ((D e. Met /\ F:NN-->X) -> (F e. (Cau` D) <-> A.x e. RR+ E.j e. NN A.k e. NN (j <_ k -> ([_j / k]_ADA) < x)))

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

Proof of Theorem iscaunns

Step	Hyp	Ref	Expression
1		lmbrnns.1	. . . 4 |- X = dom dom D
2		1z 6120	. . . 4 |- 1 e. ZZ
3		nnuz 6389	. . . 4 |- NN = (ZZ>` 1)
4	1, 2, 3	iscau3 7921	. . 3 |- (D e. Met -> (F e. (Cau` D) <-> (F (_ (CC X. X) /\ A.x e. RR (0 < x -> E.j e. NN A.k e. NN (j <_ k -> ((F` j) e. X /\ (F` k) e. X /\ ((F` j)D(F` k)) < x))))))
5	4	adantr 389	. 2 |- ((D e. Met /\ F:NN-->X) -> (F e. (Cau` D) <-> (F (_ (CC X. X) /\ A.x e. RR (0 < x -> E.j e. NN A.k e. NN (j <_ k -> ((F` j) e. X /\ (F` k) e. X /\ ((F` j)D(F` k)) < x))))))
6		ax-17 970	. . . . . . . . . . . . . . . 16 |- (j e. NN -> A.k j e. NN)
7		visset 1811	. . . . . . . . . . . . . . . . . 18 |- j e. V
8		ax-17 970	. . . . . . . . . . . . . . . . . 18 |- (y e. j -> A.k y e. j)
9	7, 8	hbcsb1 2023	. . . . . . . . . . . . . . . . 17 |- (y e. [_j / k]_A -> A.k y e. [_j / k]_A)
10		ax-17 970	. . . . . . . . . . . . . . . . 17 |- (y e. (F` j) -> A.k y e. (F` j))
11	9, 10	hbeq 1564	. . . . . . . . . . . . . . . 16 |- ([_j / k]_A = (F` j) -> A.k[_j / k]_A = (F` j))
12	6, 11	hbim 1006	. . . . . . . . . . . . . . 15 |- ((j e. NN -> [_j / k]_A = (F` j)) -> A.k(j e. NN -> [_j / k]_A = (F` j)))
13		eleq1 1533	. . . . . . . . . . . . . . . 16 |- (k = j -> (k e. NN <-> j e. NN))
14		csbeq1a 2004	. . . . . . . . . . . . . . . . 17 |- (k = j -> A = [_j / k]_A)
15		fveq2 3721	. . . . . . . . . . . . . . . . 17 |- (k = j -> (F` k) = (F` j))
16	14, 15	eqeq12d 1488	. . . . . . . . . . . . . . . 16 |- (k = j -> (A = (F` k) <-> [_j / k]_A = (F` j)))
17	13, 16	imbi12d 625	. . . . . . . . . . . . . . 15 |- (k = j -> ((k e. NN -> A = (F` k)) <-> (j e. NN -> [_j / k]_A = (F` j))))
18		lmbrnns.2	. . . . . . . . . . . . . . 15 |- (k e. NN -> A = (F` k))
19	12, 17, 18	chvar 1166	. . . . . . . . . . . . . 14 |- (j e. NN -> [_j / k]_A = (F` j))
20	19, 18	opreqan12d 3976	. . . . . . . . . . . . 13 |- ((j e. NN /\ k e. NN) -> ([_j / k]_ADA) = ((F` j)D(F` k)))
21	20	breq1d 2626	. . . . . . . . . . . 12 |- ((j e. NN /\ k e. NN) -> (([_j / k]_ADA) < x <-> ((F` j)D(F` k)) < x))
22	21	adantll 392	. . . . . . . . . . 11 |- (((F:NN-->X /\ j e. NN) /\ k e. NN) -> (([_j / k]_ADA) < x <-> ((F` j)D(F` k)) < x))
23		ffvelrn 3811	. . . . . . . . . . . . . . 15 |- ((F:NN-->X /\ j e. NN) -> (F` j) e. X)
24		ffvelrn 3811	. . . . . . . . . . . . . . 15 |- ((F:NN-->X /\ k e. NN) -> (F` k) e. X)
25	23, 24	anim12i 333	. . . . . . . . . . . . . 14 |- (((F:NN-->X /\ j e. NN) /\ (F:NN-->X /\ k e. NN)) -> ((F` j) e. X /\ (F` k) e. X))
26	25	anandis 512	. . . . . . . . . . . . 13 |- ((F:NN-->X /\ (j e. NN /\ k e. NN)) -> ((F` j) e. X /\ (F` k) e. X))
27	26	anassrs 441	. . . . . . . . . . . 12 |- (((F:NN-->X /\ j e. NN) /\ k e. NN) -> ((F` j) e. X /\ (F` k) e. X))
28	27	biantrurd 726	. . . . . . . . . . 11 |- (((F:NN-->X /\ j e. NN) /\ k e. NN) -> (((F` j)D(F` k)) < x <-> (((F` j) e. X /\ (F` k) e. X) /\ ((F` j)D(F` k)) < x)))
29	22, 28	bitrd 527	. . . . . . . . . 10 |- (((F:NN-->X /\ j e. NN) /\ k e. NN) -> (([_j / k]_ADA) < x <-> (((F` j) e. X /\ (F` k) e. X) /\ ((F` j)D(F` k)) < x)))
30		df-3an 776	. . . . . . . . . 10 |- (((F` j) e. X /\ (F` k) e. X /\ ((F` j)D(F` k)) < x) <-> (((F` j) e. X /\ (F` k) e. X) /\ ((F` j)D(F` k)) < x))
31	29, 30	syl6bbr 537	. . . . . . . . 9 |- (((F:NN-->X /\ j e. NN) /\ k e. NN) -> (([_j / k]_ADA) < x <-> ((F` j) e. X /\ (F` k) e. X /\ ((F` j)D(F` k)) < x)))
32	31	imbi2d 611	. . . . . . . 8 |- (((F:NN-->X /\ j e. NN) /\ k e. NN) -> ((j <_ k -> ([_j / k]_ADA) < x) <-> (j <_ k -> ((F` j) e. X /\ (F` k) e. X /\ ((F` j)D(F` k)) < x))))
33	32	ralbidva 1658	. . . . . . 7 |- ((F:NN-->X /\ j e. NN) -> (A.k e. NN (j <_ k -> ([_j / k]_ADA) < x) <-> A.k e. NN (j <_ k -> ((F` j) e. X /\ (F` k) e. X /\ ((F` j)D(F` k)) < x))))
34	33	rexbidva 1659	. . . . . 6 |- (F:NN-->X -> (E.j e. NN A.k e. NN (j <_ k -> ([_j / k]_ADA) < x) <-> E.j e. NN A.k e. NN (j <_ k -> ((F` j) e. X /\ (F` k) e. X /\ ((F` j)D(F` k)) < x))))
35	34	ralbidv 1662	. . . . 5 |- (F:NN-->X -> (A.x e. RR+ E.j e. NN A.k e. NN (j <_ k -> ([_j / k]_ADA) < x) <-> A.x e. RR+ E.j e. NN A.k e. NN (j <_ k -> ((F` j) e. X /\ (F` k) e. X /\ ((F` j)D(F` k)) < x))))
36		ralrp 6244	. . . . 5 |- (A.x e. RR+ E.j e. NN A.k e. NN (j <_ k -> ((F` j) e. X /\ (F` k) e. X /\ ((F` j)D(F` k)) < x)) <-> A.x e. RR (0 < x -> E.j e. NN A.k e. NN (j <_ k -> ((F` j) e. X /\ (F` k) e. X /\ ((F` j)D(F` k)) < x))))
37	35, 36	syl6bb 535	. . . 4 |- (F:NN-->X -> (A.x e. RR+ E.j e. NN A.k e. NN (j <_ k -> ([_j / k]_ADA) < x) <-> A.x e. RR (0 < x -> E.j e. NN A.k e. NN (j <_ k -> ((F` j) e. X /\ (F` k) e. X /\ ((F` j)D(F` k)) < x)))))
38		fssxp 3634	. . . . . 6 |- (F:NN-->X -> F (_ (NN X. X))
39		nnsscn 5890	. . . . . . . 8 |- NN (_ CC
40		ssid 2078	. . . . . . . 8 |- X (_ X
41		ssxp 3253	. . . . . . . 8 |- ((NN (_ CC /\ X (_ X) -> (NN X. X) (_ (CC X. X))
42	39, 40, 41	mp2an 696	. . . . . . 7 |- (NN X. X) (_ (CC X. X)
43		sstr 2070	. . . . . . 7 |- ((F (_ (NN X. X) /\ (NN X. X) (_ (CC X. X)) -> F (_ (CC X. X))
44	42, 43	mpan2 695	. . . . . 6 |- (F (_ (NN X. X) -> F (_ (CC X. X))
45	38, 44	syl 10	. . . . 5 |- (F:NN-->X -> F (_ (CC X. X))
46	45	biantrurd 726	. . . 4 |- (F:NN-->X -> (A.x e. RR (0 < x -> E.j e. NN A.k e. NN (j <_ k -> ((F` j) e. X /\ (F` k) e. X /\ ((F` j)D(F` k)) < x))) <-> (F (_ (CC X. X) /\ A.x e. RR (0 < x -> E.j e. NN A.k e. NN (j <_ k -> ((F` j) e. X /\ (F` k) e. X /\ ((F` j)D(F` k)) < x))))))
47	37, 46	bitrd 527	. . 3 |- (F:NN-->X -> (A.x e. RR+ E.j e. NN A.k e. NN (j <_ k -> ([_j / k]_ADA) < x) <-> (F (_ (CC X. X) /\ A.x e. RR (0 < x -> E.j e. NN A.k e. NN (j <_ k -> ((F`