Theorem homcard 14893

Description: Homeomorphisms preserve the cardinality of the topologies.

Assertion

Ref	Expression
homcard	|- ((J e. Top /\ K e. Top) -> (J ~= K -> J ~~ K))

Proof of Theorem homcard

Step	Hyp	Ref	Expression
1		hmph 10241	. 2 |- ((J e. Top /\ K e. Top) -> (J ~= K <-> E.f f e. (J Homeo K)))
2		eqid 1884	. . . . . . . . 9 |- U.J = U.J
3		eqid 1884	. . . . . . . . 9 |- U.K = U.K
4	2, 3	ishomeo 10235	. . . . . . . 8 |- ((J e. Top /\ K e. Top /\ f e. (J Homeo K)) -> (f e. (J Homeo K) <-> (f:U.J-1-1-onto->U.K /\ A.x e. J (f"x) e. K /\ A.x e. K (`'f"x) e. J)))
5		opabex2g 4540	. . . . . . . . . . . . 13 |- (J e. Top -> {<.a, b>. | (a e. J /\ b = (f"a))} e. _V)
6	5	3ad2ant1 897	. . . . . . . . . . . 12 |- ((J e. Top /\ K e. Top /\ f e. (J Homeo K)) -> {<.a, b>. | (a e. J /\ b = (f"a))} e. _V)
7	6	adantr 425	. . . . . . . . . . 11 |- (((J e. Top /\ K e. Top /\ f e. (J Homeo K)) /\ (f:U.J-1-1-onto->U.K /\ A.x e. J (f"x) e. K /\ A.x e. K (`'f"x) e. J)) -> {<.a, b>. | (a e. J /\ b = (f"a))} e. _V)
8		visset 2295	. . . . . . . . . . . . . . . . . . . . 21 |- f e. _V
9		imaexg 4279	. . . . . . . . . . . . . . . . . . . . 21 |- (f e. _V -> (f"a) e. _V)
10	8, 9	ax-mp 7	. . . . . . . . . . . . . . . . . . . 20 |- (f"a) e. _V
11	10	a1i 8	. . . . . . . . . . . . . . . . . . 19 |- ((((J e. Top /\ K e. Top /\ f e. (J Homeo K)) /\ (f:U.J-1-1-onto->U.K /\ A.x e. J (f"x) e. K /\ A.x e. K (`'f"x) e. J)) /\ a e. J) -> (f"a) e. _V)
12	11	r19.21aiva 2176	. . . . . . . . . . . . . . . . . 18 |- (((J e. Top /\ K e. Top /\ f e. (J Homeo K)) /\ (f:U.J-1-1-onto->U.K /\ A.x e. J (f"x) e. K /\ A.x e. K (`'f"x) e. J)) -> A.a e. J (f"a) e. _V)
13		eqid 1884	. . . . . . . . . . . . . . . . . . 19 |- {<.a, b>. | (a e. J /\ b = (f"a))} = {<.a, b>. | (a e. J /\ b = (f"a))}
14	13	fnopab2g 4547	. . . . . . . . . . . . . . . . . 18 |- (A.a e. J (f"a) e. _V <-> {<.a, b>. | (a e. J /\ b = (f"a))} Fn J)
15	12, 14	sylib 215	. . . . . . . . . . . . . . . . 17 |- (((J e. Top /\ K e. Top /\ f e. (J Homeo K)) /\ (f:U.J-1-1-onto->U.K /\ A.x e. J (f"x) e. K /\ A.x e. K (`'f"x) e. J)) -> {<.a, b>. | (a e. J /\ b = (f"a))} Fn J)
16		eleq1 1957	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (b = (f"a) -> (b e. K <-> (f"a) e. K))
17	16	imbi2d 674	. . . . . . . . . . . . . . . . . . . . . . 23 |- (b = (f"a) -> ((((J e. Top /\ K e. Top /\ f e. (J Homeo K)) /\ (f:U.J-1-1-onto->U.K /\ A.x e. J (f"x) e. K /\ A.x e. K (`'f"x) e. J)) -> b e. K) <-> (((J e. Top /\ K e. Top /\ f e. (J Homeo K)) /\ (f:U.J-1-1-onto->U.K /\ A.x e. J (f"x) e. K /\ A.x e. K (`'f"x) e. J)) -> (f"a) e. K)))
18		imaeq2 4260	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (x = a -> (f"x) = (f"a))
19	18	eleq1d 1963	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (x = a -> ((f"x) e. K <-> (f"a) e. K))
20	19	rcla4va 2378	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((a e. J /\ A.x e. J (f"x) e. K) -> (f"a) e. K)
21	20	expcom 403	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (A.x e. J (f"x) e. K -> (a e. J -> (f"a) e. K))
22	21	3ad2ant2 898	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((f:U.J-1-1-onto->U.K /\ A.x e. J (f"x) e. K /\ A.x e. K (`'f"x) e. J) -> (a e. J -> (f"a) e. K))
23	22	adantl 424	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((J e. Top /\ K e. Top /\ f e. (J Homeo K)) /\ (f:U.J-1-1-onto->U.K /\ A.x e. J (f"x) e. K /\ A.x e. K (`'f"x) e. J)) -> (a e. J -> (f"a) e. K))
24	23	com12 14	. . . . . . . . . . . . . . . . . . . . . . 23 |- (a e. J -> (((J e. Top /\ K e. Top /\ f e. (J Homeo K)) /\ (f:U.J-1-1-onto->U.K /\ A.x e. J (f"x) e. K /\ A.x e. K (`'f"x) e. J)) -> (f"a) e. K))
25	17, 24	syl5cbir 228	. . . . . . . . . . . . . . . . . . . . . 22 |- (a e. J -> (b = (f"a) -> (((J e. Top /\ K e. Top /\ f e. (J Homeo K)) /\ (f:U.J-1-1-onto->U.K /\ A.x e. J (f"x) e. K /\ A.x e. K (`'f"x) e. J)) -> b e. K)))
26	25	r19.23aiv 2211	. . . . . . . . . . . . . . . . . . . . 21 |- (E.a e. J b = (f"a) -> (((J e. Top /\ K e. Top /\ f e. (J Homeo K)) /\ (f:U.J-1-1-onto->U.K /\ A.x e. J (f"x) e. K /\ A.x e. K (`'f"x) e. J)) -> b e. K))
27	26	com12 14	. . . . . . . . . . . . . . . . . . . 20 |- (((J e. Top /\ K e. Top /\ f e. (J Homeo K)) /\ (f:U.J-1-1-onto->U.K /\ A.x e. J (f"x) e. K /\ A.x e. K (`'f"x) e. J)) -> (E.a e. J b = (f"a) -> b e. K))
28	27	19.21aiv 1664	. . . . . . . . . . . . . . . . . . 19 |- (((J e. Top /\ K e. Top /\ f e. (J Homeo K)) /\ (f:U.J-1-1-onto->U.K /\ A.x e. J (f"x) e. K /\ A.x e. K (`'f"x) e. J)) -> A.b(E.a e. J b = (f"a) -> b e. K))
29		abss 2676	. . . . . . . . . . . . . . . . . . 19 |- ({b | E.a e. J b = (f"a)} C_ K <-> A.b(E.a e. J b = (f"a) -> b e. K))
30	28, 29	sylibr 217	. . . . . . . . . . . . . . . . . 18 |- (((J e. Top /\ K e. Top /\ f e. (J Homeo K)) /\ (f:U.J-1-1-onto->U.K /\ A.x e. J (f"x) e. K /\ A.x e. K (`'f"x) e. J)) -> {b | E.a e. J b = (f"a)} C_ K)
31		rnopab2 4202	. . . . . . . . . . . . . . . . . 18 |- ran {<.a, b>. | (a e. J /\ b = (f"a))} = {b | E.a e. J b = (f"a)}
32	30, 31	syl5ss 2661	. . . . . . . . . . . . . . . . 17 |- (((J e. Top /\ K e. Top /\ f e. (J Homeo K)) /\ (f:U.J-1-1-onto->U.K /\ A.x e. J (f"x) e. K /\ A.x e. K (`'f"x) e. J)) -> ran {<.a, b>. | (a e. J /\ b = (f"a))} C_ K)
33	15, 32	jca 310	. . . . . . . . . . . . . . . 16 |- (((J e. Top /\ K e. Top /\ f e. (J Homeo K)) /\ (f:U.J-1-1-onto->U.K /\ A.x e. J (f"x) e. K /\ A.x e. K (`'f"x) e. J)) -> ({<.a, b>. | (a e. J /\ b = (f"a))} Fn J /\ ran {<.a, b>. | (a e. J /\ b = (f"a))} C_ K))
34		df-f 4010	. . . . . . . . . . . . . . . 16 |- ({<.a, b>. | (a e. J /\ b = (f"a))}:J-->K <-> ({<.a, b>. | (a e. J /\ b = (f"a))} Fn J /\ ran {<.a, b>. | (a e. J /\ b = (f"a))} C_ K))
35	33, 34	sylibr 217	. . . . . . . . . . . . . . 15 |- (((J e. Top /\ K e. Top /\ f e. (J Homeo K)) /\ (f:U.J-1-1-onto->U.K /\ A.x e. J (f"x) e. K /\ A.x e. K (`'f"x) e. J)) -> {<.a, b>. | (a e. J /\ b = (f"a))}:J-->K)
36		f1of1 4634	. . . . . . . . . . . . . . . . . . . . . 22 |- (f:U.J-1-1-onto->U.K -> f:U.J-1-1->U.K)
37		imaeq2 4260	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (a = m -> (f"a) = (f"m))
38	37, 13	fvopab4g 4742	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((m e. J /\ (f"m) e. _V) -> ({<.a, b>. | (a e. J /\ b = (f"a))}` m) = (f"m))
39	38	ex 402	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (m e. J -> ((f"m) e. _V -> ({<.a, b>. | (a e. J /\ b = (f"a))}` m) = (f"m)))
40		imaeq2 4260	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (a = n -> (f"a) = (f"n))
41	40, 13	fvopab4g 4742	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((n e. J /\ (f"n) e. _V) -> ({<.a, b>. | (a e. J /\ b = (f"a))}` n) = (f"n))
42	41	ex 402	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (n e. J -> ((f"n) e. _V -> ({<.a, b>. | (a e. J /\ b = (f"a))}` n) = (f"n)))
43	39, 42	im2anan9 622	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((m e. J /\ n e. J) -> (((f"m) e. _V /\ (f"n) e. _V) -> (({<.a, b>. | (a e. J /\ b = (f"a))}` m) = (f"m) /\ ({<.a, b>. | (a e. J /\ b = (f"a))}` n) = (f"n))))
44		eqtr 1904	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (((f"m) = ({<.a, b>. | (a e. J /\ b = (f"a))}` m) /\ ({<.a, b>. | (a e. J /\ b = (f"a))}` m) = ({<.a, b>. | (a e. J /\ b = (f"a))}` n)) -> (f"m) = ({<.a, b>. | (a e. J /\ b = (f"a))}` n))
45		eqtr 1904	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (((f"m) = ({<.a, b>. | (a e. J /\ b = (f"a))}` n) /\ ({<.a, b>. | (a e. J /\ b = (f"a))}` n) = (f"n)) -> (f"m) = (f"n))
46	45	ex 402	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ((f"m) = ({<.a, b>. | (a e. J /\ b = (f"a))}` n) -> (({<.a, b>. | (a e. J /\ b = (f"a))}` n) = (f"n) -> (f"m) = (f"n)))
47	44, 46	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (((f"m) = ({<.a, b>. | (a e. J /\ b = (f"a))}` m) /\ ({<.a, b>. | (a e. J /\ b = (f"a))}` m) = ({<.a, b>. | (a e. J /\ b = (f"a))}` n)) -> (({<.a, b>. | (a e. J /\ b = (f"a))}` n) = (f"n) -> (f"m) = (f"n)))
48	47	ex 402	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ((f"m) = ({<.a, b>. | (a e. J /\ b = (f"a))}` m) -> (({<.a, b>. | (a e. J /\ b = (f"a))}` m) = ({<.a, b>. | (a e. J /\ b = (f"a))}` n) -> (({<.a, b>. | (a e. J /\ b = (f"a))}` n) = (f"n) -> (f"m) = (f"n))))
49	48	eqcoms 1887	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (({<.a, b>. | (a e. J /\ b = (f"a))}` m) = (f"m) -> (({<.a, b>. | (a e. J /\ b = (f"a))}` m) = ({<.a, b>. | (a e. J /\ b = (f"a))}` n) -> (({<.a, b>. | (a e. J /\ b = (f"a))}` n) = (f"n) -> (f"m) = (f"n))))
50	49	com12 14	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (({<.a, b>. | (a e. J /\ b = (f"a))}` m) = ({<.a, b>. | (a e. J /\ b = (f"a))}` n) -> (({<.a, b>. | (a e. J /\ b = (f"a))}` m) = (f"m) -> (({<.a, b>. | (a e. J /\ b = (f"a))}` n) = (f"n) -> (f"m) = (f"n))))
51	50	imp3a 388	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (({<.a, b>. | (a e. J /\ b = (f"a))}` m) = ({<.a, b>. | (a e. J /\ b = (f"a))}` n) -> ((({<.a, b>. | (a e. J /\ b = (f"a))}` m) = (f"m) /\ ({<.a, b>. | (a e. J /\ b = (f"a))}` n) = (f"n)) -> (f"m) = (f"n)))
52	2	eltopss 8872	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ((J e. Top /\ m e. J) -> m C_ U.J)
53	52	ex 402	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (J e. Top -> (m e. J -> m C_ U.J))
54	2	eltopss 8872	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ((J e. Top /\ n e. J) -> n C_ U.J)
55	54	ex 402	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (J e. Top -> (n e. J -> n C_ U.J))
56	53, 55	anim12d 617	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (J e. Top -> ((m e. J /\ n e. J) -> (m C_ U.J /\ n C_ U.J)))
57	56	adantr 425	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ((J e. Top /\ K e. Top) -> ((m e. J /\ n e. J) -> (m C_ U.J /\ n C_ U.J)))
58		oooeqim2 14356	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ((f:U.J-1-1->U.K /\ m C_ U.J /\ n C_ U.J) -> ((f"m) = (f"n) <-> m = n))
59	58	biimpd 170	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ((f:U.J-1-1->U.K /\ m C_ U.J /\ n C_ U.J) -> ((f"m) = (f"n) -> m = n))
60	59	3expib 1070	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (f:U.J-1-1->U.K -> ((m C_ U.J /\ n C_ U.J) -> ((f"m) = (f"n) -> m = n)))
61	60	com12 14	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ((m C_ U.J /\ n C_ U.J) -> (f:U.J-1-1->U.K -> ((f"m) = (f"n) -> m = n)))
62	57, 61	syl6 25	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ((J e. Top /\ K e. Top) -> ((m e. J /\ n e. J) -> (f:U.J-1-1->U.K -> ((f"m) = (f"n) -> m = n))))
63	62	com24 41	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ((J e. Top /\ K e. Top) -> ((f"m) = (f"n) -> (f:U.J-1-1->U.K -> ((m e. J /\ n e. J) -> m = n))))
64	63	com12 14	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((f"m) = (f"n) -> ((J e. Top /\ K e. Top) -> (f:U.J-1-1->U.K -> ((m e. J /\ n e. J) -> m = n))))
65	51, 64	syl6 25	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (({<.a, b>. | (a e. J /\ b = (f"a))}` m) = ({<.a, b>. | (a e. J /\ b = (f"a))}` n) -> ((({<.a, b>. | (a e. J /\ b = (f"a))}` m) = (f"m) /\ ({<.a, b>. | (a e. J /\ b = (f"a))}` n) = (f"n)) -> ((J e. Top /\ K e. Top) -> (f:U.J-1-1->U.K -> ((m e. J /\ n e. J) -> m = n)))))
66	65	imp3a 388	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (({<.a, b>. | (a e. J /\ b = (f"a))}` m) = ({<.a, b>. | (a e. J /\ b = (f"a))}` n) -> (((({<.a, b>. | (a e. J /\ b = (f"a))}` m) = (f"m) /\ ({<.a, b>. | (a e. J /\ b = (f"a))}` n) = (f"n)) /\ (J e. Top /\ K e. Top)) -> (f:U.J-1-1->U.K -> ((m e. J /\ n e. J) -> m = n))))
67	66	com14 42	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((m e. J /\ n e. J) -> (((({<.a, b>. | (a e. J /\ b = (f"a))}` m) = (f"m) /\ ({<.a, b>. | (a e. J /\ b = (f"a))}` n) = (f"n)) /\ (J e. Top /\ K e. Top)) -> (f:U.J-1-1->U.K -> (({<.a, b>. | (a e. J /\ b = (f"a))}` m) = ({<.a, b>. | (a e. J /\ b = (f"a))}` n) -> m = n))))
68	67	exp3a 405	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((m e. J /\ n e. J) -> ((({<.a, b>. | (a e. J /\ b = (f"a))}` m) = (f"m) /\ ({<.a, b>. | (a e. J /\ b = (f"a))}` n) = (f"n)) -> ((J e. Top /\ K e. Top) -> (f:U.J-1-1->U.K -> (({<.a, b>. | (a e. J /\ b = (f"a))}` m) = ({<.a, b>. | (a e. J /\ b = (f"a))}` n) -> m = n)))))
69	43, 68	syld 30	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((m e. J /\ n e. J) -> (((f"m) e. _V /\ (f"n) e. _V) -> ((J e. Top /\ K e. Top) -> (f:U.J-1-1->U.K -> (({<.a, b>. | (a e. J /\ b = (f"a))}` m) = ({<.a, b>. | (a e. J /\ b = (f"a))}` n) -> m = n)))))
70	69	com14 42	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (f:U.J-1-1->U.K -> (((f"m) e. _V /\ (f"n) e. _V) -> ((J e. Top /\ K e. Top) -> ((m e. J /\ n e. J) -> (({<.a, b>. | (a e. J /\ b = (f"a))}` m) = ({<.a, b>. | (a e. J /\ b = (f"a))}` n) -> m = n)))))
71		imaexg 4279	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (f e. _V -> (f"m) e. _V)
72		imaexg 4279	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (f e. _V -> (f"n) e. _V)
73	71, 72	anim12i 360	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((f e. _V /\ f e. _V) -> ((f"m) e. _V /\ (f"n) e. _V))
74	70, 73	syl5com 63	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((f e. _V /\ f e. _V) -> (f:U.J-1-1->U.K -> ((J e. Top /\ K e. Top) -> ((m e. J /\ n e. J) -> (({<.a, b>. | (a e. J /\ b = (f"a))}` m) = ({<.a, b>. | (a e. J /\ b = (f"a))}` n) -> m = n)))))
75	8, 8, 74	mp2an 761	. . . . . . . . . . . . . . . . . . . . . 22 |- (f:U.J-1-1->U.K -> ((J e. Top /\ K e. Top) -> ((m e. J /\ n e. J) -> (({<.a, b>. | (a e. J /\ b = (f"a))}` m) = ({<.a, b>. | (a e. J /\ b = (f"a))}` n) -> m = n))))
76	36, 75	syl 12	. . . . . . . . . . . . . . . . . . . . 21 |- (f:U.J-1-1-onto->U.K -> ((J e. Top /\ K e. Top) -> ((m e. J /\ n e. J) -> (({<.a, b>. | (a e. J /\ b = (f"a))}` m) = ({<.a, b>. | (a e. J /\ b = (f"a))}` n) -> m = n))))
77	76	com12 14	. . . . . . . . . . . . . . . . . . . 20 |- ((J e. Top /\ K e. Top) -> (f:U.J-1-1-onto->U.K -> ((m e. J /\ n e. J) -> (({<.a, b>. | (a e. J /\ b = (f"a))}` m) = ({<.a, b>. | (a e. J /\ b = (f"a))}` n) -> m = n))))
78	77	3adant3 896	. . . . . . . . . . . . . . . . . . 19 |- ((J e. Top /\ K e. Top /\ f e. (J Homeo K)) -> (f:U.J-1-1-onto->U.K -> ((m e. J /\ n e. J) -> (({<.a, b>. | (a e. J /\ b = (f"a))}` m) = ({<.a, b>. | (a e. J /\ b = (f"a))}` n) -> m = n))))
79	78	com12 14	. . . . . . . . . . . . . . . . . 18 |- (f:U.J-1-1-onto->U.K -> ((J e. Top /\ K e. Top /\ f e. (J Homeo K)) -> ((m e. J /\ n e. J) -> (({<.a, b>. | (a e. J /\ b = (f"a))}` m) = ({<.a, b>. | (a e. J /\ b = (f"a))}` n) -> m = n))))
80	79	3ad2ant1 897	. . . . . . . . . . . . . . . . 17 |- ((f:U.J-1-1-onto->U.K /\ A.x e. J (f"x) e. K /\ A.x e. K (`'f"x) e. J) -> ((J e. Top /\ K e. Top /\ f e. (J Homeo K)) -> ((m e. J /\ n e. J) -> (({<.a, b>. | (a e. J /\ b = (f"a))}` m) = ({<.a, b>. | (a e. J /\ b = (f"a))}` n) -> m = n))))
81	80	impcom 378	. . . . . . . . . . . . . . . 16 |- (((J e. Top /\ K e. Top /\ f e. (J Homeo K)) /\ (f:U.J-1-1-onto->U.K /\ A.x e. J (f"x) e. K /\ A.x e. K (`'f"x) e. J)) -> ((m e. J /\ n e. J) -> (({<.a, b>. | (a e. J /\ b = (f"a))}` m) = ({<.a, b>. | (a e. J /\ b = (f"a))}` n) -> m = n)))
82	81	r19.21aivv 2183	. . . . . . . . . . . . . . 15 |- (((J e. Top /\ K e. Top /\ f e. (J Homeo K)) /\ (f:U.J-1-1-onto->U.K /\ A.x e. J (f"x) e. K /\ A.x e. K (`'f"x) e. J)) -> A.m e. J A.n e. J (({<.a, b>. | (a e. J /\ b = (f"a))}` m) = ({<.a, b>. | (a e. J /\ b = (f"a))}` n) -> m = n))
83	35, 82	jca 310	. . . . . . . . . . . . . 14 |- (((J e. Top /\ K e. Top /\ f e. (J Homeo K)) /\ (f:U.J-1-1-onto->U.K /\ A.x e. J (f"x) e. K /\ A.x e. K (`'f"x) e. J)) -> ({<.a, b>. | (a e. J /\ b = (f"a))}:J-->K /\ A.m e. J A.n e. J (({<.a, b>. | (a e. J /\ b = (f"a))}` m) = ({<.a, b>. | (a e. J /\ b = (f"a))}` n) -> m = n)))
84		dff13 4850	. . . . . . . . . . . . . 14 |- ({<.a, b>. | (a e. J /\ b = (f"a))}:J-1-1->K <-> ({<.a, b>. | (a e. J /\ b = (f"a))}:J-->K /\ A.m e. J A.n e. J (({<.a, b>. | (a e. J /\ b = (f"a))}` m) = ({<.a, b>. | (a e. J /\ b = (f"a))}` n) -> m = n)))
85	83, 84	sylibr 217	. . . . . . . . . . . . 13 |- (((J e. Top /\ K e. Top /\ f e. (J Homeo K)) /\ (f:U.J-1-1-onto->U.K /\ A.x e. J (f"x) e. K /\ A.x e. K (`'f"x) e. J)) -> {<.a, b>. | (a e. J /\ b = (f"a))}:J-1-1->K)
86		hbra1 2147	. . . . . . . . . . . . . . . . . . . . . . 23 |- (A.x e. J (f"x) e. K -> A.xA.x e. J (f"x) e. K)
87		ax-17 1317	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((J e. Top /\ K e. Top /\ f e. (J Homeo K)) -> A.x(J e. Top /\ K e. Top /\ f e. (J Homeo K)))
88	86, 87	hban 1356	. . . . . . . . . . . . . . . . . . . . . 22 |- ((A.x e. J (f"x) e. K /\ (J e. Top /\ K e. Top /\ f e. (J Homeo K))) -> A.x(A.x e. J (f"x) e. K /\ (J e. Top /\ K e. Top /\ f e. (J Homeo K))))
89	19	rcla4v 2376	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (a e. J -> (A.x e. J (f"x) e. K -> (f"a) e. K))
90		eleq1a 1966	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((f"a) e. K -> (x = (f"a) -> x e. K))
91	90	a1d 15	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((f"a) e. K -> ((J e. Top /\ K e. Top /\ f e. (J Homeo K)) -> (x = (f"a) -> x e. K)))
92	89, 91	syl6 25	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (a e. J -> (A.x e. J (f"x) e. K -> ((J e. Top /\ K e. Top /\ f e. (J Homeo K)) -> (x = (f"a) -> x e. K))))
93	92	com3l 38	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (A.x e. J (f"x) e. K -> ((J e. Top /\ K e. Top /\ f e. (J Homeo K)) -> (a e. J -> (x = (f"a) -> x e. K))))
94	93	imp 377	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((A.x e. J (f"x) e. K /\ (J e. Top /\ K e. Top /\ f e. (J Homeo K))) -> (a e. J -> (x = (f"a) -> x e. K)))
95	94	com3l 38	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (a e. J -> (x = (f"a) -> ((A.x e. J (f"x) e. K /\ (J e. Top /\ K e. Top /\ f e. (J Homeo K))) -> x e. K)))
96	95	r19.23aiv 2211	. . . . . . . . . . . . . . . . . . . . . . 23 |- (E.a e. J x = (f"a) -> ((A.x e. J (f"x) e. K /\ (J e. Top /\ K e. Top /\ f e. (J Homeo K))) -> x e. K))
97	96	com12 14	. . . . . . . . . . . . . . . . . . . . . 22 |- ((A.x e. J (f"x) e. K /\ (J e. Top /\ K e. Top /\ f e. (J Homeo K))) -> (E.a e. J x = (f"a) -> x e. K))
98	88, 97	19.21ai 1345	. . . . . . . . . . . . . . . . . . . . 21 |- ((A.x e. J (f"x) e. K /\ (J e. Top /\ K e. Top /\ f e. (J Homeo K))) -> A.x(E.a e. J x = (f"a) -> x e. K))
99	98	ex 402	. . . . . . . . . . . . . . . . . . . 20 |- (A.x e. J (f"x) e. K -> ((J e. Top /\ K e. Top /\ f e. (J Homeo K)) -> A.x(E.a e. J x = (f"a) -> x e. K)))
100	99	3ad2ant2 898	. . . . . . . . . . . . . . . . . . 19 |- ((f:U.J-1-1-onto->U.K /\ A.x e. J (f"x) e. K /\ A.x e. K (`'f"x) e. J) -> ((J e. Top /\ K e. Top /\ f e. (J Homeo K)) -> A.x(E.a e. J x = (f"a) -> x e. K)))
101	100	impcom 378	. . . . . . . . . . . . . . . . . 18 |- (((J e. Top /\ K e. Top /\ f e. (J Homeo K)) /\ (f:U.J-1-1-onto->U.K /\ A.x e. J (f"x) e. K /\ A.x e. K (`'f"x) e. J)) -> A.x(E.a e. J x = (f"a) -> x e. K))
102		ax-17 1317	. . . . . . . . . . . . . . . . . . . . . 22 |- (f:U.J-1-1-onto->U.K -> A.x f:U.J-1-1-onto->U.K)
103		hbra1 2147	. . . . . . . . . . . . . . . . . . . . . 22 |- (A.x e. K (`'f"x) e. J -> A.xA.x e. K (`'f"x) e. J)
104	102, 103	hban 1356	. . . . . . . . . . . . . . . . . . . . 21 |- ((f:U.J-1-1-onto->U.K /\ A.x e. K (`'f"x) e. J) -> A.x(f:U.J-1-1-onto->U.K /\ A.x e. K (`'f"x) e. J))
105		ra4 2155	. . . . . . . . . . . . . . . . . . . . . . 23 |- (A.x e. K (`'f"x) e. J -> (x e. K -> (`'f"x) e. J))
106		elssuni 3206	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (x e. K -> x C_ U.K)
107		imaeq2 4260	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (a = (`'f"x) -> (f"a) = (f"(`'f"x)))
108		eqeq1 1890	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ((f"a) = (f"(`'f"x)) -> ((f"a) = x <-> (f"(`'f"x)) = x))
109		eqcom 1886	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (x = (f"a) <-> (f"a) = x)
110	108, 109	syl5bb 591	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ((f"a) = (f"(`'f"x)) -> (x = (f"a) <-> (f"(`'f"x)) = x))
111	107, 110	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (a = (`'f"x) -> (x = (f"a) <-> (f"(`'f"x)) = x))
112	111	rcla4ev 2381	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (((`'f"x) e. J /\ (f"(`'f"x)) = x) -> E.a e. J x = (f"a))
113	112	ex 402	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((`'f"x) e. J -> ((f"(`'f"x)) = x -> E.a e. J x = (f"a)))
114		f2imacnv 14355	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((f:U.J-1-1-onto->U.K /\ x C_ U.K) -> (f"(`'f"x)) = x)
115	113, 114	syl5com 63	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((f:U.J-1-1-onto->U.K /\ x C_ U.K) -> ((`'f"x) e. J -> E.a e. J x = (f"a)))
116	115	ex 402	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (f:U.J-1-1-onto->U.K -> (x C_ U.K -> ((`'f"x) e. J -> E.a e. J x = (f"a))))
117	116	com3l 38	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (x C_ U.K -> ((`'f"x) e. J -> (f:U.J-1-1-onto->U.K -> E.a e. J x = (f"a))))
118	106, 117	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (x e. K -> ((`'f"x) e. J -> (f:U.J-1-1-onto->U.K -> E.a e. J x = (f"a))))
119	118	imim2d 28	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (x e. K -> ((x e. K -> (`'f"x) e. J) -> (x e. K -> (f:U.J-1-1-onto->U.K -> E.a e. J x = (f"a)))))
120	119	pm2.43a 80	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (x e. K -> ((x e. K -> (`'f"x) e. J) -> (f:U.J-1-1-onto->U.K -> E.a e. J x = (f"a))))
121	120	com3l 38	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((x e. K -> (`'f"x) e. J) -> (f:U.J-1-1-onto->U.K -> (x e. K -> E.a e. J x = (f"a))))
122	105, 121	syl 12	. . . . . . . . . . . . . . . . . . . . . 22 |- (A.x e. K (`'f"x) e. J -> (f:U.J-1-1-onto->U.K -> (x e. K -> E.a e. J x = (f"a))))
123	122	impcom 378	. . . . . . . . . . . . . . . . . . . . 21 |- ((f:U.J-1-1-onto->U.K /\ A.x e. K (`'f"x) e. J) -> (x e. K -> E.a e. J x = (f"a)))
124	104, 123	19.21ai 1345	. . . . . . . . . . . . . . . . . . . 20 |- ((f:U.J-1-1-onto->U.K /\ A.x e. K (`'f"x) e. J) -> A.x(x e. K -> E.a e. J x = (f"a)))
125	124	3adant2 895	. . . . . . . . . . . . . . . . . . 19 |- ((f:U.J-1-1-onto->U.K /\ A.x e. J (f"x) e. K /\ A.x e. K (`'f"x) e. J) -> A.x(x e. K -> E.a e. J x = (f"a)))
126	125	adantl 424	. . . . . . . . . . . . . . . . . 18 |- (((J e. Top /\ K e. Top /\ f e. (J Homeo K)) /\ (f:U.J-1-1-onto->U.K /\ A.x e. J (f"x) e. K /\ A.x e. K (`'f"x) e. J)) -> A.x(x e. K -> E.a e. J x = (f"a)))
127	101, 126	jca 310	. . . . . . . . . . . . . . . . 17 |- (((J e. Top /\ K e. Top /\ f e. (J Homeo K)) /\ (f:U.J-1-1-onto->U.K /\ A.x e. J (f"x) e. K /\ A.x e. K (`'f"x) e. J)) -> (A.x(E.a e. J x = (f"a) -> x e. K) /\ A.x(x e. K -> E.a e. J x = (f"a))))
128		albiim 1465	. . . . . . . . . . . . . . . . 17 |- (A.x(E.a e. J x = (f"a) <-> x e. K) <-> (A.x(E.a e. J x = (f"a) -> x e. K) /\ A.x(x e. K -> E.a e. J x = (f"a))))
129	127, 128	sylibr 217	. . . . . . . . . . . . . . . 16 |- (((J e. Top /\ K e. Top /\ f e. (J Homeo K)) /\ (f:U.J-1-1-onto->U.K /\ A.x e. J (f"x) e. K /\ A.x e. K (`'f"x) e. J)) -> A.x(E.a e. J x = (f"a) <-> x e. K))
130		ax-17 1317	. . . . . . . . . . . . . . . . 17 |- ((E.a e. J x = (f"a) <-> x e. K) -> A.b(E.a e. J x = (f"a) <-> x e. K))
131		ax-17 1317	. . . . . . . . . . . . . . . . 17 |- ((E.a e. J b = (f"a) <-> b e. K) -> A.x(E.a e. J b = (f"a) <-> b e. K))
132		ax-17 1317	. . . . . . . . . . . . . . . . . . 19 |- (x = b -> A.a x = b)
133		eqeq1 1890	. . . . . . . . . . . . . . . . . . 19 |- (x = b -> (x = (f"a) <-> b = (f"a)))
134	132, 133	rexbid 2122	. . . . . . . . . . . . . . . . . 18 |- (x = b -> (E.a e. J x = (f"a) <-> E.a e. J b = (f"a)))
135		eleq1 1957	. . . . . . . . . . . . . . . . . 18 |- (x = b -> (x e. K <-> b e. K))
136	134, 135	bibi12d 691	. . . . . . . . . . . . . . . . 17 |- (x = b -> ((E.a e. J x = (f"a) <-> x e. K) <-> (E.a e. J b = (f"a) <-> b e. K)))
137	130, 131, 136	cbval 1527	. . . . . . . . . . . . . . . 16 |- (A.x(E.a e. J x = (f"a) <-> x e. K) <-> A.b(E.a e. J b = (f"a) <-> b e. K))
138	129, 137	sylib 215	. . . . . . . . . . . . . . 15 |- (((J e. Top /\ K e. Top /\ f e. (J Homeo K)) /\ (f:U.J-1-1-onto->U.K /\ A.x e. J (f"x) e. K /\ A.x e. K (`'f"x) e. J)) -> A.b(E.a e. J b = (f"a) <-> b e. K))
139		abeq1 2000	. . . . . . . . . . . . . . 15 |- ({b | E.a e. J b = (f"a)} = K <-> A.b(E.a e. J b = (f"a) <-> b e. K))
140	138, 139	sylibr 217	. . . . . . . . . . . . . 14 |- (((J e. Top /\ K e. Top /\ f e. (J Homeo K)) /\ (f:U.J-1-1-onto->U.K /\ A.x e. J (f"x) e. K /\ A.x e. K (`'f"x) e. J)) -> {b | E.a e. J b = (f"a)} = K)
141	140, 31	syl5eq 1940	. . . . . . . . . . . . 13 |- (((J e. Top /\ K e. Top /\ f e. (J Homeo K)) /\ (f:U.J-1-1-onto->U.K /\ A.x e. J (f"x) e. K /\ A.x e. K (`'f"x) e. J)) -> ran {<.a, b>. | (a e. J /\ b = (f"a))} = K)
142	85, 141	jca 310	. . . . . . . . . . . 12 |- (((J e. Top /\ K e. Top /\ f e. (J Homeo K)) /\ (f:U.J-1-1-onto->U.K /\ A.x e. J (f"x) e. K /\ A.x e. K (`'f"x) e. J)) -> ({<.a, b>. | (a e. J /\ b = (f"a))}:J-1-1->K /\ ran {<.a, b>. | (a e. J /\ b = (f"a))} = K))
143		dff1o5 4646	. . . . . . . . . . . 12 |- ({<.a, b>. | (a e. J /\ b = (f"a))}:J-1-1-onto->K <-> ({<.a, b>. | (a e. J /\ b = (f"a))}:J-1-1->K /\ ran {<.a, b>. | (a e. J /\ b = (f"a))} = K))
144	142, 143	sylibr 217	. . . . . . . . . . 11 |- (((J e. Top /\ K e. Top /\ f e. (J Homeo K)) /\ (f:U.J-1-1-onto->U.K /\ A.x e. J (f"x) e. K /\ A.x e. K (`'f"x) e. J)) -> {<.a, b>. | (a e. J /\ b = (f"a))}:J-1-1-onto->K)
145		f1oeq1 4630	. . . . . . . . . . . 12 |- (g = {<.a, b>. | (a e. J /\ b = (f"a))} -> (g:J-1-1-onto->K <-> {<.a, b>. | (a e. J /\ b = (f"a))}:J-1-1-onto->K))
146	145	cla4egv 2365	. . . . . . . . . . 11 |- ({<.a, b>. | (a e. J /\ b = (f"a))} e. _V -> ({<.a, b>. | (a e. J /\ b = (f"a))}:J-1-1-onto->K -> E.g g:J-1-1-onto->K))
147	7, 144, 146	sylc 83	. . . . . . . . . 10 |- (((J e. Top /\ K e. Top /\ f e. (J Homeo K)) /\ (f:U.J-1-1-onto->U.K /\ A.x e. J (f"x) e. K /\ A.x e. K (`'f"x) e. J)) -> E.g g:J-1-1-onto->K)
148		breng 5434	. . . . . . . . . . . 12 |- (K e. Top -> (J ~~ K <-> E.g g:J-1-1-onto->K))
149	148	3ad2ant2 898	. . . . . . . . . . 11 |- ((J e. Top /\ K e. Top /\ f e. (J Homeo K)) -> (J ~~ K <-> E.g g:J-1-1-onto->K))
150	149	adantr 425	. . . . . . . . . 10 |- (((J e. Top /\ K e. Top /\ f e. (J Homeo K)) /\ (f:U.J-1-1-onto->U.K /\ A.x e. J (f"x) e. K /\ A.x e. K (`'f"x) e. J)) -> (J ~~ K <-> E.g g:J-1-1-onto->K))
151	147, 150	mpbird 213	. . . . . . . . 9 |- (((J e. Top /\ K e. Top /\ f e. (J Homeo K)) /\ (f:U.J-1-1-onto->U.K /\ A.x e. J (f"x) e. K /\ A.x e. K (`'f"x) e. J)) -> J ~~ K)
152	151	ex 402	. . . . . . . 8 |- ((J e. Top /\ K e. Top /\ f e. (J Homeo K)) -> ((f:U.J-1-1-onto->U.K /\ A.x e. J (f"x) e. K /\ A.x e. K (`'f"x) e. J) -> J ~~ K))
153	4, 152	sylbid 220	. . . . . . 7 |- ((J e. Top /\ K e. Top /\ f e. (J Homeo K)) -> (f e. (J Homeo K) -> J ~~ K))
154	153	3expia 1069	. . . . . 6 |- ((J e. Top /\ K e. Top) -> (f e. (J Homeo K) -> (f e. (J Homeo K) -> J ~~ K)))
155	154	com3l 38	. . . . 5 |- (f e. (J Homeo K) -> (f e. (J Homeo K) -> ((J e. Top /\ K e. Top) -> J ~~ K)))
156	155	pm2.43i 78	. . . 4 |- (f e. (J Homeo K) -> ((J e. Top /\ K e. Top) -> J ~~ K))
157	156	19.23aiv 1674	. . 3 |- (E.f f e. (J Homeo K) -> ((J e. Top /\ K e. Top) -> J ~~ K))
158	157	com12 14	. 2 |- ((J e. Top /\ K e. Top) -> (E.f f e. (J Homeo K) -> J ~~ K))
159	1, 158	sylbid 220	1 |- ((J e. Top /\ K e. Top) -> (J ~= K -> J ~~ K))

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240   /\ w3a 858  A.wal 1296   = wceq 1298   e. wcel 1300  E.wex 1326  {cab 1871  A.wral 2105  E.wrex 2106  _Vcvv 2292   C_ wss 2593  U.cuni 3177   class class class wbr 3338  {copab 3395  `'ccnv 3985  ran crn 3987  "cima 3989   Fn wfn 3993  -->wf 3994  -1-1->wf1 3995  -1-1-onto->wf1o 3997  ` cfv 3998  (class class class)co 4884   ~~ cen 5423  Topctop 8857   Homeo chomeosm 10230   ~= chomeo 10231

This theorem is referenced by:  homindlem2 14899  homindlem3 14900

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-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-f1 4011  df-fo 4012  df-f1o 4013  df-fv 4014  df-opr 4886  df-oprab 4887  df-en 5427  df-homeo 10232  df-hmph 10233

Copyright terms: Public domain