Theorem iscncl 7770

Description: A definition of a continuous function using closed sets. Bourbaki TG I.9 Th. 1 (d). (Contributed by FL, 30-Jan-2007.)

Hypotheses

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

Assertion

Ref	Expression
iscncl	|- ((J e. Top /\ K e. Top) -> (F e. (J Cn K) <-> (F:X-->Y /\ A.y e. (Clsd` K)(`'F"y) e. (Clsd` J))))

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

Proof of Theorem iscncl

Step	Hyp	Ref	Expression
1		iscncl.1	. . 3 |- X = U.J
2		iscncl.2	. . 3 |- Y = U.K
3	1, 2	iscn 7758	. 2 |- ((J e. Top /\ K e. Top) -> (F e. (J Cn K) <-> (F:X-->Y /\ A.x e. K (`'F"x) e. J)))
4		fimacnv 3810	. . . . . . . . . . . . . . . . . 18 |- (F:X-->Y -> (`'F"Y) = X)
5	4	eqcomd 1480	. . . . . . . . . . . . . . . . 17 |- (F:X-->Y -> X = (`'F"Y))
6	5	difeq1d 2158	. . . . . . . . . . . . . . . 16 |- (F:X-->Y -> (X \ (`'F"y)) = ((`'F"Y) \ (`'F"y)))
7		ffun 3629	. . . . . . . . . . . . . . . . 17 |- (F:X-->Y -> Fun F)
8		funcnvcnv 3555	. . . . . . . . . . . . . . . . 17 |- (Fun F -> Fun `'`'F)
9		imadif 3574	. . . . . . . . . . . . . . . . 17 |- (Fun `'`'F -> (`'F"(Y \ y)) = ((`'F"Y) \ (`'F"y)))
10	7, 8, 9	3syl 20	. . . . . . . . . . . . . . . 16 |- (F:X-->Y -> (`'F"(Y \ y)) = ((`'F"Y) \ (`'F"y)))
11	6, 10	eqtr4d 1510	. . . . . . . . . . . . . . 15 |- (F:X-->Y -> (X \ (`'F"y)) = (`'F"(Y \ y)))
12	11	a1i 8	. . . . . . . . . . . . . 14 |- (A.x e. K (`'F"x) e. J -> (F:X-->Y -> (X \ (`'F"y)) = (`'F"(Y \ y))))
13	12	a1i 8	. . . . . . . . . . . . 13 |- (y e. (Clsd` K) -> (A.x e. K (`'F"x) e. J -> (F:X-->Y -> (X \ (`'F"y)) = (`'F"(Y \ y)))))
14	13	com13 33	. . . . . . . . . . . 12 |- (F:X-->Y -> (A.x e. K (`'F"x) e. J -> (y e. (Clsd` K) -> (X \ (`'F"y)) = (`'F"(Y \ y)))))
15	14	a1i 8	. . . . . . . . . . 11 |- (K e. Top -> (F:X-->Y -> (A.x e. K (`'F"x) e. J -> (y e. (Clsd` K) -> (X \ (`'F"y)) = (`'F"(Y \ y))))))
16	15	imp41 368	. . . . . . . . . 10 |- ((((K e. Top /\ F:X-->Y) /\ A.x e. K (`'F"x) e. J) /\ y e. (Clsd` K)) -> (X \ (`'F"y)) = (`'F"(Y \ y)))
17		imaeq2 3402	. . . . . . . . . . . . . 14 |- (x = (Y \ y) -> (`'F"x) = (`'F"(Y \ y)))
18	17	eleq1d 1540	. . . . . . . . . . . . 13 |- (x = (Y \ y) -> ((`'F"x) e. J <-> (`'F"(Y \ y)) e. J))
19	18	rcla4cva 1876	. . . . . . . . . . . 12 |- ((A.x e. K (`'F"x) e. J /\ (Y \ y) e. K) -> (`'F"(Y \ y)) e. J)
20		simplr 413	. . . . . . . . . . . 12 |- (((K e. Top /\ A.x e. K (`'F"x) e. J) /\ y e. (Clsd` K)) -> A.x e. K (`'F"x) e. J)
21	2	cldopn 7672	. . . . . . . . . . . . 13 |- ((K e. Top /\ y e. (Clsd` K)) -> (Y \ y) e. K)
22	21	adantlr 393	. . . . . . . . . . . 12 |- (((K e. Top /\ A.x e. K (`'F"x) e. J) /\ y e. (Clsd` K)) -> (Y \ y) e. K)
23	19, 20, 22	sylanc 471	. . . . . . . . . . 11 |- (((K e. Top /\ A.x e. K (`'F"x) e. J) /\ y e. (Clsd` K)) -> (`'F"(Y \ y)) e. J)
24	23	adantllr 397	. . . . . . . . . 10 |- ((((K e. Top /\ F:X-->Y) /\ A.x e. K (`'F"x) e. J) /\ y e. (Clsd` K)) -> (`'F"(Y \ y)) e. J)
25	16, 24	eqeltrd 1548	. . . . . . . . 9 |- ((((K e. Top /\ F:X-->Y) /\ A.x e. K (`'F"x) e. J) /\ y e. (Clsd` K)) -> (X \ (`'F"y)) e. J)
26	25	exp41 382	. . . . . . . 8 |- (K e. Top -> (F:X-->Y -> (A.x e. K (`'F"x) e. J -> (y e. (Clsd` K) -> (X \ (`'F"y)) e. J))))
27	26	adantl 388	. . . . . . 7 |- ((J e. Top /\ K e. Top) -> (F:X-->Y -> (A.x e. K (`'F"x) e. J -> (y e. (Clsd` K) -> (X \ (`'F"y)) e. J))))
28	27	imp41 368	. . . . . 6 |- (((((J e. Top /\ K e. Top) /\ F:X-->Y) /\ A.x e. K (`'F"x) e. J) /\ y e. (Clsd` K)) -> (X \ (`'F"y)) e. J)
29	1	iscld2 7670	. . . . . . . . 9 |- ((J e. Top /\ (`'F"y) (_ X) -> ((`'F"y) e. (Clsd` J) <-> (X \ (`'F"y)) e. J))
30		cnvimass 3423	. . . . . . . . . . 11 |- (`'F"y) (_ dom F
31	30	a1i 8	. . . . . . . . . 10 |- (F:X-->Y -> (`'F"y) (_ dom F)
32		fdm 3631	. . . . . . . . . 10 |- (F:X-->Y -> dom F = X)
33	31, 32	sseqtrd 2097	. . . . . . . . 9 |- (F:X-->Y -> (`'F"y) (_ X)
34	29, 33	sylan2 451	. . . . . . . 8 |- ((J e. Top /\ F:X-->Y) -> ((`'F"y) e. (Clsd` J) <-> (X \ (`'F"y)) e. J))
35	34	adantlr 393	. . . . . . 7 |- (((J e. Top /\ K e. Top) /\ F:X-->Y) -> ((`'F"y) e. (Clsd` J) <-> (X \ (`'F"y)) e. J))
36	35	ad2antrr 404	. . . . . 6 |- (((((J e. Top /\ K e. Top) /\ F:X-->Y) /\ A.x e. K (`'F"x) e. J) /\ y e. (Clsd` K)) -> ((`'F"y) e. (Clsd` J) <-> (X \ (`'F"y)) e. J))
37	28, 36	mpbird 196	. . . . 5 |- (((((J e. Top /\ K e. Top) /\ F:X-->Y) /\ A.x e. K (`'F"x) e. J) /\ y e. (Clsd` K)) -> (`'F"y) e. (Clsd` J))
38	37	r19.21aiva 1714	. . . 4 |- ((((J e. Top /\ K e. Top) /\ F:X-->Y) /\ A.x e. K (`'F"x) e. J) -> A.y e. (Clsd` K)(`'F"y) e. (Clsd` J))
39	5	difeq1d 2158	. . . . . . . . . . . . . . . 16 |- (F:X-->Y -> (X \ (`'F"x)) = ((`'F"Y) \ (`'F"x)))
40		imadif 3574	. . . . . . . . . . . . . . . . 17 |- (Fun `'`'F -> (`'F"(Y \ x)) = ((`'F"Y) \ (`'F"x)))
41	7, 8, 40	3syl 20	. . . . . . . . . . . . . . . 16 |- (F:X-->Y -> (`'F"(Y \ x)) = ((`'F"Y) \ (`'F"x)))
42	39, 41	eqtr4d 1510	. . . . . . . . . . . . . . 15 |- (F:X-->Y -> (X \ (`'F"x)) = (`'F"(Y \ x)))
43	42	a1i 8	. . . . . . . . . . . . . 14 |- (A.y e. (Clsd` K)(`'F"y) e. (Clsd` J) -> (F:X-->Y -> (X \ (`'F"x)) = (`'F"(Y \ x))))
44	43	a1i 8	. . . . . . . . . . . . 13 |- (x e. K -> (A.y e. (Clsd` K)(`'F"y) e. (Clsd` J) -> (F:X-->Y -> (X \ (`'F"x)) = (`'F"(Y \ x)))))
45	44	com13 33	. . . . . . . . . . . 12 |- (F:X-->Y -> (A.y e. (Clsd` K)(`'F"y) e. (Clsd` J) -> (x e. K -> (X \ (`'F"x)) = (`'F"(Y \ x)))))
46	45	a1i 8	. . . . . . . . . . 11 |- (K e. Top -> (F:X-->Y -> (A.y e. (Clsd` K)(`'F"y) e. (Clsd` J) -> (x e. K -> (X \ (`'F"x)) = (`'F"(Y \ x))))))
47	46	imp41 368	. . . . . . . . . 10 |- ((((K e. Top /\ F:X-->Y) /\ A.y e. (Clsd` K)(`'F"y) e. (Clsd` J)) /\ x e. K) -> (X \ (`'F"x)) = (`'F"(Y \ x)))
48		imaeq2 3402	. . . . . . . . . . . . . 14 |- (y = (Y \ x) -> (`'F"y) = (`'F"(Y \ x)))
49	48	eleq1d 1540	. . . . . . . . . . . . 13 |- (y = (Y \ x) -> ((`'F"y) e. (Clsd` J) <-> (`'F"(Y \ x)) e. (Clsd` J)))
50	49	rcla4cva 1876	. . . . . . . . . . . 12 |- ((A.y e. (Clsd` K)(`'F"y) e. (Clsd` J) /\ (Y \ x) e. (Clsd` K)) -> (`'F"(Y \ x)) e. (Clsd` J))
51		simplr 413	. . . . . . . . . . . 12 |- (((K e. Top /\ A.y e. (Clsd` K)(`'F"y) e. (Clsd` J)) /\ x e. K) -> A.y e. (Clsd` K)(`'F"y