Theorem ishomeo 10611

Description: The predicate F is a homeomorphism between topology J and topology K. Based on Bourbaki TG I.2.

Hypotheses

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

Assertion

Ref	Expression
ishomeo	|- ((J e. Top /\ K e. Top /\ F e. A) -> (F e. (J Homeo K) <-> (F:X-1-1-onto->Y /\ A.x e. J (F"x) e. K /\ A.x e. K (`'F"x) e. J)))

Distinct variable groups:   x,F   x,J   x,K

Proof of Theorem ishomeo

Step	Hyp	Ref	Expression
1		ishomeo.1	. . . . 5 |- X = U.J
2		ishomeo.2	. . . . 5 |- Y = U.K
3	1, 2	homeofval 10610	. . . 4 |- ((J e. Top /\ K e. Top) -> (J Homeo K) = {f | (f:X-1-1-onto->Y /\ A.x e. J (f"x) e. K /\ A.x e. K (`'f"x) e. J)})
4	3	3adant3 811	. . 3 |- ((J e. Top /\ K e. Top /\ F e. A) -> (J Homeo K) = {f | (f:X-1-1-onto->Y /\ A.x e. J (f"x) e. K /\ A.x e. K (`'f"x) e. J)})
5	4	eleq2d 1588	. 2 |- ((J e. Top /\ K e. Top /\ F e. A) -> (F e. (J Homeo K) <-> F e. {f | (f:X-1-1-onto->Y /\ A.x e. J (f"x) e. K /\ A.x e. K (`'f"x) e. J)}))
6		f1oeq1 3741	. . . . 5 |- (f = F -> (f:X-1-1-onto->Y <-> F:X-1-1-onto->Y))
7		imaeq1 3458	. . . . . . 7 |- (f = F -> (f"x) = (F"x))
8	7	eleq1d 1587	. . . . . 6 |- (f = F -> ((f"x) e. K <-> (F"x) e. K))
9	8	ralbidv 1710	. . . . 5 |- (f = F -> (A.x e. J (f"x) e. K <-> A.x e. J (F"x) e. K))
10		cnveq 3349	. . . . . . . 8 |- (f = F -> `'f = `'F)
11	10	imaeq1d 3460	. . . . . . 7 |- (f = F -> (`'f"x) = (`'F"x))
12	11	eleq1d 1587	. . . . . 6 |- (f = F -> ((`'f"x) e. J <-> (`'F"x) e. J))
13	12	ralbidv 1710	. . . . 5 |- (f = F -> (A.x e. K (`'f"x) e. J <-> A.x e. K (`'F"x) e. J))
14	6, 9, 13	3anbi123d 905	. . . 4 |- (f = F -> ((f:X-1-1-onto->Y /\ A.x e. J (f"x) e. K /\ A.x e. K (`'f"x) e. J) <-> (F:X-1-1-onto->Y /\ A.x e. J (F"x) e. K /\ A.x e. K (`'F"x) e. J)))
15	14	elabg 1946	. . 3 |- (F e. A -> (F e. {f | (f:X-1-1-onto->Y /\ A.x e. J (f"x) e. K /\ A.x e. K (`'f"x) e. J)} <-> (F:X-1-1-onto->Y /\ A.x e. J (F"x) e. K /\ A.x e. K (`'F"x) e. J)))
16	15	3ad2ant3 814	. 2 |- ((J e. Top /\ K e. Top /\ F e. A) -> (F e. {f | (f:X-1-1-onto->Y /\ A.x e. J (f"x) e. K /\ A.x e. K (`'f"x) e. J)} <-> (F:X-1-1-onto->Y /\ A.x e. J (F"x) e. K /\ A.x e. K (`'F"x) e. J)))
17	5, 16	bitrd 539	1 |- ((J e. Top /\ K e. Top /\ F e. A) -> (F e. (J Homeo K) <-> (F:X-1-1-onto->Y /\ A.x e. J (F"x) e. K /\ A.x e. K (`'F"x) e. J)))

Syntax hints:   -> wi 3   <-> wb 153   /\ w3a 787   = wceq 997   e. wcel 999  {cab 1509  A.wral 1692  U.cuni 2557  `'ccnv 3226  "cima 3230  -1-1-onto->wf1o 3238  (class class class)co 4021  Topctop 7680   Homeo chomeosm 10607

This theorem is referenced by:  hmeomap 10612  hmeocna 10613  hmeocnb 10614  cmphmp 10615  idhme 10616  cnvhmpha 10619  cnvhmphb 10620  cnvhmph 10621  hmphsyma 10622  hmphre 10624  homcard 10633  eqindhome 10635  hmeobc 10636

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1003  ax-gen 1004  ax-8 1005  ax-9 1006  ax-10 1007  ax-11 1008  ax-12 1009  ax-13 1010  ax-14 1011  ax-17 1012  ax-4 1014  ax-5o 1016  ax-6o 1019  ax-9o 1164  ax-10o 1182  ax-16 1252  ax-11o 1260  ax-ext 1504  ax-sep 2758  ax-pow 2798  ax-pr 2835  ax-un 2922

This theorem depends on definitions:  df-bi 154  df-or 231  df-an 232  df-3an 789  df-ex 1022  df-sb 1214  df-eu 1424  df-mo 1425  df-clab 1510  df-cleq 1515  df-clel 1518  df-ne 1634  df-ral 1696  df-rex 1697  df-v 1859  df-sbc 1989  df-csb 2052  df-dif 2100  df-un 2101  df-in 2102  df-ss 2104  df-nul 2332  df-pw 2454  df-sn 2464  df-pr 2465  df-op 2468  df-uni 2558  df-br 2675  df-opab 2722  df-id 2891  df-xp 3241  df-rel 3242  df-cnv 3243  df-co 3244  df-dm 3245  df-rn 3246  df-res 3247  df-ima 3248  df-fun 3249  df-fn 3250  df-f 3251  df-f1 3252  df-fo 3253  df-f1o 3254  df-fv 3255  df-opr 4023  df-oprab 4024  df-homeo 10609

Copyright terms: Public domain