Theorem homcard 10525

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 10510	. 2 |- ((J e. Top /\ K e. Top) -> (J ~= K <-> E.f f e. (J Homeo K)))
2		eqid 1478	. . . . . . . . 9 |- U.J = U.J
3		eqid 1478	. . . . . . . . 9 |- U.K = U.K
4	2, 3	ishomeo 10503	. . . . . . . 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		f1oeq1 3690	. . . . . . . . . . . 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))
6	5	cla4egv 1866	. . . . . . . . . . 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))
7		opabex2g 3617	. . . . . . . . . . . . 13 |- (J e. Top -> {<.a, b>. | (a e. J /\ b = (f"a))} e. V)
8	7	3ad2ant1 802	. . . . . . . . . . . 12 |- ((J e. Top /\ K e. Top /\ f e. (J Homeo K)) -> {<.a, b>. | (a e. J /\ b = (f"a))} e. V)
9	8	adantr 391	. . . . . . . . . . 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)
10		visset 1816	. . . . . . . . . . . . . . . . . . . . 21 |- f e. V
11		imaexg 3422	. . . . . . . . . . . . . . . . . . . . 21 |- (f e. V -> (f"a) e. V)
12	10, 11	ax-mp 7	. . . . . . . . . . . . . . . . . . . 20 |- (f"a) e. V
13	12	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)
14	13	r19.21aiva 1717	. . . . . . . . . . . . . . . . . 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)
15		eqid 1478	. . . . . . . . . . . . . . . . . . 19 |- {<.a, b>. | (a e. J /\ b = (f"a))} = {<.a, b>. | (a e. J /\ b = (f"a))}
16	15	fnopab2g 3622	. . . . . . . . . . . . . . . . . 18 |- (A.a e. J (f"a) e. V <-> {<.a, b>. | (a e. J /\ b = (f"a))} Fn J)
17	14, 16	sylib 198	. . . . . . . . . . . . . . . . 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)
18		eleq1 1537	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (b = (f"a) -> (b e. K <-> (f"a) e. K))
19	18	imbi2d 614	. . . . . . . . . . . . . . . . . . . . . . 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)))
20		imaeq2 3408	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (x = a -> (f"x) = (f"a))
21	20	eleq1d 1543	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (x = a -> ((f"x) e. K <-> (f"a) e. K))
22	21	rcla4va 1878	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((a e. J /\ A.x e. J (f"x) e. K) -> (f"a) e. K)
23	22	expcom 374	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (A.x e. J (f"x) e. K -> (a e. J -> (f"a) e. K))
24	23	3ad2ant2 803	. . . . . . . . . . . . . . . . . . . . . . . . 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))
25	24	adantl 390	. . . . . . . . . . . . . . . . . . . . . . . 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))
26	25	com12 11	. . . . . . . . . . . . . . . . . . . . . . 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))
27	19, 26	syl5cbir 211	. . . . . . . . . . . . . . . . . . . . . 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)))
28	27	r19.23aiv 1746	. . . . . . . . . . . . . . . . . . . . 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))
29	28	com12 11	. . . . . . . . . . . . . . . . . . . 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))
30	29	19.21aiv 1288	. . . . . . . . . . . . . . . . . . 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))
31		abss 2120	. . . . . . . . . . . . . . . . . . 19 |- ({b | E.a e. J b = (f"a)} (_ K <-> A.b(E.a e. J b = (f"a) -> b e. K))
32	30, 31	sylibr 200	. . . . . . . . . . . . . . . . . 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)} (_ K)
33		rnopab2 3360	. . . . . . . . . . . . . . . . . 18 |- ran {<.a, b>. | (a e. J /\ b = (f"a))} = {b | E.a e. J b = (f"a)}
34	32, 33	syl5ss 2108	. . . . . . . . . . . . . . . . 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))} (_ K)
35	17, 34	jca 288	. . . . . . . . . . . . . . . 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))} (_ K))
36		df-f 3200	. . . . . . . . . . . . . . . 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))} (_ K))
37	35, 36	sylibr 200	. . . . . . . . . . . . . . 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)
38		f1of1 3694	. . . . . . . . . . . . . . . . . . . . . 22 |- (f:U.J-1-1-onto->U.K -> f:U.J-1-1->U.K)
39		imaeq2 3408	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (a = m -> (f"a) = (f"m))
40	39, 15	fvopab4g 3785	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((m e. J /\ (f"m) e. V) -> ({<.a, b>. | (a e. J /\ b = (f"a))}` m) = (f"m))
41	40	ex 373	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (m e. J -> ((f"m) e. V -> ({<.a, b>. | (a e. J /\ b = (f"a))