Theorem cnpnei 9043

Description: A condition for continuity at a point in terms of neighborhoods. (Contributed by Jeff Hankins, 7-Sep-2009.)

Hypotheses

Ref	Expression
cnpnei.1	|- X = U.J
cnpnei.2	|- Y = U.K

Assertion

Ref	Expression
cnpnei	|- (((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) -> (F e. ((J CnP K)` A) <-> A.y e. ((nei` K)` {(F` A)})(`'F"y) e. ((nei` J)` {A})))

Distinct variable groups:   y,A   y,F   y,J   y,K   y,X   y,Y

Proof of Theorem cnpnei

Step	Hyp	Ref	Expression
1		cnpnei.1	. . . . . . . 8 |- X = U.J
2	1	isneip 8996	. . . . . . 7 |- ((J e. Top /\ A e. X) -> ((`'F"y) e. ((nei` J)` {A}) <-> ((`'F"y) C_ X /\ E.o e. J (A e. o /\ o C_ (`'F"y)))))
3	2	3ad2antl1 1038	. . . . . 6 |- (((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) -> ((`'F"y) e. ((nei` J)` {A}) <-> ((`'F"y) C_ X /\ E.o e. J (A e. o /\ o C_ (`'F"y)))))
4	3	adantr 425	. . . . 5 |- ((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (F e. ((J CnP K)` A) /\ y e. ((nei` K)` {(F` A)}))) -> ((`'F"y) e. ((nei` J)` {A}) <-> ((`'F"y) C_ X /\ E.o e. J (A e. o /\ o C_ (`'F"y)))))
5		fdm 4567	. . . . . . . 8 |- (F:X-->Y -> dom F = X)
6		cnvimass 4286	. . . . . . . . 9 |- (`'F"y) C_ dom F
7		sseq2 2639	. . . . . . . . 9 |- (dom F = X -> ((`'F"y) C_ dom F <-> (`'F"y) C_ X))
8	6, 7	mpbii 210	. . . . . . . 8 |- (dom F = X -> (`'F"y) C_ X)
9	5, 8	syl 12	. . . . . . 7 |- (F:X-->Y -> (`'F"y) C_ X)
10	9	3ad2ant3 899	. . . . . 6 |- ((J e. Top /\ K e. Top /\ F:X-->Y) -> (`'F"y) C_ X)
11	10	ad2antrr 440	. . . . 5 |- ((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (F e. ((J CnP K)` A) /\ y e. ((nei` K)` {(F` A)}))) -> (`'F"y) C_ X)
12		neii2 8998	. . . . . . . 8 |- ((K e. Top /\ y e. ((nei` K)` {(F` A)})) -> E.g e. K ({(F` A)} C_ g /\ g C_ y))
13	12	3ad2antl2 1039	. . . . . . 7 |- (((J e. Top /\ K e. Top /\ F:X-->Y) /\ y e. ((nei` K)` {(F` A)})) -> E.g e. K ({(F` A)} C_ g /\ g C_ y))
14	13	ad2ant2rl 447	. . . . . 6 |- ((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (F e. ((J CnP K)` A) /\ y e. ((nei` K)` {(F` A)}))) -> E.g e. K ({(F` A)} C_ g /\ g C_ y))
15		simp1 876	. . . . . . . . . . . . 13 |- ((J e. Top /\ K e. Top /\ F:X-->Y) -> J e. Top)
16	15	adantr 425	. . . . . . . . . . . 12 |- (((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) -> J e. Top)
17		simp2 877	. . . . . . . . . . . . 13 |- ((J e. Top /\ K e. Top /\ F:X-->Y) -> K e. Top)
18	17	adantr 425	. . . . . . . . . . . 12 |- (((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) -> K e. Top)
19		simpr 350	. . . . . . . . . . . 12 |- (((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) -> A e. X)
20	16, 18, 19	3jca 1050	. . . . . . . . . . 11 |- (((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) -> (J e. Top /\ K e. Top /\ A e. X))
21	20	ad2antrr 440	. . . . . . . . . 10 |- (((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (F e. ((J CnP K)` A) /\ y e. ((nei` K)` {(F` A)}))) /\ (g e. K /\ ({(F` A)} C_ g /\ g C_ y))) -> (J e. Top /\ K e. Top /\ A e. X))
22		simpll 448	. . . . . . . . . . . 12 |- (((F e. ((J CnP K)` A) /\ y e. ((nei` K)` {(F` A)})) /\ (g e. K /\ ({(F` A)} C_ g /\ g C_ y))) -> F e. ((J CnP K)` A))
23		simprl 450	. . . . . . . . . . . 12 |- (((F e. ((J CnP K)` A) /\ y e. ((nei` K)` {(F` A)})) /\ (g e. K /\ ({(F` A)} C_ g /\ g C_ y))) -> g e. K)
24		fvex 4689	. . . . . . . . . . . . . . . 16 |- (F` A) e. _V
25	24	snss 3122	. . . . . . . . . . . . . . 15 |- ((F` A) e. g <-> {(F` A)} C_ g)
26	25	biimpri 169	. . . . . . . . . . . . . 14 |- ({(F` A)} C_ g -> (F` A) e. g)
27	26	adantr 425	. . . . . . . . . . . . 13 |- (({(F` A)} C_ g /\ g C_ y) -> (F` A) e. g)
28	27	ad2antll 443	. . . . . . . . . . . 12 |- (((F e. ((J CnP K)` A) /\ y e. ((nei` K)` {(F` A)})) /\ (g e. K /\ ({(F` A)} C_ g /\ g C_ y))) -> (F` A) e. g)
29	22, 23, 28	3jca 1050	. . . . . . . . . . 11 |- (((F e. ((J CnP K)` A) /\ y e. ((nei` K)` {(F` A)})) /\ (g e. K /\ ({(F` A)} C_ g /\ g C_ y))) -> (F e. ((J CnP K)` A) /\ g e. K /\ (F` A) e. g))
30	29	adantll 428	. . . . . . . . . 10 |- (((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (F e. ((J CnP K)` A) /\ y e. ((nei` K)` {(F` A)}))) /\ (g e. K /\ ({(F` A)} C_ g /\ g C_ y))) -> (F e. ((J CnP K)` A) /\ g e. K /\ (F` A) e. g))
31	1	cnpimaex 9041	. . . . . . . . . 10 |- (((J e. Top /\ K e. Top /\ A e. X) /\ (F e. ((J CnP K)` A) /\ g e. K /\ (F` A) e. g)) -> E.o e. J (A e. o /\ (F"o) C_ g))
32	21, 30, 31	syl11anc 524	. . . . . . . . 9 |- (((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (F e. ((J CnP K)` A) /\ y e. ((nei` K)` {(F` A)}))) /\ (g e. K /\ ({(F` A)} C_ g /\ g C_ y))) -> E.o e. J (A e. o /\ (F"o) C_ g))
33		sstr2 2623	. . . . . . . . . . . . . . 15 |- ((F"o) C_ g -> (g C_ y -> (F"o) C_ y))
34	33	com12 14	. . . . . . . . . . . . . 14 |- (g C_ y -> ((F"o) C_ g -> (F"o) C_ y))
35	34	ad2antll 443	. . . . . . . . . . . . 13 |- ((g e. K /\ ({(F` A)} C_ g /\ g C_ y)) -> ((F"o) C_ g -> (F"o) C_ y))
36	35	ad2antlr 441	. . . . . . . . . . . 12 |- ((((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (F e. ((J CnP K)` A) /\ y e. ((nei` K)` {(F` A)}))) /\ (g e. K /\ ({(F` A)} C_ g /\ g C_ y))) /\ o e. J) -> ((F"o) C_ g -> (F"o) C_ y))
37		ffun 4565	. . . . . . . . . . . . . . . 16 |- (F:X-->Y -> Fun F)
38	37	3ad2ant3 899	. . . . . . . . . . . . . . 15 |- ((J e. Top /\ K e. Top /\ F:X-->Y) -> Fun F)
39	38	ad2antrr 440	. . . . . . . . . . . . . 14 |- ((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (F e. ((J CnP K)` A) /\ y e. ((nei` K)` {(F` A)}))) -> Fun F)
40	39	ad2antrr 440	. . . . . . . . . . . . 13 |- ((((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (F e. ((J CnP K)` A) /\ y e. ((nei` K)` {(F` A)}))) /\ (g e. K /\ ({(F` A)} C_ g /\ g C_ y))) /\ o e. J) -> Fun F)
41	1	eltopss 8872	. . . . . . . . . . . . . . . . . . 19 |- ((J e. Top /\ o e. J) -> o C_ X)
42	41	adantlr 429	. . . . . . . . . . . . . . . . . 18 |- (((J e. Top /\ F:X-->Y) /\ o e. J) -> o C_ X)
43	5	sseq2d 2645	. . . . . . . . . . . . . . . . . . 19 |- (F:X-->Y -> (o C_ dom F <-> o C_ X))
44	43	ad2antlr 441	. . . . . . . . . . . . . . . . . 18 |- (((J e. Top /\ F:X-->Y) /\ o e. J) -> (o C_ dom F <-> o C_ X))
45	42, 44	mpbird 213	. . . . . . . . . . . . . . . . 17 |- (((J e. Top /\ F:X-->Y) /\ o e. J) -> o C_ dom F)
46	45	3adantl2 1033	. . . . . . . . . . . . . . . 16 |- (((J e. Top /\ K e. Top /\ F:X-->Y) /\ o e. J) -> o C_ dom F)
47	46	adantlr 429	. . . . . . . . . . . . . . 15 |- ((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ o e. J) -> o C_ dom F)
48	47	adantlr 429	. . . . . . . . . . . . . 14 |- (((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (F e. ((J CnP K)` A) /\ y e. ((nei` K)` {(F` A)}))) /\ o e. J) -> o C_ dom F)
49	48	adantlr 429	. . . . . . . . . . . . 13 |- ((((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (F e. ((J CnP K)` A) /\ y e. ((nei` K)` {(F` A)}))) /\ (g e. K /\ ({(F` A)} C_ g /\ g C_ y))) /\ o e. J) -> o C_ dom F)
50		funimass3 4779	. . . . . . . . . . . . 13 |- ((Fun F /\ o C_ dom F) -> ((F"o) C_ y <-> o C_ (`'F"y)))
51	40, 49, 50	syl11anc 524	. . . . . . . . . . . 12 |- ((((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (F e. ((J CnP K)` A) /\ y e. ((nei` K)` {(F` A)}))) /\ (g e. K /\ ({(F` A)} C_ g /\ g C_ y))) /\ o e. J) -> ((F"o) C_ y <-> o C_ (`'F"y)))
52	36, 51	sylibd 219	. . . . . . . . . . 11 |- ((((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (F e. ((J CnP K)` A) /\ y e. ((nei` K)` {(F` A)}))) /\ (g e. K /\ ({(F` A)} C_ g /\ g C_ y))) /\ o e. J) -> ((F"o) C_ g -> o C_ (`'F"y)))
53	52	anim2d 620	. . . . . . . . . 10 |- ((((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (F e. ((J CnP K)` A) /\ y e. ((nei` K)` {(F` A)}))) /\ (g e. K /\ ({(F` A)} C_ g /\ g C_ y))) /\ o e. J) -> ((A e. o /\ (F"o) C_ g) -> (A e. o /\ o C_ (`'F"y))))
54	53	reximdva 2203	. . . . . . . . 9 |- (((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (F e. ((J CnP K)` A) /\ y e. ((nei` K)` {(F` A)}))) /\ (g e. K /\ ({(F` A)} C_ g /\ g C_ y))) -> (E.o e. J (A e. o /\ (F"o) C_ g) -> E.o e. J (A e. o /\ o C_ (`'F"y))))
55	32, 54	mpd 29	. . . . . . . 8 |- (((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (F e. ((J CnP K)` A) /\ y e. ((nei` K)` {(F` A)}))) /\ (g e. K /\ ({(F` A)} C_ g /\ g C_ y))) -> E.o e. J (A e. o /\ o C_ (`'F"y)))
56	55	exp32 408	. . . . . . 7 |- ((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (F e. ((J CnP K)` A) /\ y e. ((nei` K)` {(F` A)}))) -> (g e. K -> (({(F` A)} C_ g /\ g C_ y) -> E.o e. J (A e. o /\ o C_ (`'F"y)))))
57	56	r19.23adv 2215	. . . . . 6 |- ((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (F e. ((J CnP K)` A) /\ y e. ((nei` K)` {(F` A)}))) -> (E.g e. K ({(F` A)} C_ g /\ g C_ y) -> E.o e. J (A e. o /\ o C_ (`'F"y))))
58	14, 57	mpd 29	. . . . 5 |- ((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (F e. ((J CnP K)` A) /\ y e. ((nei` K)` {(F` A)}))) -> E.o e. J (A e. o /\ o C_ (`'F"y)))
59	4, 11, 58	mpbir2and 802	. . . 4 |- ((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (F e. ((J CnP K)` A) /\ y e. ((nei` K)` {(F` A)}))) -> (`'F"y) e. ((nei` J)` {A}))
60	59	exp32 408	. . 3 |- (((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) -> (F e. ((J CnP K)` A) -> (y e. ((nei` K)` {(F` A)}) -> (`'F"y) e. ((nei` J)` {A}))))
61	60	r19.21adv 2181	. 2 |- (((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) -> (F e. ((J CnP K)` A) -> A.y e. ((nei` K)` {(F` A)})(`'F"y) e. ((nei` J)` {A})))
62		cnpnei.2	. . . . . . . 8 |- Y = U.K
63	1, 62	iscnp 9036	. . . . . . 7 |- ((J e. Top /\ K e. Top /\ A e. X) -> (F e. ((J CnP K)` A) <-> (F:X-->Y /\ A.o e. K ((F` A) e. o -> E.g e. J (A e. g /\ (F"g) C_ o)))))
64	63	3expa 1067	. . . . . 6 |- (((J e. Top /\ K e. Top) /\ A e. X) -> (F e. ((J CnP K)` A) <-> (F:X-->Y /\ A.o e. K ((F` A) e. o -> E.g e. J (A e. g /\ (F"g) C_ o)))))
65	64	3adantl3 1034	. . . . 5 |- (((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) -> (F e. ((J CnP K)` A) <-> (F:X-->Y /\ A.o e. K ((F` A) e. o -> E.g e. J (A e. g /\ (F"g) C_ o)))))
66	65	adantr 425	. . . 4 |- ((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ A.y e. ((nei` K)` {(F` A)})(`'F"y) e. ((nei` J)` {A})) -> (F e. ((J CnP K)` A) <-> (F:X-->Y /\ A.o e. K ((F` A) e. o -> E.g e. J (A e. g /\ (F"g) C_ o)))))
67		simpll3 917	. . . 4 |- ((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ A.y e. ((nei` K)` {(F` A)})(`'F"y) e. ((nei` J)` {A})) -> F:X-->Y)
68		opnneip 9009	. . . . . . . . . . . . . 14 |- ((K e. Top /\ o e. K /\ (F` A) e. o) -> o e. ((nei` K)` {(F` A)}))
69		imaeq2 4260	. . . . . . . . . . . . . . . 16 |- (y = o -> (`'F"y) = (`'F"o))
70	69	eleq1d 1963	. . . . . . . . . . . . . . 15 |- (y = o -> ((`'F"y) e. ((nei` J)` {A}) <-> (`'F"o) e. ((nei` J)` {A})))
71	70	rcla4v 2376	. . . . . . . . . . . . . 14 |- (o e. ((nei` K)` {(F` A)}) -> (A.y e. ((nei` K)` {(F` A)})(`'F"y) e. ((nei` J)` {A}) -> (`'F"o) e. ((nei` J)` {A})))
72	68, 71	syl 12	. . . . . . . . . . . . 13 |- ((K e. Top /\ o e. K /\ (F` A) e. o) -> (A.y e. ((nei` K)` {(F` A)})(`'F"y) e. ((nei` J)` {A}) -> (`'F"o) e. ((nei` J)` {A})))
73	72	3com23 1074	. . . . . . . . . . . 12 |- ((K e. Top /\ (F` A) e. o /\ o e. K) -> (A.y e. ((nei` K)` {(F` A)})(`'F"y) e. ((nei` J)` {A}) -> (`'F"o) e. ((nei` J)` {A})))
74	73	3expb 1068	. . . . . . . . . . 11 |- ((K e. Top /\ ((F` A) e. o /\ o e. K)) -> (A.y e. ((nei` K)` {(F` A)})(`'F"y) e. ((nei` J)` {A}) -> (`'F"o) e. ((nei` J)` {A})))
75	74	3ad2antl2 1039	. . . . . . . . . 10 |- (((J e. Top /\ K e. Top /\ F:X-->Y) /\ ((F` A) e. o /\ o e. K)) -> (A.y e. ((nei` K)` {(F` A)})(`'F"y) e. ((nei` J)` {A}) -> (`'F"o) e. ((nei` J)` {A})))
76	75	adantlr 429	. . . . . . . . 9 |- ((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ ((F` A) e. o /\ o e. K)) -> (A.y e. ((nei` K)` {(F` A)})(`'F"y) e. ((nei` J)` {A}) -> (`'F"o) e. ((nei` J)` {A})))
77		neii2 8998	. . . . . . . . . . . 12 |- ((J e. Top /\ (`'F"o) e. ((nei` J)` {A})) -> E.g e. J ({A} C_ g /\ g C_ (`'F"o)))
78	77	ex 402	. . . . . . . . . . 11 |- (J e. Top -> ((`'F"o) e. ((nei` J)` {A}) -> E.g e. J ({A} C_ g /\ g C_ (`'F"o))))
79	78	3ad2ant1 897	. . . . . . . . . 10 |- ((J e. Top /\ K e. Top /\ F:X-->Y) -> ((`'F"o) e. ((nei` J)` {A}) -> E.g e. J ({A} C_ g /\ g C_ (`'F"o))))
80	79	ad2antrr 440	. . . . . . . . 9 |- ((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ ((F` A) e. o /\ o e. K)) -> ((`'F"o) e. ((nei` J)` {A}) -> E.g e. J ({A} C_ g /\ g C_ (`'F"o))))
81		snssg 3124	. . . . . . . . . . . . . 14 |- (A e. X -> (A e. g <-> {A} C_ g))
82	81	adantl 424	. . . . . . . . . . . . 13 |- (((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) -> (A e. g <-> {A} C_ g))
83	82	ad2antrr 440	. . . . . . . . . . . 12 |- (((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ ((F` A) e. o /\ o e. K)) /\ g e. J) -> (A e. g <-> {A} C_ g))
84	38	adantr 425	. . . . . . . . . . . . . 14 |- (((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) -> Fun F)
85	84	ad2antrr 440	. . . . . . . . . . . . 13 |- (((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ ((F` A) e. o /\ o e. K)) /\ g e. J) -> Fun F)
86	1	eltopss 8872	. . . . . . . . . . . . . . . . 17 |- ((J e. Top /\ g e. J) -> g C_ X)
87	86	3ad2antl1 1038	. . . . . . . . . . . . . . . 16 |- (((J e. Top /\ K e. Top /\ F:X-->Y) /\ g e. J) -> g C_ X)
88	5	sseq2d 2645	. . . . . . . . . . . . . . . . . 18 |- (F:X-->Y -> (g C_ dom F <-> g C_ X))
89	88	3ad2ant3 899	. . . . . . . . . . . . . . . . 17 |- ((J e. Top /\ K e. Top /\ F:X-->Y) -> (g C_ dom F <-> g C_ X))
90	89	biimpar 461	. . . . . . . . . . . . . . . 16 |- (((J e. Top /\ K e. Top /\ F:X-->Y) /\ g C_ X) -> g C_ dom F)
91	87, 90	syldan 516	. . . . . . . . . . . . . . 15 |- (((J e. Top /\ K e. Top /\ F:X-->Y) /\ g e. J) -> g C_ dom F)
92	91	adantlr 429	. . . . . . . . . . . . . 14 |- ((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ g e. J) -> g C_ dom F)
93	92	adantlr 429	. . . . . . . . . . . . 13 |- (((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ ((F` A) e. o /\ o e. K)) /\ g e. J) -> g C_ dom F)
94		funimass3 4779	. . . . . . . . . . . . 13 |- ((Fun F /\ g C_ dom F) -> ((F"g) C_ o <-> g C_ (`'F"o)))
95	85, 93, 94	syl11anc 524	. . . . . . . . . . . 12 |- (((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ ((F` A) e. o /\ o e. K)) /\ g e. J) -> ((F"g) C_ o <-> g C_ (`'F"o)))
96	83, 95	anbi12d 690	. . . . . . . . . . 11 |- (((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ ((F` A) e. o /\ o e. K)) /\ g e. J) -> ((A e. g /\ (F"g) C_ o) <-> ({A} C_ g /\ g C_ (`'F"o))))
97	96	biimprd 171	. . . . . . . . . 10 |- (((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ ((F` A) e. o /\ o e. K)) /\ g e. J) -> (({A} C_ g /\ g C_ (`'F"o)) -> (A e. g /\ (F"g) C_ o)))
98	97	reximdva 2203	. . . . . . . . 9 |- ((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ ((F` A) e. o /\ o e. K)) -> (E.g e. J ({A} C_ g /\ g C_ (`'F"o)) -> E.g e. J (A e. g /\ (F"g) C_ o)))
99	76, 80, 98	3syld 31	. . . . . . . 8 |- ((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ ((F` A) e. o /\ o e. K)) -> (A.y e. ((nei` K)` {(F` A)})(`'F"y) e. ((nei` J)` {A}) -> E.g e. J (A e. g /\ (F"g) C_ o)))
100	99	exp32 408	. . . . . . 7 |- (((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) -> ((F` A) e. o -> (o e. K -> (A.y e. ((nei` K)` {(F` A)})(`'F"y) e. ((nei` J)` {A}) -> E.g e. J (A e. g /\ (F"g) C_ o)))))
101	100	com24 41	. . . . . 6 |- (((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) -> (A.y e. ((nei` K)` {(F` A)})(`'F"y) e. ((nei` J)` {A}) -> (o e. K -> ((F` A) e. o -> E.g e. J (A e. g /\ (F"g) C_ o)))))
102	101	imp 377	. . . . 5 |- ((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ A.y e. ((nei` K)` {(F` A)})(`'F"y) e. ((nei` J)` {A})) -> (o e. K -> ((F` A) e. o -> E.g e. J (A e. g /\ (F"g) C_ o))))
103	102	r19.21aiv 2175	. . . 4 |- ((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ A.y e. ((nei` K)` {(F` A)})(`'F"y) e. ((nei` J)` {A})) -> A.o e. K ((F` A) e. o -> E.g e. J (A e. g /\ (F"g) C_ o)))
104	66, 67, 103	mpbir2and 802	. . 3 |- ((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ A.y e. ((nei` K)` {(F` A)})(`'F"y) e. ((nei` J)` {A})) -> F e. ((J CnP K)` A))
105	104	ex 402	. 2 |- (((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) -> (A.y e. ((nei` K)` {(F` A)})(`'F"y) e. ((nei` J)` {A}) -> F e. ((J CnP K)` A)))
106	61, 105	impbid 574	1 |- (((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) -> (F e. ((J CnP K)` A) <-> A.y e. ((nei` K)` {(F` A)})(`'F"y) e. ((nei` J)` {A})))

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240   /\ w3a 858   = wceq 1298   e. wcel 1300  A.wral 2105  E.wrex 2106   C_ wss 2593  {csn 3044  U.cuni 3177  `'ccnv 3985  dom cdm 3986  "cima 3989  Fun wfun 3992  -->wf 3994  ` cfv 3998  (class class class)co 4884  Topctop 8857  neicnei 8988   CnP ccnp 9029

This theorem is referenced by:  cnpfillim 15589

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

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  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-rab 2112  df-v 2294  df-sbc 2454  df-csb 2541  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-nul 2876  df-pw 3035  df-sn 3049  df-pr 3050  df-op 3053  df-uni 3178  df-br 3339  df-opab 3396  df-id 3586  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-fv 4014  df-opr 4886  df-oprab 4887  df-map 5383  df-nei 8989  df-cnp 9031

Copyright terms: Public domain