Theorem bwt2 14960

Description: The glorious Bolzano-Weierstrass theorem. Certainly the first general topology theorem ever proved. In his course Weierstrass called it a lemma. He certainly didn't know how famous this theorem would be. He used an euclidian space instead of a general compact space. And he was not conscious of the Heine-Borel property. Cantor was one of his students. He used the concept of neighborhood and limit point invented by his master when he studied the linear point sets and the rest of the general topology followed from that.

Hypothesis

Ref	Expression
bwt2.1	|- X = U.J

Assertion

Ref	Expression
bwt2	|- ((J e. Comp /\ A C_ X /\ -. A e. Fin) -> E.x e. X x e. ((limPt` J)` A))

Distinct variable groups:   x,A   x,J   x,X

Proof of Theorem bwt2

Step	Hyp	Ref	Expression
1		cmptop 14958	. . . . . . . . 9 |- Comp C_ Top
2	1	sseli 2617	. . . . . . . 8 |- (J e. Comp -> J e. Top)
3		bwt2.1	. . . . . . . . . 10 |- X = U.J
4	3	islp3 14861	. . . . . . . . 9 |- ((J e. Top /\ A C_ X /\ x e. X) -> (x e. ((limPt` J)` A) <-> A.o e. J (x e. o -> (o i^i (A \ {x})) =/= (/))))
5	4	3exp 1066	. . . . . . . 8 |- (J e. Top -> (A C_ X -> (x e. X -> (x e. ((limPt` J)` A) <-> A.o e. J (x e. o -> (o i^i (A \ {x})) =/= (/))))))
6	2, 5	syl 12	. . . . . . 7 |- (J e. Comp -> (A C_ X -> (x e. X -> (x e. ((limPt` J)` A) <-> A.o e. J (x e. o -> (o i^i (A \ {x})) =/= (/))))))
7	6	imp31 389	. . . . . 6 |- (((J e. Comp /\ A C_ X) /\ x e. X) -> (x e. ((limPt` J)` A) <-> A.o e. J (x e. o -> (o i^i (A \ {x})) =/= (/))))
8	7	rexbidva 2120	. . . . 5 |- ((J e. Comp /\ A C_ X) -> (E.x e. X x e. ((limPt` J)` A) <-> E.x e. X A.o e. J (x e. o -> (o i^i (A \ {x})) =/= (/))))
9	8	notbid 673	. . . 4 |- ((J e. Comp /\ A C_ X) -> (-. E.x e. X x e. ((limPt` J)` A) <-> -. E.x e. X A.o e. J (x e. o -> (o i^i (A \ {x})) =/= (/))))
10	9	3adant3 896	. . 3 |- ((J e. Comp /\ A C_ X /\ -. A e. Fin) -> (-. E.x e. X x e. ((limPt` J)` A) <-> -. E.x e. X A.o e. J (x e. o -> (o i^i (A \ {x})) =/= (/))))
11		uniexg 3795	. . . . . . . 8 |- (J e. Comp -> U.J e. _V)
12	11, 3	syl5eqel 1975	. . . . . . 7 |- (J e. Comp -> X e. _V)
13		eleq2 1958	. . . . . . . . 9 |- (o = (f` x) -> (x e. o <-> x e. (f` x)))
14		ineq1 2789	. . . . . . . . . . 11 |- (o = (f` x) -> (o i^i (A \ {x})) = ((f` x) i^i (A \ {x})))
15	14	eqeq1d 1892	. . . . . . . . . 10 |- (o = (f` x) -> ((o i^i (A \ {x})) = (/) <-> ((f` x) i^i (A \ {x})) = (/)))
16		nne 2021	. . . . . . . . . 10 |- (-. (o i^i (A \ {x})) =/= (/) <-> (o i^i (A \ {x})) = (/))
17	15, 16	syl5bb 591	. . . . . . . . 9 |- (o = (f` x) -> (-. (o i^i (A \ {x})) =/= (/) <-> ((f` x) i^i (A \ {x})) = (/)))
18	13, 17	anbi12d 690	. . . . . . . 8 |- (o = (f` x) -> ((x e. o /\ -. (o i^i (A \ {x})) =/= (/)) <-> (x e. (f` x) /\ ((f` x) i^i (A \ {x})) = (/))))
19	18	ac6sg 10188	. . . . . . 7 |- (X e. _V -> (A.x e. X E.o e. J (x e. o /\ -. (o i^i (A \ {x})) =/= (/)) -> E.f(f:X-->J /\ A.x e. X (x e. (f` x) /\ ((f` x) i^i (A \ {x})) = (/)))))
20	12, 19	syl 12	. . . . . 6 |- (J e. Comp -> (A.x e. X E.o e. J (x e. o /\ -. (o i^i (A \ {x})) =/= (/)) -> E.f(f:X-->J /\ A.x e. X (x e. (f` x) /\ ((f` x) i^i (A \ {x})) = (/)))))
21	20	3ad2ant1 897	. . . . 5 |- ((J e. Comp /\ A C_ X /\ -. A e. Fin) -> (A.x e. X E.o e. J (x e. o /\ -. (o i^i (A \ {x})) =/= (/)) -> E.f(f:X-->J /\ A.x e. X (x e. (f` x) /\ ((f` x) i^i (A \ {x})) = (/)))))
22		frn 4569	. . . . . . . . . . 11 |- (f:X-->J -> ran f C_ J)
23		visset 2295	. . . . . . . . . . . . 13 |- f e. _V
24	23	rnex 4209	. . . . . . . . . . . 12 |- ran f e. _V
25	24	elpw 3037	. . . . . . . . . . 11 |- (ran f e. ~PJ <-> ran f C_ J)
26	22, 25	sylibr 217	. . . . . . . . . 10 |- (f:X-->J -> ran f e. ~PJ)
27	26	adantr 425	. . . . . . . . 9 |- ((f:X-->J /\ A.x e. X (x e. (f` x) /\ ((f` x) i^i (A \ {x})) = (/))) -> ran f e. ~PJ)
28		uniss 3199	. . . . . . . . . . . 12 |- (ran f C_ J -> U.ran f C_ U.J)
29	22, 28	syl 12	. . . . . . . . . . 11 |- (f:X-->J -> U.ran f C_ U.J)
30		ax-17 1317	. . . . . . . . . . . . . . . . 17 |- ((U.ran f C_ U.J /\ f:X-->J) -> A.x(U.ran f C_ U.J /\ f:X-->J))
31	3	eqcomi 1888	. . . . . . . . . . . . . . . . . . . 20 |- U.J = X
32	31	eleq2i 1961	. . . . . . . . . . . . . . . . . . 19 |- (x e. U.J <-> x e. X)
33		pm2.27 76	. . . . . . . . . . . . . . . . . . . . 21 |- (x e. X -> ((x e. X -> (x e. (f` x) /\ ((f` x) i^i (A \ {x})) = (/))) -> (x e. (f` x) /\ ((f` x) i^i (A \ {x})) = (/))))
34		fdm 4567	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (f:X-->J -> dom f = X)
35		eleq2 1958	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (X = dom f -> (x e. X <-> x e. dom f))
36	35	biimpd 170	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (X = dom f -> (x e. X -> x e. dom f))
37		ffun 4565	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (f:X-->J -> Fun f)
38		fvelrn 4785	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ((Fun f /\ x e. dom f) -> (f` x) e. ran f)
39	38	ex 402	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (Fun f -> (x e. dom f -> (f` x) e. ran f))
40		elunii 3182	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ((x e. (f` x) /\ (f` x) e. ran f) -> x e. U.ran f)
41	40	ex 402	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (x e. (f` x) -> ((f` x) e. ran f -> x e. U.ran f))
42		idd 75	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (f:X-->J -> (x e. U.ran f -> x e. U.ran f))
43	42	a1i 8	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (U.ran f C_ U.J -> (f:X-->J -> (x e. U.ran f -> x e. U.ran f)))
44	43	com13 37	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (x e. U.ran f -> (f:X-->J -> (U.ran f C_ U.J -> x e. U.ran f)))
45	41, 44	syl6 25	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (x e. (f` x) -> ((f` x) e. ran f -> (f:X-->J -> (U.ran f C_ U.J -> x e. U.ran f))))
46	45	com4l 43	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ((f` x) e. ran f -> (f:X-->J -> (U.ran f C_ U.J -> (x e. (f` x) -> x e. U.ran f))))
47	39, 46	syl6 25	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (Fun f -> (x e. dom f -> (f:X-->J -> (U.ran f C_ U.J -> (x e. (f` x) -> x e. U.ran f)))))
48	47	com23 36	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (Fun f -> (f:X-->J -> (x e. dom f -> (U.ran f C_ U.J -> (x e. (f` x) -> x e. U.ran f)))))
49	37, 48	mpcom 60	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (f:X-->J -> (x e. dom f -> (U.ran f C_ U.J -> (x e. (f` x) -> x e. U.ran f))))
50	49	com12 14	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (x e. dom f -> (f:X-->J -> (U.ran f C_ U.J -> (x e. (f` x) -> x e. U.ran f))))
51	36, 50	syl6com 64	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (x e. X -> (X = dom f -> (f:X-->J -> (U.ran f C_ U.J -> (x e. (f` x) -> x e. U.ran f)))))
52	51	com4l 43	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (X = dom f -> (f:X-->J -> (U.ran f C_ U.J -> (x e. X -> (x e. (f` x) -> x e. U.ran f)))))
53	52	eqcoms 1887	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (dom f = X -> (f:X-->J -> (U.ran f C_ U.J -> (x e. X -> (x e. (f` x) -> x e. U.ran f)))))
54	34, 53	mpcom 60	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (f:X-->J -> (U.ran f C_ U.J -> (x e. X -> (x e. (f` x) -> x e. U.ran f))))
55	54	impcom 378	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((U.ran f C_ U.J /\ f:X-->J) -> (x e. X -> (x e. (f` x) -> x e. U.ran f)))
56	55	com13 37	. . . . . . . . . . . . . . . . . . . . . 22 |- (x e. (f` x) -> (x e. X -> ((U.ran f C_ U.J /\ f:X-->J) -> x e. U.ran f)))
57	56	adantr 425	. . . . . . . . . . . . . . . . . . . . 21 |- ((x e. (f` x) /\ ((f` x) i^i (A \ {x})) = (/)) -> (x e. X -> ((U.ran f C_ U.J /\ f:X-->J) -> x e. U.ran f)))
58	33, 57	syl6 25	. . . . . . . . . . . . . . . . . . . 20 |- (x e. X -> ((x e. X -> (x e. (f` x) /\ ((f` x) i^i (A \ {x})) = (/))) -> (x e. X -> ((U.ran f C_ U.J /\ f:X-->J) -> x e. U.ran f))))
59	58	pm2.43a 80	. . . . . . . . . . . . . . . . . . 19 |- (x e. X -> ((x e. X -> (x e. (f` x) /\ ((f` x) i^i (A \ {x})) = (/))) -> ((U.ran f C_ U.J /\ f:X-->J) -> x e. U.ran f)))
60	32, 59	sylbi 216	. . . . . . . . . . . . . . . . . 18 |- (x e. U.J -> ((x e. X -> (x e. (f` x) /\ ((f` x) i^i (A \ {x})) = (/))) -> ((U.ran f C_ U.J /\ f:X-->J) -> x e. U.ran f)))
61	60	com13 37	. . . . . . . . . . . . . . . . 17 |- ((U.ran f C_ U.J /\ f:X-->J) -> ((x e. X -> (x e. (f` x) /\ ((f` x) i^i (A \ {x})) = (/))) -> (x e. U.J -> x e. U.ran f)))
62	30, 61	alimd 1343	. . . . . . . . . . . . . . . 16 |- ((U.ran f C_ U.J /\ f:X-->J) -> (A.x(x e. X -> (x e. (f` x) /\ ((f` x) i^i (A \ {x})) = (/))) -> A.x(x e. U.J -> x e. U.ran f)))
63		df-ral 2109	. . . . . . . . . . . . . . . 16 |- (A.x e. X (x e. (f` x) /\ ((f` x) i^i (A \ {x})) = (/)) <-> A.x(x e. X -> (x e. (f` x) /\ ((f` x) i^i (A \ {x})) = (/))))
64	62, 63	syl5ib 223	. . . . . . . . . . . . . . 15 |- ((U.ran f C_ U.J /\ f:X-->J) -> (A.x e. X (x e. (f` x) /\ ((f` x) i^i (A \ {x})) = (/)) -> A.x(x e. U.J -> x e. U.ran f)))
65	64	3impia 1064	. . . . . . . . . . . . . 14 |- ((U.ran f C_ U.J /\ f:X-->J /\ A.x e. X (x e. (f` x) /\ ((f` x) i^i (A \ {x})) = (/))) -> A.x(x e. U.J -> x e. U.ran f))
66		dfss2 2610	. . . . . . . . . . . . . 14 |- (U.J C_ U.ran f <-> A.x(x e. U.J -> x e. U.ran f))
67	65, 66	sylibr 217	. . . . . . . . . . . . 13 |- ((U.ran f C_ U.J /\ f:X-->J /\ A.x e. X (x e. (f` x) /\ ((f` x) i^i (A \ {x})) = (/))) -> U.J C_ U.ran f)
68		simp1 876	. . . . . . . . . . . . 13 |- ((U.ran f C_ U.J /\ f:X-->J /\ A.x e. X (x e. (f` x) /\ ((f` x) i^i (A \ {x})) = (/))) -> U.ran f C_ U.J)
69	67, 68	eqssd 2633	. . . . . . . . . . . 12 |- ((U.ran f C_ U.J /\ f:X-->J /\ A.x e. X (x e. (f` x) /\ ((f` x) i^i (A \ {x})) = (/))) -> U.J = U.ran f)
70	69	3exp 1066	. . . . . . . . . . 11 |- (U.ran f C_ U.J -> (f:X-->J -> (A.x e. X (x e. (f` x) /\ ((f` x) i^i (A \ {x})) = (/)) -> U.J = U.ran f)))
71	29, 70	mpcom 60	. . . . . . . . . 10 |- (f:X-->J -> (A.x e. X (x e. (f` x) /\ ((f` x) i^i (A \ {x})) = (/)) -> U.J = U.ran f))
72	71	imp 377	. . . . . . . . 9 |- ((f:X-->J /\ A.x e. X (x e. (f` x) /\ ((f` x) i^i (A \ {x})) = (/))) -> U.J = U.ran f)
73	27, 72	jca 310	. . . . . . . 8 |- ((f:X-->J /\ A.x e. X (x e. (f` x) /\ ((f` x) i^i (A \ {x})) = (/))) -> (ran f e. ~PJ /\ U.J = U.ran f))
74		iscomp 10330	. . . . . . . . . . 11 |- (J e. Comp <-> (J e. Top /\ A.a e. ~P J(U.J = U.a -> E.z e. (~Pa i^i Fin)U.J = U.z)))
75		ax-17 1317	. . . . . . . . . . . . . . . . . 18 |- ((U.J = U.ran f -> E.z e. (~Pran f i^i Fin)U.J = U.z) -> A.a(U.J = U.ran f -> E.z e. (~Pran f i^i Fin)U.J = U.z))
76		unieq 3185	. . . . . . . . . . . . . . . . . . . 20 |- (a = ran f -> U.a = U.ran f)
77	76	eqeq2d 1895	. . . . . . . . . . . . . . . . . . 19 |- (a = ran f -> (U.J = U.a <-> U.J = U.ran f))
78		pweq 3036	. . . . . . . . . . . . . . . . . . . . 21 |- (a = ran f -> ~Pa = ~Pran f)
79	78	ineq1d 2795	. . . . . . . . . . . . . . . . . . . 20 |- (a = ran f -> (~Pa i^i Fin) = (~Pran f i^i Fin))
80	79	rexeqdv 2270	. . . . . . . . . . . . . . . . . . 19 |- (a = ran f -> (E.z e. (~Pa i^i Fin)U.J = U.z <-> E.z e. (~Pran f i^i Fin)U.J = U.z))
81	77, 80	imbi12d 688	. . . . . . . . . . . . . . . . . 18 |- (a = ran f -> ((U.J = U.a -> E.z e. (~Pa i^i Fin)U.J = U.z) <-> (U.J = U.ran f -> E.z e. (~Pran f i^i Fin)U.J = U.z)))
82	75, 81	rcla4 2373	. . . . . . . . . . . . . . . . 17 |- (ran f e. ~PJ -> (A.a e. ~P J(U.J = U.a -> E.z e. (~Pa i^i Fin)U.J = U.z) -> (U.J = U.ran f -> E.z e. (~Pran f i^i Fin)U.J = U.z)))
83		elin 2786	. . . . . . . . . . . . . . . . . . . 20 |- (z e. (~Pran f i^i Fin) <-> (z e. ~Pran f /\ z e. Fin))
84	31	eqeq1i 1891	. . . . . . . . . . . . . . . . . . . . . 22 |- (U.J = U.z <-> X = U.z)
85		sseq2 2639	. . . . . . . . . . . . . . . . . . . . . . 23 |- (X = U.z -> (A C_ X <-> A C_ U.z))
86		isunscov 14386	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((-. A e. Fin /\ z e. Fin /\ A C_ U.z) -> E.b e. z -. (A i^i b) e. Fin)
87	86	3exp 1066	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (-. A e. Fin -> (z e. Fin -> (A C_ U.z -> E.b e. z -. (A i^i b) e. Fin)))
88	87	com3l 38	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (z e. Fin -> (A C_ U.z -> (-. A e. Fin -> E.b e. z -. (A i^i b) e. Fin)))
89		elelpwi 3040	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ((b e. z /\ z e. ~Pran f) -> b e. ran f)
90	89	ex 402	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (b e. z -> (z e. ~Pran f -> b e. ran f))
91		ffn 4562	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (f:X-->J -> f Fn X)
92		fvelrnb 4719	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (f Fn X -> (b e. ran f <-> E.x e. X (f` x) = b))
93		ax-17 1317	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- (-. (A i^i b) e. Fin -> A.x -. (A i^i b) e. Fin)
94		hbra1 2147	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- (A.x e. X (x e. (f` x) /\ ((f` x) i^i (A \ {x})) = (/)) -> A.xA.x e. X (x e. (f` x) /\ ((f` x) i^i (A \ {x})) = (/)))
95		hbre1 2150	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- (E.x e. X x e. ((limPt` J)` A) -> A.xE.x e. X x e. ((limPt` J)` A))
96	94, 95	hbim 1354	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ((A.x e. X (x e. (f` x) /\ ((f` x) i^i (A \ {x})) = (/)) -> E.x e. X x e. ((limPt` J)` A)) -> A.x(A.x e. X (x e. (f` x) /\ ((f` x) i^i (A \ {x})) = (/)) -> E.x e. X x e. ((limPt` J)` A)))
97	93, 96	hbim 1354	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ((-. (A i^i b) e. Fin -> (A.x e. X (x e. (f` x) /\ ((f` x) i^i (A \ {x})) = (/)) -> E.x e. X x e. ((limPt` J)` A))) -> A.x(-. (A i^i b) e. Fin -> (A.x e. X (x e. (f` x) /\ ((f` x) i^i (A \ {x})) = (/)) -> E.x e. X x e. ((limPt` J)` A))))
98		ineq2 2790	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- (b = (f` x) -> (A i^i b) = (A i^i (f` x)))
99	98	eleq1d 1963	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- (b = (f` x) -> ((A i^i b) e. Fin <-> (A i^i (f` x)) e. Fin))
100	99	notbid 673	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- (b = (f` x) -> (-. (A i^i b) e. Fin <-> -. (A i^i (f` x)) e. Fin))
101	100	biimpd 170	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- (b = (f` x) -> (-. (A i^i b) e. Fin -> -. (A i^i (f` x)) e. Fin))
102	101	eqcoms 1887	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ((f` x) = b -> (-. (A i^i b) e. Fin -> -. (A i^i (f` x)) e. Fin))
103		difeq1 2717	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- (((f` x) i^i (A \ {x})) = (/) -> (((f` x) i^i (A \ {x})) \ {x}) = ((/) \ {x}))
104		0dif 2944	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- ((/) \ {x}) = (/)
105		eqtr 1904	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 |- (((((f` x) i^i (A \ {x})) \ {x}) = ((/) \ {x}) /\ ((/) \ {x}) = (/)) -> (((f` x) i^i (A \ {x})) \ {x}) = (/))
106	105	ex 402	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- ((((f` x) i^i (A \ {x})) \ {x}) = ((/) \ {x}) -> (((/) \ {x}) = (/) -> (((f` x) i^i (A \ {x})) \ {x}) = (/)))
107		difindir 2850	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 |- (((f` x) i^i (A \ {x})) \ {x}) = (((f` x) \ {x}) i^i ((A \ {x}) \ {x}))
108		eqtr 1904	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 |- (((((f` x) \ {x}) i^i ((A \ {x}) \ {x})) = (((f` x) i^i (A \ {x})) \ {x}) /\ (((f` x) i^i (A \ {x})) \ {x}) = (/)) -> (((f` x) \ {x}) i^i ((A \ {x}) \ {x})) = (/))
109		remcon 14387	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 |- ((A \ {x}) \ {x}) = (A \ {x})
110	109	ineq2i 2793	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 |- (((f` x) \ {x}) i^i ((A \ {x}) \ {x})) = (((f` x) \ {x}) i^i (A \ {x}))
111		eqtr2 1905	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 |- (((((f` x) \ {x}) i^i ((A \ {x}) \ {x})) = (((f` x) \ {x}) i^i (A \ {x})) /\ (((f` x) \ {x}) i^i ((A \ {x}) \ {x})) = (/)) -> (((f` x) \ {x}) i^i (A \ {x})) = (/))
112		difindir 2850	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 |- (((f` x) i^i A) \ {x}) = (((f` x) \ {x}) i^i (A \ {x}))
113	112	eqcomi 1888	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 |- (((f` x) \ {x}) i^i (A \ {x})) = (((f` x) i^i A) \ {x})
114		eqtr2 1905	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 |- (((((f` x) \ {x}) i^i (A \ {x})) = (((f` x) i^i A) \ {x}) /\ (((f` x) \ {x}) i^i (A \ {x})) = (/)) -> (((f` x) i^i A) \ {x}) = (/))
115		emfin 10165	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57 |- (/) e. Fin
116		eleq1 1957	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 58 |- ((((f` x) i^i A) \ {x}) = (/) -> ((((f` x) i^i A) \ {x}) e. Fin <-> (/) e. Fin))
117		incom 2787	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 60 |- ((f` x) i^i A) = (A i^i (f` x))
118	117	difeq1i 2722	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 59 |- (((f` x) i^i A) \ {x}) = ((A i^i (f` x)) \ {x})
119	118	eleq1i 1960	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 58 |- ((((f` x) i^i A) \ {x}) e. Fin <-> ((A i^i (f` x)) \ {x}) e. Fin)
120	116, 119	syl5bbr 593	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57 |- ((((f` x) i^i A) \ {x}) = (/) -> (((A i^i (f` x)) \ {x}) e. Fin <-> (/) e. Fin))
121	115, 120	mpbiri 211	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56 |- ((((f` x) i^i A) \ {x}) = (/) -> ((A i^i (f` x)) \ {x}) e. Fin)
122		snfi 5491	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 58 |- {x} e. Fin
123		islfin 10168	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 58 |- ((-. (A i^i (f` x)) e. Fin /\ {x} e. Fin) -> -. ((A i^i (f` x)) \ {x}) e. Fin)
124	122, 123	mpan2 760	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57 |- (-. (A i^i (f` x)) e. Fin -> -. ((A i^i (f` x)) \ {x}) e. Fin)
125	124	con4i 90	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56 |- (((A i^i (f` x)) \ {x}) e. Fin -> (A i^i (f` x)) e. Fin)
126	121, 125	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 |- ((((f` x) i^i A) \ {x}) = (/) -> (A i^i (f` x)) e. Fin)
127	114, 126	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 |- (((((f` x) \ {x}) i^i (A \ {x})) = (((f` x) i^i A) \ {x}) /\ (((f` x) \ {x}) i^i (A \ {x})) = (/)) -> (A i^i (f` x)) e. Fin)
128	113, 127	mpan 759	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 |- ((((f` x) \ {x}) i^i (A \ {x})) = (/) -> (A i^i (f` x)) e. Fin)
129	111, 128	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 |- (((((f` x) \ {x}) i^i ((A \ {x}) \ {x})) = (((f` x) \ {x}) i^i (A \ {x})) /\ (((f` x) \ {x}) i^i ((A \ {x}) \ {x})) = (/)) -> (A i^i (f` x)) e. Fin)
130	110, 129	mpan 759	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 |- ((((f` x) \ {x}) i^i ((A \ {x}) \ {x})) = (/) -> (A i^i (f` x)) e. Fin)
131	130	pm2.24d 120	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 |- ((((f` x) \ {x}) i^i ((A \ {x}) \ {x})) = (/) -> (-. (A i^i (f` x)) e. Fin -> E.x e. X x e. ((limPt` J)` A)))
132	108, 131	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 |- (((((f` x) \ {x}) i^i ((A \ {x}) \ {x})) = (((f` x) i^i (A \ {x})) \ {x}) /\ (((f` x) i^i (A \ {x})) \ {x}) = (/)) -> (-. (A i^i (f` x)) e. Fin -> E.x e. X x e. ((limPt` J)` A)))
133	132	ex 402	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 |- ((((f` x) \ {x}) i^i ((A \ {x}) \ {x})) = (((f` x) i^i (A \ {x})) \ {x}) -> ((((f` x) i^i (A \ {x})) \ {x}) = (/) -> (-. (A i^i (f` x)) e. Fin -> E.x e. X x e. ((limPt` J)` A))))
134	133	eqcoms 1887	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 |- ((((f` x) i^i (A \ {x})) \ {x}) = (((f` x) \ {x}) i^i ((A \ {x}) \ {x})) -> ((((f` x) i^i (A \ {x})) \ {x}) = (/) -> (-. (A i^i (f` x)) e. Fin -> E.x e. X x e. ((limPt` J)` A))))
135	107, 134	ax-mp 7	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- ((((f` x) i^i (A \ {x})) \ {x}) = (/) -> (-. (A i^i (f` x)) e. Fin -> E.x e. X x e. ((limPt` J)` A)))
136	106, 135	syl6 25	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- ((((f` x) i^i (A \ {x})) \ {x}) = ((/) \ {x}) -> (((/) \ {x}) = (/) -> (-. (A i^i (f` x)) e. Fin -> E.x e. X x e. ((limPt` J)` A))))
137	104, 136	mpi 55	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- ((((f` x) i^i (A \ {x})) \ {x}) = ((/) \ {x}) -> (-. (A i^i (f` x)) e. Fin -> E.x e. X x e. ((limPt` J)` A)))
138	103, 137	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 |- (((f` x) i^i (A \ {x})) = (/) -> (-. (A i^i (f` x)) e. Fin -> E.x e. X x e. ((limPt` J)` A)))
139	138	adantl 424	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- ((x e. (f` x) /\ ((f` x) i^i (A \ {x})) = (/)) -> (-. (A i^i (f` x)) e. Fin -> E.x e. X x e. ((limPt` J)` A)))
140	139	imim2i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- ((x e. X -> (x e. (f` x) /\ ((f` x) i^i (A \ {x})) = (/))) -> (x e. X -> (-. (A i^i (f` x)) e. Fin -> E.x e. X x e. ((limPt` J)` A))))
141	140	a4s 1330	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- (A.x(x e. X -> (x e. (f` x) /\ ((f` x) i^i (A \ {x})) = (/))) -> (x e. X -> (-. (A i^i (f` x)) e. Fin -> E.x e. X x e. ((limPt` J)` A))))
142	63, 141	sylbi 216	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- (A.x e. X (x e. (f` x) /\ ((f` x) i^i (A \ {x})) = (/)) -> (x e. X -> (-. (A i^i (f` x)) e. Fin -> E.x e. X x e. ((limPt` J)` A))))
143	142	com13 37	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- (-. (A i^i (f` x)) e. Fin -> (x e. X -> (A.x e. X (x e. (f` x) /\ ((f` x) i^i (A \ {x})) = (/)) -> E.x e. X x e. ((limPt` J)` A))))
144	102, 143	syl6 25	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ((f` x) = b -> (-. (A i^i b) e. Fin -> (x e. X -> (A.x e. X (x e. (f` x) /\ ((f` x) i^i (A \ {x})) = (/)) -> E.x e. X x e. ((limPt` J)` A)))))
145	144	com3r 39	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (x e. X -> ((f` x) = b -> (-. (A i^i b) e. Fin -> (A.x e. X (x e. (f` x) /\ ((f` x) i^i (A \ {x})) = (/)) -> E.x e. X x e. ((limPt` J)` A)))))
146	97, 145	r19.23ai 2209	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (E.x e. X (f` x) = b -> (-. (A i^i b) e. Fin -> (A.x e. X (x e. (f` x) /\ ((f` x) i^i (A \ {x})) = (/)) -> E.x e. X x e. ((limPt` J)` A))))
147	92, 146	syl6bi 231	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (f Fn X -> (b e. ran f -> (-. (A i^i b) e. Fin -> (A.x e. X (x e. (f` x) /\ ((f` x) i^i (A \ {x})) = (/)) -> E.x e. X x e. ((limPt` J)` A)))))
148	147	com24 41	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (f Fn X -> (A.x e. X (x e. (f` x) /\ ((f` x) i^i (A \ {x})) = (/)) -> (-. (A i^i b) e. Fin -> (b e. ran f -> E.x e. X x e. ((limPt` J)` A)))))
149	91, 148	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (f:X-->J -> (A.x e. X (x e. (f` x) /\ ((f` x) i^i (A \ {x})) = (/)) -> (-. (A i^i b) e. Fin -> (b e. ran f -> E.x e. X x e. ((limPt` J)` A)))))
150	149	imp 377	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ((f:X-->J /\ A.x e. X (x e. (f` x) /\ ((f` x) i^i (A \ {x})) = (/))) -> (-. (A i^i b) e. Fin -> (b e. ran f -> E.x e. X x e. ((limPt` J)` A))))
151	150	com13 37	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (b e. ran f -> (-. (A i^i b) e. Fin -> ((f:X-->J /\ A.x e. X (x e. (f` x) /\ ((f` x) i^i (A \ {x})) = (/))) -> E.x e. X x e. ((limPt` J)` A))))
152	90, 151	syl6 25	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (b e. z -> (z e. ~Pran f -> (-. (A i^i b) e. Fin -> ((f:X-->J /\ A.x e. X (x e. (f` x) /\ ((f` x) i^i (A \ {x})) = (/))) -> E.x e. X x e. ((limPt` J)` A)))))
153	152	com23 36	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (b e. z -> (-. (A i^i b) e. Fin -> (z e. ~Pran f -> ((f:X-->J /\ A.x e. X (x e. (f` x) /\ ((f` x) i^i (A \ {x})) = (/))) -> E.x e. X x e. ((limPt` J)` A)))))
154	153	r19.23aiv 2211	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (E.b e. z -. (A i^i b) e. Fin -> (z e. ~Pran f -> ((f:X-->J /\ A.x e. X (x e. (f` x) /\ ((f` x) i^i (A \ {x})) = (/))) -> E.x e. X x e. ((limPt` J)` A))))
155	88, 154	syl8 27	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (z e. Fin -> (A C_ U.z -> (-. A e. Fin -> (z e. ~Pran f -> ((f:X-->J /\ A.x e. X (x e. (f` x) /\ ((f` x) i^i (A \ {x})) = (/))) -> E.x e. X x e. ((limPt` J)` A))))))
156	155	com4r 45	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (z e. ~Pran f -> (z e. Fin -> (A C_ U.z -> (-. A e. Fin -> ((f:X-->J /\ A.x e. X (x e. (f` x) /\ ((f` x) i^i (A \ {x})) = (/))) -> E.x e. X x e. ((limPt` J)` A))))))
157	156	imp 377	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((z e. ~Pran f /\ z e. Fin) -> (A C_ U.z -> (-. A e. Fin -> ((f:X-->J /\ A.x e. X (x e. (f` x) /\ ((f` x) i^i (A \ {x})) = (/))) -> E.x e. X x e. ((limPt` J)` A)))))
158	157	com12 14	. . . . . . . . . . . . . . . . . . . . . . 23 |- (A C_ U.z -> ((z e. ~Pran f /\ z e. Fin) -> (-. A e. Fin -> ((f:X-->J /\ A.x e. X (x e. (f` x) /\ ((f` x) i^i (A \ {x})) = (/))) -> E.x e. X x e. ((limPt` J)` A)))))
159	85, 158	syl6bi 231	. . . . . . . . . . . . . . . . . . . . . 22 |- (X = U.z -> (A C_ X -> ((z e. ~Pran f /\ z e. Fin) -> (-. A e. Fin -> ((f:X-->J /\ A.x e. X (x e. (f` x) /\ ((f` x) i^i (A \ {x})) = (/))) -> E.x e. X x e. ((limPt` J)` A))))))
160	84, 159	sylbi 216	. . . . . . . . . . . . . . . . . . . . 21 |- (U.J = U.z -> (A C_ X -> ((z e. ~Pran f /\ z e. Fin) -> (-. A e. Fin -> ((f:X-->J /\ A.x e. X (x e. (f` x) /\ ((f` x) i^i (A \ {x})) = (/))) -> E.x e. X x e. ((limPt` J)` A))))))
161	160	com3r 39	. . . . . . . . . . . . . . . . . . . 20 |- ((z e. ~Pran f /\ z e. Fin) -> (U.J = U.z -> (A C_ X -> (-. A e. Fin -> ((f:X-->J /\ A.x e. X (x e. (f` x) /\ ((f` x) i^i (A \ {x})) = (/))) -> E.x e. X x e. ((limPt` J)` A))))))
162	83, 161	sylbi 216	. . . . . . . . . . . . . . . . . . 19 |- (z e. (~Pran f i^i Fin) -> (U.J = U.z -> (A C_ X -> (-. A e. Fin -> ((f:X-->J /\ A.x e. X (x e. (f` x) /\ ((f` x) i^i (A \ {x})) = (/))) -> E.x e. X x e. ((limPt` J)` A))))))
163	162	r19.23aiv 2211	. . . . . . . . . . . . . . . . . 18 |- (E.z e. (~Pran f i^i Fin)U.J = U.z -> (A C_ X -> (-. A e. Fin -> ((f:X-->J /\ A.x e. X (x e. (f` x) /\ ((f` x) i^i (A \ {x})) = (/))) -> E.x e. X x e. ((limPt` J)` A)))))
164	163	3impd 1082	. . . . . . . . . . . . . . . . 17 |- (E.z e. (~Pran f i^i Fin)U.J = U.z -> ((A C_ X /\ -. A e. Fin /\ (f:X-->J /\ A.x e. X (x e. (f` x) /\ ((f` x) i^i (A \ {x})) = (/)))) -> E.x e. X x e. ((limPt` J)` A)))
165	82, 164	syl8 27	. . . . . . . . . . . . . . . 16 |- (ran f e. ~PJ -> (A.a e. ~P J(U.J = U.a -> E.z e. (~Pa i^i Fin)U.J = U.z) -> (U.J = U.ran f -> ((A C_ X /\ -. A e. Fin /\ (f:X-->J /\ A.x e. X (x e. (f` x) /\ ((f` x) i^i (A \ {x})) = (/)))) -> E.x e. X x e. ((limPt` J)` A)))))
166	165	com23 36	. . . . . . . . . . . . . . 15 |- (ran f e. ~PJ -> (U.J = U.ran f -> (A.a e. ~P J(U.J = U.a -> E.z e. (~Pa i^i Fin)U.J = U.z) -> ((A C_ X /\ -. A e. Fin /\ (f:X-->J /\ A.x e. X (x e. (f` x) /\ ((f` x) i^i (A \ {x})) = (/)))) -> E.x e. X x e. ((limPt` J)` A)))))
167	166	imp 377	. . . . . . . . . . . . . 14 |- ((ran f e. ~PJ /\ U.J = U.ran f) -> (A.a e. ~P J(U.J = U.a -> E.z e. (~Pa i^i Fin)U.J = U.z) -> ((A C_ X /\ -. A e. Fin /\ (f:X-->J /\ A.x e. X (x e. (f` x) /\ ((f` x) i^i (A \ {x})) = (/)))) -> E.x e. X x e. ((limPt` J)` A))))
168	167	com3l 38	. . . . . . . . . . . . 13 |- (A.a e. ~P J(U.J = U.a -> E.z e. (~Pa i^i Fin)U.J = U.z) -> ((A C_ X /\ -. A e. Fin /\ (f:X-->J /\ A.x e. X (x e. (f` x) /\ ((f` x) i^i (A \ {x})) = (/)))) -> ((ran f e. ~PJ /\ U.J = U.ran f) -> E.x e. X x e. ((limPt` J)` A))))
169	168	3expd 1085	. . . . . . . . . . . 12 |- (A.a e. ~P J(U.J = U.a -> E.z e. (~Pa i^i Fin)U.J = U.z) -> (A C_ X -> (-. A e. Fin -> ((f:X-->J /\ A.x e. X (x e. (f` x) /\ ((f` x) i^i (A \ {x})) = (/))) -> ((ran f e. ~PJ /\ U.J = U.ran f) -> E.x e. X x e. ((limPt` J)` A))))))
170	169	adantl 424	. . . . . . . . . . 11 |- ((J e. Top /\ A.a e. ~P J(U.J = U.a -> E.z e. (~Pa i^i Fin)U.J = U.z)) -> (A C_ X -> (-. A e. Fin -> ((f:X-->J /\ A.x e. X (x e. (f` x) /\ ((f` x) i^i (A \ {x})) = (/))) -> ((ran f e. ~PJ /\ U.J = U.ran f) -> E.x e. X x e. ((limPt` J)` A))))))
171	74, 170	sylbi 216	. . . . . . . . . 10 |- (J e. Comp -> (A C_ X -> (-. A e. Fin -> ((f:X-->J /\ A.x e. X (x e. (f` x) /\ ((f` x) i^i (A \ {x})) = (/))) -> ((ran f e. ~PJ /\ U.J = U.ran f) -> E.x e. X x e. ((limPt` J)` A))))))
172	171	3imp 1061	. . . . . . . . 9 |- ((J e. Comp /\ A C_ X /\ -. A e. Fin) -> ((f:X-->J /\ A.x e. X (x e. (f` x) /\ ((f` x) i^i (A \ {x})) = (/))) -> ((ran f e. ~PJ /\ U.J = U.ran f) -> E.x e. X x e. ((limPt` J)` A))))
173	172	com13 37	. . . . . . . 8 |- ((ran f e. ~PJ /\ U.J = U.ran f) -> ((f:X-->J /\ A.x e. X (x e. (f` x) /\ ((f` x) i^i (A \ {x})) = (/))) -> ((J e. Comp /\ A C_ X /\ -. A e. Fin) -> E.x e. X x e. ((limPt` J)` A))))
174	73, 173	mpcom 60	. . . . . . 7 |- ((f:X-->J /\ A.x e. X (x e. (f` x) /\ ((f` x) i^i (A \ {x})) = (/))) -> ((J e. Comp /\ A C_ X /\ -. A e. Fin) -> E.x e. X x e. ((limPt` J)` A)))
175	174	19.23aiv 1674	. . . . . 6 |- (E.f(f:X-->J /\ A.x e. X (x e. (f` x) /\ ((f` x) i^i (A \ {x})) = (/))) -> ((J e. Comp /\ A C_ X /\ -. A e. Fin) -> E.x e. X x e. ((limPt` J)` A)))
176	175	com12 14	. . . . 5 |- ((J e. Comp /\ A C_ X /\ -. A e. Fin) -> (E.f(f:X-->J /\ A.x e. X (x e. (f` x) /\ ((f` x) i^i (A \ {x})) = (/))) -> E.x e. X x e. ((limPt` J)` A)))
177	21, 176	syld 30	. . . 4 |- ((J e. Comp /\ A C_ X /\ -. A e. Fin) -> (A.x e. X E.o e. J (x e. o /\ -. (o i^i (A \ {x})) =/= (/)) -> E.x e. X x e. ((limPt` J)` A)))
178		negcmpprcal1 14275	. . . 4 |- (-. E.x e. X A.o e. J (x e. o -> (o i^i (A \ {x})) =/= (/)) <-> A.x e. X E.o e. J (x e. o /\ -. (o i^i (A \ {x})) =/= (/)))
179	177, 178	syl5ib 223	. . 3 |- ((J e. Comp /\ A C_ X /\ -. A e. Fin) -> (-. E.x e. X A.o e. J (x e. o -> (o i^i (A \ {x})) =/= (/)) -> E.x e. X x e. ((limPt` J)` A)))
180	10, 179	sylbid 220	. 2 |- ((J e. Comp /\ A C_ X /\ -. A e. Fin) -> (-. E.x e. X x e. ((limPt` J)` A) -> E.x e. X x e. ((limPt` J)` A)))
181	180	pm2.01bd 14274	1 |- ((J e. Comp /\ A C_ X /\ -. A e. Fin) -> E.x e. X x e. ((limPt` J)` A))

Syntax hints:  -. wn 2   -> wi 3   <-> wb 163   /\ wa 240   /\ w3a 858  A.wal 1296   = wceq 1298   e. wcel 1300  E.wex 1326   =/= wne 2017  A.wral 2105  E.wrex 2106  _Vcvv 2292   \ cdif 2590   i^i cin 2592   C_ wss 2593  (/)c0 2875  ~Pcpw 3032  {csn 3044  U.cuni 3177  dom cdm 3986  ran crn 3987  Fun wfun 3992   Fn wfn 3993  -->wf 3994  ` cfv 3998  Fincfn 5426  Topctop 8857  limPtclp 9016  Compccomp 10328

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-13 1311  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-rep 3428  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524  ax-un 3790  ax-reg 5695  ax-inf2 5731  ax-ac 5906

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3or 859  df-3an 860  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-ral 2109  df-rex 2110  df-reu 2111  df-rab 2112  df-v 2294  df-sbc 2454  df-csb 2541  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-pss 2607  df-nul 2876  df-if 2983  df-pw 3035  df-sn 3049  df-pr 3050  df-tp 3052  df-op 3053  df-uni 3178  df-int 3215  df-iun 3257  df-iin 3258  df-br 3339  df-opab 3396  df-tr 3412  df-eprel 3583  df-id 3586  df-po 3591  df-so 3604  df-fr 3625  df-we 3644  df-ord 3660  df-on 3661  df-lim 3662  df-suc 3663  df-om 3950  df-xp 4000  df-rel 4001  df-cnv 4002  df-co 4003  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fun 4008  df-fn 4009  df-f 4010  df-f1 4011  df-fo 4012  df-f1o 4013  df-fv 4014  df-opr 4886  df-oprab 4887  df-rdg 5140  df-1o 5177  df-oadd 5179  df-er 5318  df-en 5427  df-dom 5428  df-fin 5430  df-r1 5750  df-rank 5751  df-top 8861  df-cld 8939  df-ntr 8940  df-cls 8941  df-lp 9017  df-comp 10329

Copyright terms: Public domain