Theorem cnconn 15444

Description: Connectedness is respected by a continuous onto map.

Hypotheses

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

Assertion

Ref	Expression
cnconn	|- (((J e. Con /\ K e. Top) /\ (F:X-onto->Y /\ F e. (J Cn K))) -> K e. Con)

Proof of Theorem cnconn

Step	Hyp	Ref	Expression
1		iscon2 10340	. 2 |- (K e. Con <-> (K e. Top /\ (K i^i (Clsd` K)) = {(/), U.K}))
2		simplr 449	. 2 |- (((J e. Con /\ K e. Top) /\ (F:X-onto->Y /\ F e. (J Cn K))) -> K e. Top)
3		cnvexg 4424	. . . . . . . . . . . . . . . . . . . . 21 |- (F e. (J Cn K) -> `'F e. _V)
4		imaexg 4279	. . . . . . . . . . . . . . . . . . . . 21 |- (`'F e. _V -> (`'F"y) e. _V)
5		eleq1 1957	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (x = (`'F"y) -> (x e. J <-> (`'F"y) e. J))
6		eleq1 1957	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (x = (`'F"y) -> (x e. (Clsd` J) <-> (`'F"y) e. (Clsd` J)))
7	5, 6	anbi12d 690	. . . . . . . . . . . . . . . . . . . . . . 23 |- (x = (`'F"y) -> ((x e. J /\ x e. (Clsd` J)) <-> ((`'F"y) e. J /\ (`'F"y) e. (Clsd` J))))
8		eqeq1 1890	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (x = (`'F"y) -> (x = (/) <-> (`'F"y) = (/)))
9		eqeq1 1890	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (x = (`'F"y) -> (x = U.J <-> (`'F"y) = U.J))
10	8, 9	orbi12d 689	. . . . . . . . . . . . . . . . . . . . . . 23 |- (x = (`'F"y) -> ((x = (/) \/ x = U.J) <-> ((`'F"y) = (/) \/ (`'F"y) = U.J)))
11	7, 10	bibi12d 691	. . . . . . . . . . . . . . . . . . . . . 22 |- (x = (`'F"y) -> (((x e. J /\ x e. (Clsd` J)) <-> (x = (/) \/ x = U.J)) <-> (((`'F"y) e. J /\ (`'F"y) e. (Clsd` J)) <-> ((`'F"y) = (/) \/ (`'F"y) = U.J))))
12	11	cla4gv 2364	. . . . . . . . . . . . . . . . . . . . 21 |- ((`'F"y) e. _V -> (A.x((x e. J /\ x e. (Clsd` J)) <-> (x = (/) \/ x = U.J)) -> (((`'F"y) e. J /\ (`'F"y) e. (Clsd` J)) <-> ((`'F"y) = (/) \/ (`'F"y) = U.J))))
13	3, 4, 12	3syl 24	. . . . . . . . . . . . . . . . . . . 20 |- (F e. (J Cn K) -> (A.x((x e. J /\ x e. (Clsd` J)) <-> (x = (/) \/ x = U.J)) -> (((`'F"y) e. J /\ (`'F"y) e. (Clsd` J)) <-> ((`'F"y) = (/) \/ (`'F"y) = U.J))))
14	13	adantl 424	. . . . . . . . . . . . . . . . . . 19 |- ((F:X-onto->Y /\ F e. (J Cn K)) -> (A.x((x e. J /\ x e. (Clsd` J)) <-> (x = (/) \/ x = U.J)) -> (((`'F"y) e. J /\ (`'F"y) e. (Clsd` J)) <-> ((`'F"y) = (/) \/ (`'F"y) = U.J))))
15	14	ad2antlr 441	. . . . . . . . . . . . . . . . . 18 |- ((((J e. Top /\ K e. Top) /\ (F:X-onto->Y /\ F e. (J Cn K))) /\ (y e. K /\ y e. (Clsd` K))) -> (A.x((x e. J /\ x e. (Clsd` J)) <-> (x = (/) \/ x = U.J)) -> (((`'F"y) e. J /\ (`'F"y) e. (Clsd` J)) <-> ((`'F"y) = (/) \/ (`'F"y) = U.J))))
16		cnima 9044	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((J e. Top /\ K e. Top /\ F e. (J Cn K)) /\ y e. K) -> (`'F"y) e. J)
17	16	ex 402	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((J e. Top /\ K e. Top /\ F e. (J Cn K)) -> (y e. K -> (`'F"y) e. J))
18	17	3expa 1067	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((J e. Top /\ K e. Top) /\ F e. (J Cn K)) -> (y e. K -> (`'F"y) e. J))
19	18	imp 377	. . . . . . . . . . . . . . . . . . . . . 22 |- ((((J e. Top /\ K e. Top) /\ F e. (J Cn K)) /\ y e. K) -> (`'F"y) e. J)
20	19	adantlrl 434	. . . . . . . . . . . . . . . . . . . . 21 |- ((((J e. Top /\ K e. Top) /\ (F:X-onto->Y /\ F e. (J Cn K))) /\ y e. K) -> (`'F"y) e. J)
21	20	adantrr 431	. . . . . . . . . . . . . . . . . . . 20 |- ((((J e. Top /\ K e. Top) /\ (F:X-onto->Y /\ F e. (J Cn K))) /\ (y e. K /\ y e. (Clsd` K))) -> (`'F"y) e. J)
22		cnclima 9048	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((J e. Top /\ K e. Top /\ F e. (J Cn K)) /\ y e. (Clsd` K)) -> (`'F"y) e. (Clsd` J))
23	22	ex 402	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((J e. Top /\ K e. Top /\ F e. (J Cn K)) -> (y e. (Clsd` K) -> (`'F"y) e. (Clsd` J)))
24	23	3expa 1067	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((J e. Top /\ K e. Top) /\ F e. (J Cn K)) -> (y e. (Clsd` K) -> (`'F"y) e. (Clsd` J)))
25	24	imp 377	. . . . . . . . . . . . . . . . . . . . . 22 |- ((((J e. Top /\ K e. Top) /\ F e. (J Cn K)) /\ y e. (Clsd` K)) -> (`'F"y) e. (Clsd` J))
26	25	adantlrl 434	. . . . . . . . . . . . . . . . . . . . 21 |- ((((J e. Top /\ K e. Top) /\ (F:X-onto->Y /\ F e. (J Cn K))) /\ y e. (Clsd` K)) -> (`'F"y) e. (Clsd` J))
27	26	adantrl 430	. . . . . . . . . . . . . . . . . . . 20 |- ((((J e. Top /\ K e. Top) /\ (F:X-onto->Y /\ F e. (J Cn K))) /\ (y e. K /\ y e. (Clsd` K))) -> (`'F"y) e. (Clsd` J))
28		pm2.27 76	. . . . . . . . . . . . . . . . . . . . 21 |- (((`'F"y) e. J /\ (`'F"y) e. (Clsd` J)) -> ((((`'F"y) e. J /\ (`'F"y) e. (Clsd` J)) -> ((`'F"y) = (/) \/ (`'F"y) = U.J)) -> ((`'F"y) = (/) \/ (`'F"y) = U.J)))
29		cnconn.2	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- Y = U.K
30	29	eltopss 8872	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((K e. Top /\ y e. K) -> y C_ Y)
31	30	adantll 428	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (((J e. Top /\ K e. Top) /\ y e. K) -> y C_ Y)
32	31	adantlr 429	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((((J e. Top /\ K e. Top) /\ (F:X-onto->Y /\ F e. (J Cn K))) /\ y e. K) -> y C_ Y)
33		foimacnv 4657	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((F:X-onto->Y /\ y C_ Y) -> (F"(`'F"y)) = y)
34	33	eqcomd 1889	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((F:X-onto->Y /\ y C_ Y) -> y = (F"(`'F"y)))
35	34	adantlr 429	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (((F:X-onto->Y /\ F e. (J Cn K)) /\ y C_ Y) -> y = (F"(`'F"y)))
36	35	adantll 428	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((((J e. Top /\ K e. Top) /\ (F:X-onto->Y /\ F e. (J Cn K))) /\ y C_ Y) -> y = (F"(`'F"y)))
37	32, 36	syldan 516	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((((J e. Top /\ K e. Top) /\ (F:X-onto->Y /\ F e. (J Cn K))) /\ y e. K) -> y = (F"(`'F"y)))
38	37	adantrr 431	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((((J e. Top /\ K e. Top) /\ (F:X-onto->Y /\ F e. (J Cn K))) /\ (y e. K /\ y e. (Clsd` K))) -> y = (F"(`'F"y)))
39		imaeq2 4260	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((`'F"y) = (/) -> (F"(`'F"y)) = (F"(/)))
40		ima0 4283	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (F"(/)) = (/)
41	39, 40	syl6eq 1944	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((`'F"y) = (/) -> (F"(`'F"y)) = (/))
42	38, 41	sylan9eq 1948	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((((J e. Top /\ K e. Top) /\ (F:X-onto->Y /\ F e. (J Cn K))) /\ (y e. K /\ y e. (Clsd` K))) /\ (`'F"y) = (/)) -> y = (/))
43	42	ex 402	. . . . . . . . . . . . . . . . . . . . . 22 |- ((((J e. Top /\ K e. Top) /\ (F:X-onto->Y /\ F e. (J Cn K))) /\ (y e. K /\ y e. (Clsd` K))) -> ((`'F"y) = (/) -> y = (/)))
44		cnconn.1	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- X = U.J
45	44	eqeq2i 1894	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((`'F"y) = X <-> (`'F"y) = U.J)
46		imaeq2 4260	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((`'F"y) = X -> (F"(`'F"y)) = (F"X))
47	45, 46	sylbir 218	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((`'F"y) = U.J -> (F"(`'F"y)) = (F"X))
48	47	adantl 424	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((((J e. Top /\ K e. Top) /\ (F:X-onto->Y /\ F e. (J Cn K))) /\ (y e. K /\ y e. (Clsd` K))) /\ (`'F"y) = U.J) -> (F"(`'F"y)) = (F"X))
49	33	adantlr 429	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (((F:X-onto->Y /\ F e. (J Cn K)) /\ y C_ Y) -> (F"(`'F"y)) = y)
50	49	adantll 428	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((((J e. Top /\ K e. Top) /\ (F:X-onto->Y /\ F e. (J Cn K))) /\ y C_ Y) -> (F"(`'F"y)) = y)
51	32, 50	syldan 516	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((((J e. Top /\ K e. Top) /\ (F:X-onto->Y /\ F e. (J Cn K))) /\ y e. K) -> (F"(`'F"y)) = y)
52	51	adantrr 431	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((((J e. Top /\ K e. Top) /\ (F:X-onto->Y /\ F e. (J Cn K))) /\ (y e. K /\ y e. (Clsd` K))) -> (F"(`'F"y)) = y)
53	52	adantr 425	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((((J e. Top /\ K e. Top) /\ (F:X-onto->Y /\ F e. (J Cn K))) /\ (y e. K /\ y e. (Clsd` K))) /\ (`'F"y) = U.J) -> (F"(`'F"y)) = y)
54		foima 4622	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (F:X-onto->Y -> (F"X) = Y)
55	54	ad2antrl 442	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (((J e. Top /\ K e. Top) /\ (F:X-onto->Y /\ F e. (J Cn K))) -> (F"X) = Y)
56	55, 29	syl6eq 1944	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((J e. Top /\ K e. Top) /\ (F:X-onto->Y /\ F e. (J Cn K))) -> (F"X) = U.K)
57	56	ad2antrr 440	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((((J e. Top /\ K e. Top) /\ (F:X-onto->Y /\ F e. (J Cn K))) /\ (y e. K /\ y e. (Clsd` K))) /\ (`'F"y) = U.J) -> (F"X) = U.K)
58	48, 53, 57	3eqtr3d 1934	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((((J e. Top /\ K e. Top) /\ (F:X-onto->Y /\ F e. (J Cn K))) /\ (y e. K /\ y e. (Clsd` K))) /\ (`'F"y) = U.J) -> y = U.K)
59	58	ex 402	. . . . . . . . . . . . . . . . . . . . . 22 |- ((((J e. Top /\ K e. Top) /\ (F:X-onto->Y /\ F e. (J Cn K))) /\ (y e. K /\ y e. (Clsd` K))) -> ((`'F"y) = U.J -> y = U.K))
60	43, 59	orim12d 624	. . . . . . . . . . . . . . . . . . . . 21 |- ((((J e. Top /\ K e. Top) /\ (F:X-onto->Y /\ F e. (J Cn K))) /\ (y e. K /\ y e. (Clsd` K))) -> (((`'F"y) = (/) \/ (`'F"y) = U.J) -> (y = (/) \/ y = U.K)))
61	28, 60	syl9r 72	. . . . . . . . . . . . . . . . . . . 20 |- ((((J e. Top /\ K e. Top) /\ (F:X-onto->Y /\ F e. (J Cn K))) /\ (y e. K /\ y e. (Clsd` K))) -> (((`'F"y) e. J /\ (`'F"y) e. (Clsd` J)) -> ((((`'F"y) e. J /\ (`'F"y) e. (Clsd` J)) -> ((`'F"y) = (/) \/ (`'F"y) = U.J)) -> (y = (/) \/ y = U.K))))
62	21, 27, 61	mp2and 767	. . . . . . . . . . . . . . . . . . 19 |- ((((J e. Top /\ K e. Top) /\ (F:X-onto->Y /\ F e. (J Cn K))) /\ (y e. K /\ y e. (Clsd` K))) -> ((((`'F"y) e. J /\ (`'F"y) e. (Clsd` J)) -> ((`'F"y) = (/) \/ (`'F"y) = U.J)) -> (y = (/) \/ y = U.K)))
63		bi1 165	. . . . . . . . . . . . . . . . . . 19 |- ((((`'F"y) e. J /\ (`'F"y) e. (Clsd` J)) <-> ((`'F"y) = (/) \/ (`'F"y) = U.J)) -> (((`'F"y) e. J /\ (`'F"y) e. (Clsd` J)) -> ((`'F"y) = (/) \/ (`'F"y) = U.J)))
64	62, 63	syl5 20	. . . . . . . . . . . . . . . . . 18 |- ((((J e. Top /\ K e. Top) /\ (F:X-onto->Y /\ F e. (J Cn K))) /\ (y e. K /\ y e. (Clsd` K))) -> ((((`'F"y) e. J /\ (`'F"y) e. (Clsd` J)) <-> ((`'F"y) = (/) \/ (`'F"y) = U.J)) -> (y = (/) \/ y = U.K)))
65	15, 64	syld 30	. . . . . . . . . . . . . . . . 17 |- ((((J e. Top /\ K e. Top) /\ (F:X-onto->Y /\ F e. (J Cn K))) /\ (y e. K /\ y e. (Clsd` K))) -> (A.x((x e. J /\ x e. (Clsd` J)) <-> (x = (/) \/ x = U.J)) -> (y = (/) \/ y = U.K)))
66	65	ex 402	. . . . . . . . . . . . . . . 16 |- (((J e. Top /\ K e. Top) /\ (F:X-onto->Y /\ F e. (J Cn K))) -> ((y e. K /\ y e. (Clsd` K)) -> (A.x((x e. J /\ x e. (Clsd` J)) <-> (x = (/) \/ x = U.J)) -> (y = (/) \/ y = U.K))))
67	66	com23 36	. . . . . . . . . . . . . . 15 |- (((J e. Top /\ K e. Top) /\ (F:X-onto->Y /\ F e. (J Cn K))) -> (A.x((x e. J /\ x e. (Clsd` J)) <-> (x = (/) \/ x = U.J)) -> ((y e. K /\ y e. (Clsd` K)) -> (y = (/) \/ y = U.K))))
68	67	imp 377	. . . . . . . . . . . . . 14 |- ((((J e. Top /\ K e. Top) /\ (F:X-onto->Y /\ F e. (J Cn K))) /\ A.x((x e. J /\ x e. (Clsd` J)) <-> (x = (/) \/ x = U.J))) -> ((y e. K /\ y e. (Clsd` K)) -> (y = (/) \/ y = U.K)))
69		eleq1 1957	. . . . . . . . . . . . . . . . . . 19 |- (y = (/) -> (y e. K <-> (/) e. K))
70		0opn 8870	. . . . . . . . . . . . . . . . . . 19 |- (K e. Top -> (/) e. K)
71	69, 70	syl5cbir 228	. . . . . . . . . . . . . . . . . 18 |- (K e. Top -> (y = (/) -> y e. K))
72		eleq1 1957	. . . . . . . . . . . . . . . . . . 19 |- (y = (/) -> (y e. (Clsd` K) <-> (/) e. (Clsd` K)))
73		0cld 8954	. . . . . . . . . . . . . . . . . . 19 |- (K e. Top -> (/) e. (Clsd` K))
74	72, 73	syl5cbir 228	. . . . . . . . . . . . . . . . . 18 |- (K e. Top -> (y = (/) -> y e. (Clsd` K)))
75	71, 74	jcad 661	. . . . . . . . . . . . . . . . 17 |- (K e. Top -> (y = (/) -> (y e. K /\ y e. (Clsd` K))))
76		eleq1 1957	. . . . . . . . . . . . . . . . . . 19 |- (y = U.K -> (y e. K <-> U.K e. K))
77		eqid 1884	. . . . . . . . . . . . . . . . . . . 20 |- U.K = U.K
78	77	topopn 8871	. . . . . . . . . . . . . . . . . . 19 |- (K e. Top -> U.K e. K)
79	76, 78	syl5cbir 228	. . . . . . . . . . . . . . . . . 18 |- (K e. Top -> (y = U.K -> y e. K))
80		eleq1 1957	. . . . . . . . . . . . . . . . . . 19 |- (y = U.K -> (y e. (Clsd` K) <-> U.K e. (Clsd` K)))
81	77	topcld 8951	. . . . . . . . . . . . . . . . . . 19 |- (K e. Top -> U.K e. (Clsd` K))
82	80, 81	syl5cbir 228	. . . . . . . . . . . . . . . . . 18 |- (K e. Top -> (y = U.K -> y e. (Clsd` K)))
83	79, 82	jcad 661	. . . . . . . . . . . . . . . . 17 |- (K e. Top -> (y = U.K -> (y e. K /\ y e. (Clsd` K))))
84	75, 83	jaod 469	. . . . . . . . . . . . . . . 16 |- (K e. Top -> ((y = (/) \/ y = U.K) -> (y e. K /\ y e. (Clsd` K))))
85	84	ad2antlr 441	. . . . . . . . . . . . . . 15 |- (((J e. Top /\ K e. Top) /\ (F:X-onto->Y /\ F e. (J Cn K))) -> ((y = (/) \/ y = U.K) -> (y e. K /\ y e. (Clsd` K))))
86	85	adantr 425	. . . . . . . . . . . . . 14 |- ((((J e. Top /\ K e. Top) /\ (F:X-onto->Y /\ F e. (J Cn K))) /\ A.x((x e. J /\ x e. (Clsd` J)) <-> (x = (/) \/ x = U.J))) -> ((y = (/) \/ y = U.K) -> (y e. K /\ y e. (Clsd` K))))
87	68, 86	impbid 574	. . . . . . . . . . . . 13 |- ((((J e. Top /\ K e. Top) /\ (F:X-onto->Y /\ F e. (J Cn K))) /\ A.x((x e. J /\ x e. (Clsd` J)) <-> (x = (/) \/ x = U.J))) -> ((y e. K /\ y e. (Clsd` K)) <-> (y = (/) \/ y = U.K)))
88	87	ex 402	. . . . . . . . . . . 12 |- (((J e. Top /\ K e. Top) /\ (F:X-onto->Y /\ F e. (J Cn K))) -> (A.x((x e. J /\ x e. (Clsd` J)) <-> (x = (/) \/ x = U.J)) -> ((y e. K /\ y e. (Clsd` K)) <-> (y = (/) \/ y = U.K))))
89	88	19.21adv 1666	. . . . . . . . . . 11 |- (((J e. Top /\ K e. Top) /\ (F:X-onto->Y /\ F e. (J Cn K))) -> (A.x((x e. J /\ x e. (Clsd` J)) <-> (x = (/) \/ x = U.J)) -> A.y((y e. K /\ y e. (Clsd` K)) <-> (y = (/) \/ y = U.K))))
90		elin 2786	. . . . . . . . . . . . 13 |- (x e. (J i^i (Clsd` J)) <-> (x e. J /\ x e. (Clsd` J)))
91		visset 2295	. . . . . . . . . . . . . 14 |- x e. _V
92	91	elpr 3061	. . . . . . . . . . . . 13 |- (x e. {(/), U.J} <-> (x = (/) \/ x = U.J))
93	90, 92	bibi12i 672	. . . . . . . . . . . 12 |- ((x e. (J i^i (Clsd` J)) <-> x e. {(/), U.J}) <-> ((x e. J /\ x e. (Clsd` J)) <-> (x = (/) \/ x = U.J)))
94	93	albii 1346	. . . . . . . . . . 11 |- (A.x(x e. (J i^i (Clsd` J)) <-> x e. {(/), U.J}) <-> A.x((x e. J /\ x e. (Clsd` J)) <-> (x = (/) \/ x = U.J)))
95		elin 2786	. . . . . . . . . . . . 13 |- (y e. (K i^i (Clsd` K)) <-> (y e. K /\ y e. (Clsd` K)))
96		visset 2295	. . . . . . . . . . . . . 14 |- y e. _V
97	96	elpr 3061	. . . . . . . . . . . . 13 |- (y e. {(/), U.K} <-> (y = (/) \/ y = U.K))
98	95, 97	bibi12i 672	. . . . . . . . . . . 12 |- ((y e. (K i^i (Clsd` K)) <-> y e. {(/), U.K}) <-> ((y e. K /\ y e. (Clsd` K)) <-> (y = (/) \/ y = U.K)))
99	98	albii 1346	. . . . . . . . . . 11 |- (A.y(y e. (K i^i (Clsd` K)) <-> y e. {(/), U.K}) <-> A.y((y e. K /\ y e. (Clsd` K)) <-> (y = (/) \/ y = U.K)))
100	89, 94, 99	3imtr4g 612	. . . . . . . . . 10 |- (((J e. Top /\ K e. Top) /\ (F:X-onto->Y /\ F e. (J Cn K))) -> (A.x(x e. (J i^i (Clsd` J)) <-> x e. {(/), U.J}) -> A.y(y e. (K i^i (Clsd` K)) <-> y e. {(/), U.K})))
101		dfcleq 1878	. . . . . . . . . 10 |- ((J i^i (Clsd` J)) = {(/), U.J} <-> A.x(x e. (J i^i (Clsd` J)) <-> x e. {(/), U.J}))
102		dfcleq 1878	. . . . . . . . . 10 |- ((K i^i (Clsd` K)) = {(/), U.K} <-> A.y(y e. (K i^i (Clsd` K)) <-> y e. {(/), U.K}))
103	100, 101, 102	3imtr4g 612	. . . . . . . . 9 |- (((J e. Top /\ K e. Top) /\ (F:X-onto->Y /\ F e. (J Cn K))) -> ((J i^i (Clsd` J)) = {(/), U.J} -> (K i^i (Clsd` K)) = {(/), U.K}))
104	103	exp43 415	. . . . . . . 8 |- (J e. Top -> (K e. Top -> (F:X-onto->Y -> (F e. (J Cn K) -> ((J i^i (Clsd` J)) = {(/), U.J} -> (K i^i (Clsd` K)) = {(/), U.K})))))
105	104	com4l 43	. . . . . . 7 |- (K e. Top -> (F:X-onto->Y -> (F e. (J Cn K) -> (J e. Top -> ((J i^i (Clsd` J)) = {(/), U.J} -> (K i^i (Clsd` K)) = {(/), U.K})))))
106	105	imp5d 401	. . . . . 6 |- (((K e. Top /\ F:X-onto->Y) /\ F e. (J Cn K)) -> ((J e. Top /\ (J i^i (Clsd` J)) = {(/), U.J}) -> (K i^i (Clsd` K)) = {(/), U.K}))
107		iscon2 10340	. . . . . 6 |- (J e. Con <-> (J e. Top /\ (J i^i (Clsd` J)) = {(/), U.J}))
108	106, 107	syl5ib 223	. . . . 5 |- (((K e. Top /\ F:X-onto->Y) /\ F e. (J Cn K)) -> (J e. Con -> (K i^i (Clsd` K)) = {(/), U.K}))
109	108	exp31 407	. . . 4 |- (K e. Top -> (F:X-onto->Y -> (F e. (J Cn K) -> (J e. Con -> (K i^i (Clsd` K)) = {(/), U.K}))))
110	109	com4r 45	. . 3 |- (J e. Con -> (K e. Top -> (F:X-onto->Y -> (F e. (J Cn K) -> (K i^i (Clsd` K)) = {(/), U.K}))))
111	110	imp43 397	. 2 |- (((J e. Con /\ K e. Top) /\ (F:X-onto->Y /\ F e. (J Cn K))) -> (K i^i (Clsd` K)) = {(/), U.K})
112	1, 2, 111	sylanbrc 527	1 |- (((J e. Con /\ K e. Top) /\ (F:X-onto->Y /\ F e. (J Cn K))) -> K e. Con)

Syntax hints:   -> wi 3   <-> wb 163   \/ wo 239   /\ wa 240   /\ w3a 858  A.wal 1296   = wceq 1298   e. wcel 1300  _Vcvv 2292   i^i cin 2592   C_ wss 2593  (/)c0 2875  {cpr 3045  U.cuni 3177  `'ccnv 3985  "cima 3989  -onto->wfo 3996  ` cfv 3998  (class class class)co 4884  Topctop 8857  Clsdccld 8936   Cn ccn 9028  Conccon 10337

This theorem is referenced by:  conntoppr 15445  ivthALT 15454

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-fo 4012  df-fv 4014  df-opr 4886  df-oprab 4887  df-map 5383  df-top 8861  df-cld 8939  df-cn 9030  df-con 10338

Copyright terms: Public domain