Theorem cnntr 15420

Description: Continuity in terms of interior.

Hypotheses

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

Assertion

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

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

Proof of Theorem cnntr

Step	Hyp	Ref	Expression
1		cncls.1	. . . 4 |- X = U.J
2		cncls.2	. . . 4 |- Y = U.K
3	1, 2	iscn 9034	. . 3 |- ((J e. Top /\ K e. Top) -> (F e. (J Cn K) <-> (F:X-->Y /\ A.o e. K (`'F"o) e. J)))
4	3	3adant3 896	. 2 |- ((J e. Top /\ K e. Top /\ F:X-->Y) -> (F e. (J Cn K) <-> (F:X-->Y /\ A.o e. K (`'F"o) e. J)))
5		ibar 705	. . 3 |- (F:X-->Y -> (A.o e. K (`'F"o) e. J <-> (F:X-->Y /\ A.o e. K (`'F"o) e. J)))
6	5	3ad2ant3 899	. 2 |- ((J e. Top /\ K e. Top /\ F:X-->Y) -> (A.o e. K (`'F"o) e. J <-> (F:X-->Y /\ A.o e. K (`'F"o) e. J)))
7		simp1 876	. . . . . . 7 |- ((J e. Top /\ K e. Top /\ F:X-->Y) -> J e. Top)
8	7	adantr 425	. . . . . 6 |- (((J e. Top /\ K e. Top /\ F:X-->Y) /\ (A.o e. K (`'F"o) e. J /\ y C_ Y)) -> J e. Top)
9		ffn 4562	. . . . . . . . 9 |- (F:X-->Y -> F Fn X)
10		fndm 4512	. . . . . . . . 9 |- (F Fn X -> dom F = X)
11		cnvimass 4286	. . . . . . . . . 10 |- (`'F"y) C_ dom F
12		sseq2 2639	. . . . . . . . . 10 |- (dom F = X -> ((`'F"y) C_ dom F <-> (`'F"y) C_ X))
13	11, 12	mpbii 210	. . . . . . . . 9 |- (dom F = X -> (`'F"y) C_ X)
14	9, 10, 13	3syl 24	. . . . . . . 8 |- (F:X-->Y -> (`'F"y) C_ X)
15	14	3ad2ant3 899	. . . . . . 7 |- ((J e. Top /\ K e. Top /\ F:X-->Y) -> (`'F"y) C_ X)
16	15	adantr 425	. . . . . 6 |- (((J e. Top /\ K e. Top /\ F:X-->Y) /\ (A.o e. K (`'F"o) e. J /\ y C_ Y)) -> (`'F"y) C_ X)
17	2	ntropn 8960	. . . . . . . . . . 11 |- ((K e. Top /\ y C_ Y) -> ((int` K)` y) e. K)
18	17	3ad2antl2 1039	. . . . . . . . . 10 |- (((J e. Top /\ K e. Top /\ F:X-->Y) /\ y C_ Y) -> ((int` K)` y) e. K)
19		imaeq2 4260	. . . . . . . . . . . 12 |- (o = ((int` K)` y) -> (`'F"o) = (`'F"((int` K)` y)))
20	19	eleq1d 1963	. . . . . . . . . . 11 |- (o = ((int` K)` y) -> ((`'F"o) e. J <-> (`'F"((int` K)` y)) e. J))
21	20	rcla4v 2376	. . . . . . . . . 10 |- (((int` K)` y) e. K -> (A.o e. K (`'F"o) e. J -> (`'F"((int` K)` y)) e. J))
22	18, 21	syl 12	. . . . . . . . 9 |- (((J e. Top /\ K e. Top /\ F:X-->Y) /\ y C_ Y) -> (A.o e. K (`'F"o) e. J -> (`'F"((int` K)` y)) e. J))
23	22	ex 402	. . . . . . . 8 |- ((J e. Top /\ K e. Top /\ F:X-->Y) -> (y C_ Y -> (A.o e. K (`'F"o) e. J -> (`'F"((int` K)` y)) e. J)))
24	23	com23 36	. . . . . . 7 |- ((J e. Top /\ K e. Top /\ F:X-->Y) -> (A.o e. K (`'F"o) e. J -> (y C_ Y -> (`'F"((int` K)` y)) e. J)))
25	24	imp32 390	. . . . . 6 |- (((J e. Top /\ K e. Top /\ F:X-->Y) /\ (A.o e. K (`'F"o) e. J /\ y C_ Y)) -> (`'F"((int` K)` y)) e. J)
26	2	ntrss2 8966	. . . . . . . . 9 |- ((K e. Top /\ y C_ Y) -> ((int` K)` y) C_ y)
27	26	3ad2antl2 1039	. . . . . . . 8 |- (((J e. Top /\ K e. Top /\ F:X-->Y) /\ y C_ Y) -> ((int` K)` y) C_ y)
28	27	adantrl 430	. . . . . . 7 |- (((J e. Top /\ K e. Top /\ F:X-->Y) /\ (A.o e. K (`'F"o) e. J /\ y C_ Y)) -> ((int` K)` y) C_ y)
29		imass2 4299	. . . . . . 7 |- (((int` K)` y) C_ y -> (`'F"((int` K)` y)) C_ (`'F"y))
30	28, 29	syl 12	. . . . . 6 |- (((J e. Top /\ K e. Top /\ F:X-->Y) /\ (A.o e. K (`'F"o) e. J /\ y C_ Y)) -> (`'F"((int` K)` y)) C_ (`'F"y))
31	1	ssntr 15405	. . . . . 6 |- (((J e. Top /\ (`'F"y) C_ X) /\ ((`'F"((int` K)` y)) e. J /\ (`'F"((int` K)` y)) C_ (`'F"y))) -> (`'F"((int` K)` y)) C_ ((int` J)` (`'F"y)))
32	8, 16, 25, 30, 31	syl22anc 1101	. . . . 5 |- (((J e. Top /\ K e. Top /\ F:X-->Y) /\ (A.o e. K (`'F"o) e. J /\ y C_ Y)) -> (`'F"((int` K)` y)) C_ ((int` J)` (`'F"y)))
33	32	exp32 408	. . . 4 |- ((J e. Top /\ K e. Top /\ F:X-->Y) -> (A.o e. K (`'F"o) e. J -> (y C_ Y -> (`'F"((int` K)` y)) C_ ((int` J)` (`'F"y)))))
34	33	19.21adv 1666	. . 3 |- ((J e. Top /\ K e. Top /\ F:X-->Y) -> (A.o e. K (`'F"o) e. J -> A.y(y C_ Y -> (`'F"((int` K)` y)) C_ ((int` J)` (`'F"y)))))
35	7	adantr 425	. . . . . . . 8 |- (((J e. Top /\ K e. Top /\ F:X-->Y) /\ (A.y(y C_ Y -> (`'F"((int` K)` y)) C_ ((int` J)` (`'F"y))) /\ o e. K)) -> J e. Top)
36		cnvimass 4286	. . . . . . . . . . . 12 |- (`'F"o) C_ dom F
37	36	a1i 8	. . . . . . . . . . 11 |- (F:X-->Y -> (`'F"o) C_ dom F)
38		fdm 4567	. . . . . . . . . . 11 |- (F:X-->Y -> dom F = X)
39	37, 38	sseqtrd 2653	. . . . . . . . . 10 |- (F:X-->Y -> (`'F"o) C_ X)
40	39	3ad2ant3 899	. . . . . . . . 9 |- ((J e. Top /\ K e. Top /\ F:X-->Y) -> (`'F"o) C_ X)
41	40	adantr 425	. . . . . . . 8 |- (((J e. Top /\ K e. Top /\ F:X-->Y) /\ (A.y(y C_ Y -> (`'F"((int` K)` y)) C_ ((int` J)` (`'F"y))) /\ o e. K)) -> (`'F"o) C_ X)
42	1	ntrss2 8966	. . . . . . . 8 |- ((J e. Top /\ (`'F"o) C_ X) -> ((int` J)` (`'F"o)) C_ (`'F"o))
43	35, 41, 42	syl11anc 524	. . . . . . 7 |- (((J e. Top /\ K e. Top /\ F:X-->Y) /\ (A.y(y C_ Y -> (`'F"((int` K)` y)) C_ ((int` J)` (`'F"y))) /\ o e. K)) -> ((int` J)` (`'F"o)) C_ (`'F"o))
44		simprr 451	. . . . . . . . . 10 |- (((J e. Top /\ K e. Top /\ F:X-->Y) /\ (A.y(y C_ Y -> (`'F"((int` K)` y)) C_ ((int` J)` (`'F"y))) /\ o e. K)) -> o e. K)
45		simp2 877	. . . . . . . . . . . 12 |- ((J e. Top /\ K e. Top /\ F:X-->Y) -> K e. Top)
46	45	adantr 425	. . . . . . . . . . 11 |- (((J e. Top /\ K e. Top /\ F:X-->Y) /\ (A.y(y C_ Y -> (`'F"((int` K)` y)) C_ ((int` J)` (`'F"y))) /\ o e. K)) -> K e. Top)
47	2	eltopss 8872	. . . . . . . . . . . . 13 |- ((K e. Top /\ o e. K) -> o C_ Y)
48	47	3ad2antl2 1039	. . . . . . . . . . . 12 |- (((J e. Top /\ K e. Top /\ F:X-->Y) /\ o e. K) -> o C_ Y)
49	48	adantrl 430	. . . . . . . . . . 11 |- (((J e. Top /\ K e. Top /\ F:X-->Y) /\ (A.y(y C_ Y -> (`'F"((int` K)` y)) C_ ((int` J)` (`'F"y))) /\ o e. K)) -> o C_ Y)
50	2	isopn3 8973	. . . . . . . . . . 11 |- ((K e. Top /\ o C_ Y) -> (o e. K <-> ((int` K)` o) = o))
51	46, 49, 50	syl11anc 524	. . . . . . . . . 10 |- (((J e. Top /\ K e. Top /\ F:X-->Y) /\ (A.y(y C_ Y -> (`'F"((int` K)` y)) C_ ((int` J)` (`'F"y))) /\ o e. K)) -> (o e. K <-> ((int` K)` o) = o))
52	44, 51	mpbid 212	. . . . . . . . 9 |- (((J e. Top /\ K e. Top /\ F:X-->Y) /\ (A.y(y C_ Y -> (`'F"((int` K)` y)) C_ ((int` J)` (`'F"y))) /\ o e. K)) -> ((int` K)` o) = o)
53	52	imaeq2d 4264	. . . . . . . 8 |- (((J e. Top /\ K e. Top /\ F:X-->Y) /\ (A.y(y C_ Y -> (`'F"((int` K)` y)) C_ ((int` J)` (`'F"y))) /\ o e. K)) -> (`'F"((int` K)` o)) = (`'F"o))
54		sseq1 2637	. . . . . . . . . . . . . . 15 |- (y = o -> (y C_ Y <-> o C_ Y))
55		fveq2 4681	. . . . . . . . . . . . . . . . 17 |- (y = o -> ((int` K)` y) = ((int` K)` o))
56	55	imaeq2d 4264	. . . . . . . . . . . . . . . 16 |- (y = o -> (`'F"((int` K)` y)) = (`'F"((int` K)` o)))
57		imaeq2 4260	. . . . . . . . . . . . . . . . 17 |- (y = o -> (`'F"y) = (`'F"o))
58	57	fveq2d 4685	. . . . . . . . . . . . . . . 16 |- (y = o -> ((int` J)` (`'F"y)) = ((int` J)` (`'F"o)))
59	56, 58	sseq12d 2646	. . . . . . . . . . . . . . 15 |- (y = o -> ((`'F"((int` K)` y)) C_ ((int` J)` (`'F"y)) <-> (`'F"((int` K)` o)) C_ ((int` J)` (`'F"o))))
60	54, 59	imbi12d 688	. . . . . . . . . . . . . 14 |- (y = o -> ((y C_ Y -> (`'F"((int` K)` y)) C_ ((int` J)` (`'F"y))) <-> (o C_ Y -> (`'F"((int` K)` o)) C_ ((int` J)` (`'F"o)))))
61	60	cla4gv 2364	. . . . . . . . . . . . 13 |- (o e. K -> (A.y(y C_ Y -> (`'F"((int` K)` y)) C_ ((int` J)` (`'F"y))) -> (o C_ Y -> (`'F"((int` K)` o)) C_ ((int` J)` (`'F"o)))))
62	61	adantl 424	. . . . . . . . . . . 12 |- (((J e. Top /\ K e. Top /\ F:X-->Y) /\ o e. K) -> (A.y(y C_ Y -> (`'F"((int` K)` y)) C_ ((int` J)` (`'F"y))) -> (o C_ Y -> (`'F"((int` K)` o)) C_ ((int` J)` (`'F"o)))))
63	48, 62	mpid 58	. . . . . . . . . . 11 |- (((J e. Top /\ K e. Top /\ F:X-->Y) /\ o e. K) -> (A.y(y C_ Y -> (`'F"((int` K)` y)) C_ ((int` J)` (`'F"y))) -> (`'F"((int` K)` o)) C_ ((int` J)` (`'F"o))))
64	63	ex 402	. . . . . . . . . 10 |- ((J e. Top /\ K e. Top /\ F:X-->Y) -> (o e. K -> (A.y(y C_ Y -> (`'F"((int` K)` y)) C_ ((int` J)` (`'F"y))) -> (`'F"((int` K)` o)) C_ ((int` J)` (`'F"o)))))
65	64	com23 36	. . . . . . . . 9 |- ((J e. Top /\ K e. Top /\ F:X-->Y) -> (A.y(y C_ Y -> (`'F"((int` K)` y)) C_ ((int` J)` (`'F"y))) -> (o e. K -> (`'F"((int` K)` o)) C_ ((int` J)` (`'F"o)))))
66	65	imp32 390	. . . . . . . 8 |- (((J e. Top /\ K e. Top /\ F:X-->Y) /\ (A.y(y C_ Y -> (`'F"((int` K)` y)) C_ ((int` J)` (`'F"y))) /\ o e. K)) -> (`'F"((int` K)` o)) C_ ((int` J)` (`'F"o)))
67	53, 66	eqsstr3d 2652	. . . . . . 7 |- (((J e. Top /\ K e. Top /\ F:X-->Y) /\ (A.y(y C_ Y -> (`'F"((int` K)` y)) C_ ((int` J)` (`'F"y))) /\ o e. K)) -> (`'F"o) C_ ((int` J)` (`'F"o)))
68	43, 67	eqssd 2633	. . . . . 6 |- (((J e. Top /\ K e. Top /\ F:X-->Y) /\ (A.y(y C_ Y -> (`'F"((int` K)` y)) C_ ((int` J)` (`'F"y))) /\ o e. K)) -> ((int` J)` (`'F"o)) = (`'F"o))
69	1	isopn3 8973	. . . . . . 7 |- ((J e. Top /\ (`'F"o) C_ X) -> ((`'F"o) e. J <-> ((int` J)` (`'F"o)) = (`'F"o)))
70	35, 41, 69	syl11anc 524	. . . . . 6 |- (((J e. Top /\ K e. Top /\ F:X-->Y) /\ (A.y(y C_ Y -> (`'F"((int` K)` y)) C_ ((int` J)` (`'F"y))) /\ o e. K)) -> ((`'F"o) e. J <-> ((int` J)` (`'F"o)) = (`'F"o)))
71	68, 70	mpbird 213	. . . . 5 |- (((J e. Top /\ K e. Top /\ F:X-->Y) /\ (A.y(y C_ Y -> (`'F"((int` K)` y)) C_ ((int` J)` (`'F"y))) /\ o e. K)) -> (`'F"o) e. J)
72	71	exp32 408	. . . 4 |- ((J e. Top /\ K e. Top /\ F:X-->Y) -> (A.y(y C_ Y -> (`'F"((int` K)` y)) C_ ((int` J)` (`'F"y))) -> (o e. K -> (`'F"o) e. J)))
73	72	r19.21adv 2181	. . 3 |- ((J e. Top /\ K e. Top /\ F:X-->Y) -> (A.y(y C_ Y -> (`'F"((int` K)` y)) C_ ((int` J)` (`'F"y))) -> A.o e. K (`'F"o) e. J))
74	34, 73	impbid 574	. 2 |- ((J e. Top /\ K e. Top /\ F:X-->Y) -> (A.o e. K (`'F"o) e. J <-> A.y(y C_ Y -> (`'F"((int` K)` y)) C_ ((int` J)` (`'F"y)))))
75	4, 6, 74	3bitr2d 605	1 |- ((J e. Top /\ K e. Top /\ F:X-->Y) -> (F e. (J Cn K) <-> A.y(y C_ Y -> (`'F"((int` K)` y)) C_ ((int` J)` (`'F"y)))))

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240   /\ w3a 858  A.wal 1296   = wceq 1298   e. wcel 1300  A.wral 2105   C_ wss 2593  U.cuni 3177  `'ccnv 3985  dom cdm 3986  "cima 3989   Fn wfn 3993  -->wf 3994  ` cfv 3998  (class class class)co 4884  Topctop 8857  intcnt 8937   Cn ccn 9028

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-top 8861  df-ntr 8940  df-cn 9030

Copyright terms: Public domain