Theorem hmphsyma 15639

Description: "Is homeomorph to" is symmetric.

Assertion

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

Proof of Theorem hmphsyma

Step	Hyp	Ref	Expression
1		visset 2541	. . . 4 |- f e. _V
2		eqid 2141	. . . . . 6 |- U.J = U.J
3		eqid 2141	. . . . . 6 |- U.K = U.K
4	2, 3	ishomeo 11070	. . . . 5 |- ((J e. Top /\ K e. Top /\ f e. _V) -> (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		cnvexg 4527	. . . . . . . . 9 |- (f e. _V -> `'f e. _V)
6	5	3ad2ant3 1143	. . . . . . . 8 |- ((J e. Top /\ K e. Top /\ f e. _V) -> `'f e. _V)
7	6	adantr 447	. . . . . . 7 |- (((J e. Top /\ K e. Top /\ f e. _V) /\ (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 e. _V)
8		f1orel 4726	. . . . . . . . . . . 12 |- (f:U.J-1-1-onto->U.K -> Rel f)
9	8	3ad2ant1 1141	. . . . . . . . . . 11 |- ((f:U.J-1-1-onto->U.K /\ A.x e. J (f"x) e. K /\ A.x e. K (`'f"x) e. J) -> Rel f)
10	9	adantl 448	. . . . . . . . . 10 |- (((J e. Top /\ K e. Top /\ f e. _V) /\ (f:U.J-1-1-onto->U.K /\ A.x e. J (f"x) e. K /\ A.x e. K (`'f"x) e. J)) -> Rel f)
11		f1ocnv 4735	. . . . . . . . . . . . 13 |- (f:U.J-1-1-onto->U.K -> `'f:U.K-1-1-onto->U.J)
12	11	a1i 8	. . . . . . . . . . . 12 |- ((Rel f /\ (J e. Top /\ K e. Top /\ f e. _V)) -> (f:U.J-1-1-onto->U.K -> `'f:U.K-1-1-onto->U.J))
13		dfrel2 4463	. . . . . . . . . . . . . . . . . . 19 |- (Rel f <-> `'`'f = f)
14	13	biimpi 224	. . . . . . . . . . . . . . . . . 18 |- (Rel f -> `'`'f = f)
15	14	eqcomd 2146	. . . . . . . . . . . . . . . . 17 |- (Rel f -> f = `'`'f)
16	15	imaeq1d 4383	. . . . . . . . . . . . . . . 16 |- (Rel f -> (f"x) = (`'`'f"x))
17	16	eleq1d 2210	. . . . . . . . . . . . . . 15 |- (Rel f -> ((f"x) e. K <-> (`'`'f"x) e. K))
18	17	biimpd 231	. . . . . . . . . . . . . 14 |- (Rel f -> ((f"x) e. K -> (`'`'f"x) e. K))
19	18	ad2antrr 799	. . . . . . . . . . . . 13 |- (((Rel f /\ (J e. Top /\ K e. Top /\ f e. _V)) /\ x e. J) -> ((f"x) e. K -> (`'`'f"x) e. K))
20	19	ralimdva 2421	. . . . . . . . . . . 12 |- ((Rel f /\ (J e. Top /\ K e. Top /\ f e. _V)) -> (A.x e. J (f"x) e. K -> A.x e. J (`'`'f"x) e. K))
21		idd 17	. . . . . . . . . . . 12 |- ((Rel f /\ (J e. Top /\ K e. Top /\ f e. _V)) -> (A.x e. K (`'f"x) e. J -> A.x e. K (`'f"x) e. J))
22	12, 20, 21	3anim123d 1448	. . . . . . . . . . 11 |- ((Rel f /\ (J e. Top /\ K e. Top /\ f e. _V)) -> ((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:U.K-1-1-onto->U.J /\ A.x e. J (`'`'f"x) e. K /\ A.x e. K (`'f"x) e. J)))
23	22	expimpd 576	. . . . . . . . . 10 |- (Rel f -> (((J e. Top /\ K e. Top /\ f e. _V) /\ (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:U.K-1-1-onto->U.J /\ A.x e. J (`'`'f"x) e. K /\ A.x e. K (`'f"x) e. J)))
24	10, 23	mpcom 101	. . . . . . . . 9 |- (((J e. Top /\ K e. Top /\ f e. _V) /\ (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:U.K-1-1-onto->U.J /\ A.x e. J (`'`'f"x) e. K /\ A.x e. K (`'f"x) e. J))
25		3ancomb 1110	. . . . . . . . 9 |- ((`'f:U.K-1-1-onto->U.J /\ A.x e. J (`'`'f"x) e. K /\ A.x e. K (`'f"x) e. J) <-> (`'f:U.K-1-1-onto->U.J /\ A.x e. K (`'f"x) e. J /\ A.x e. J (`'`'f"x) e. K))
26	24, 25	sylib 242	. . . . . . . 8 |- (((J e. Top /\ K e. Top /\ f e. _V) /\ (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:U.K-1-1-onto->U.J /\ A.x e. K (`'f"x) e. J /\ A.x e. J (`'`'f"x) e. K))
27	3, 2	ishomeo 11070	. . . . . . . . . . 11 |- ((K e. Top /\ J e. Top /\ `'f e. _V) -> (`'f e. (K Homeo J) <-> (`'f:U.K-1-1-onto->U.J /\ A.x e. K (`'f"x) e. J /\ A.x e. J (`'`'f"x) e. K)))
28	5, 27	syl3an3 1384	. . . . . . . . . 10 |- ((K e. Top /\ J e. Top /\ f e. _V) -> (`'f e. (K Homeo J) <-> (`'f:U.K-1-1-onto->U.J /\ A.x e. K (`'f"x) e. J /\ A.x e. J (`'`'f"x) e. K)))
29	28	3com12 1321	. . . . . . . . 9 |- ((J e. Top /\ K e. Top /\ f e. _V) -> (`'f e. (K Homeo J) <-> (`'f:U.K-1-1-onto->U.J /\ A.x e. K (`'f"x) e. J /\ A.x e. J (`'`'f"x) e. K)))
30	29	adantr 447	. . . . . . . 8 |- (((J e. Top /\ K e. Top /\ f e. _V) /\ (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 e. (K Homeo J) <-> (`'f:U.K-1-1-onto->U.J /\ A.x e. K (`'f"x) e. J /\ A.x e. J (`'`'f"x) e. K)))
31	26, 30	mpbird 318	. . . . . . 7 |- (((J e. Top /\ K e. Top /\ f e. _V) /\ (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 e. (K Homeo J))
32		eleq1 2204	. . . . . . . 8 |- (g = `'f -> (g e. (K Homeo J) <-> `'f e. (K Homeo J)))
33	32	cla4egv 2605	. . . . . . 7 |- (`'f e. _V -> (`'f e. (K Homeo J) -> E.g g e. (K Homeo J)))
34	7, 31, 33	sylc 44	. . . . . 6 |- (((J e. Top /\ K e. Top /\ f e. _V) /\ (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 e. (K Homeo J))
35	34	ex 398	. . . . 5 |- ((J e. Top /\ K e. Top /\ f e. _V) -> ((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 e. (K Homeo J)))
36	4, 35	sylbid 246	. . . 4 |- ((J e. Top /\ K e. Top /\ f e. _V) -> (f e. (J Homeo K) -> E.g g e. (K Homeo J)))
37	1, 36	mp3an3 1455	. . 3 |- ((J e. Top /\ K e. Top) -> (f e. (J Homeo K) -> E.g g e. (K Homeo J)))
38	37	19.23adv 1860	. 2 |- ((J e. Top /\ K e. Top) -> (E.f f e. (J Homeo K) -> E.g g e. (K Homeo J)))
39		hmph 11076	. 2 |- ((J e. Top /\ K e. Top) -> (J ~= K <-> E.f f e. (J Homeo K)))
40		hmph 11076	. . 3 |- ((K e. Top /\ J e. Top) -> (K ~= J <-> E.g g e. (K Homeo J)))
41	40	ancoms 416	. 2 |- ((J e. Top /\ K e. Top) -> (K ~= J <-> E.g g e. (K Homeo J)))
42	38, 39, 41	3imtr4d 330	1 |- ((J e. Top /\ K e. Top) -> (J ~= K -> K ~= J))

Syntax hints:   -> wi 3   <-> wb 219   /\ wa 337   /\ w3a 1102   = wceq 1586   e. wcel 1588  E.wex 1615  A.wral 2355  _Vcvv 2538  U.cuni 3366   class class class wbr 3507  `'ccnv 4118  "cima 4122  Rel wrel 4124  -1-1-onto->wf1o 4130  (class class class)co 4981  Topctop 9686   Homeo chomeosm 11065   ~= chomeo 11066

This theorem is referenced by:  hmphsym 15640  hmpher 15647  homindlem3 15657

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1592  ax-gen 1593  ax-8 1594  ax-9 1595  ax-10 1596  ax-11 1597  ax-12 1598  ax-13 1599  ax-14 1600  ax-17 1605  ax-4 1608  ax-5o 1610  ax-6o 1613  ax-9o 1763  ax-10o 1781  ax-16 1854  ax-11o 1864  ax-ext 2123  ax-sep 3606  ax-nul 3613  ax-pow 3649  ax-pr 3687  ax-un 3929

This theorem depends on definitions:  df-bi 220  df-or 338  df-an 339  df-3an 1104  df-ex 1616  df-sb 1816  df-eu 2041  df-mo 2042  df-clab 2129  df-cleq 2134  df-clel 2137  df-ne 2268  df-ral 2359  df-rex 2360  df-v 2540  df-sbc 2700  df-csb 2774  df-dif 2830  df-un 2832  df-in 2834  df-ss 2836  df-nul 3083  df-pw 3229  df-sn 3242  df-pr 3243  df-op 3246  df-uni 3367  df-br 3508  df-opab 3566  df-id 3747  df-xp 4133  df-rel 4134  df-cnv 4135  df-co 4136  df-dm 4137  df-rn 4138  df-res 4139  df-ima 4140  df-fun 4141  df-fn 4142  df-f 4143  df-f1 4144  df-fo 4145  df-f1o 4146  df-fv 4147  df-opr 4983  df-oprab 4984  df-homeo 11067  df-hmph 11068

Copyright terms: Public domain