hmeobc - Mathbox for Frédéric Liné

Mathbox for Frédéric Liné

< Previous Next >
Related theorems
GIF version

Theorem hmeobc 11048

Description: A homeomorphism is a bicontinuous bijection.

**Hypotheses**
Ref	Expression
hmeobc.1	⊢ X = ∪J
hmeobc.2	⊢ Y = ∪K

**Assertion**
Ref	Expression
hmeobc	⊢ ((J ∈ Top ⋀ K ∈ Top ⋀ F ∈ A) → (F ∈ (J Homeo K) ↔ (F:X–1-1-onto→Y ⋀ F ∈ (J Cn K) ⋀ ^◡F ∈ (K Cn J))))

**Proof of Theorem hmeobc**
Step	Hyp	Ref	Expression
1		3simp1 794	. . . . 5 ⊢ ((F:X–1-1-onto→Y ⋀ ∀x ∈ J (F “ x) ∈ K ⋀ ∀x ∈ K (^◡F “ x) ∈ J) → F:X–1-1-onto→Y)
2	1	adantl 388	. . . 4 ⊢ (((J ∈ Top ⋀ K ∈ Top ⋀ F ∈ A) ⋀ (F:X–1-1-onto→Y ⋀ ∀x ∈ J (F “ x) ∈ K ⋀ ∀x ∈ K (^◡F “ x) ∈ J)) → F:X–1-1-onto→Y)
3		f1of 3797	. . . . . . 7 ⊢ (F:X–1-1-onto→Y → F:X–→Y)
4	3	3ad2ant1 806	. . . . . 6 ⊢ ((F:X–1-1-onto→Y ⋀ ∀x ∈ J (F “ x) ∈ K ⋀ ∀x ∈ K (^◡F “ x) ∈ J) → F:X–→Y)
5	4	adantl 388	. . . . 5 ⊢ (((J ∈ Top ⋀ K ∈ Top ⋀ F ∈ A) ⋀ (F:X–1-1-onto→Y ⋀ ∀x ∈ J (F “ x) ∈ K ⋀ ∀x ∈ K (^◡F “ x) ∈ J)) → F:X–→Y)
6		3simp3 796	. . . . . 6 ⊢ ((F:X–1-1-onto→Y ⋀ ∀x ∈ J (F “ x) ∈ K ⋀ ∀x ∈ K (^◡F “ x) ∈ J) → ∀x ∈ K (^◡F “ x) ∈ J)
7	6	adantl 388	. . . . 5 ⊢ (((J ∈ Top ⋀ K ∈ Top ⋀ F ∈ A) ⋀ (F:X–1-1-onto→Y ⋀ ∀x ∈ J (F “ x) ∈ K ⋀ ∀x ∈ K (^◡F “ x) ∈ J)) → ∀x ∈ K (^◡F “ x) ∈ J)
8	5, 7	jca 286	. . . 4 ⊢ (((J ∈ Top ⋀ K ∈ Top ⋀ F ∈ A) ⋀ (F:X–1-1-onto→Y ⋀ ∀x ∈ J (F “ x) ∈ K ⋀ ∀x ∈ K (^◡F “ x) ∈ J)) → (F:X–→Y ⋀ ∀x ∈ K (^◡F “ x) ∈ J))
9		f1ocnv 3809	. . . . . . . 8 ⊢ (F:X–1-1-onto→Y → ^◡F:Y–1-1-onto→X)
10		f1of 3797	. . . . . . . 8 ⊢ (^◡F:Y–1-1-onto→X → ^◡F:Y–→X)
11	9, 10	syl 10	. . . . . . 7 ⊢ (F:X–1-1-onto→Y → ^◡F:Y–→X)
12	11	3ad2ant1 806	. . . . . 6 ⊢ ((F:X–1-1-onto→Y ⋀ ∀x ∈ J (F “ x) ∈ K ⋀ ∀x ∈ K (^◡F “ x) ∈ J) → ^◡F:Y–→X)
13	12	adantl 388	. . . . 5 ⊢ (((J ∈ Top ⋀ K ∈ Top ⋀ F ∈ A) ⋀ (F:X–1-1-onto→Y ⋀ ∀x ∈ J (F “ x) ∈ K ⋀ ∀x ∈ K (^◡F “ x) ∈ J)) → ^◡F:Y–→X)
14		imacnvcnv 3593	. . . . . . . . . . 11 ⊢ (^◡^◡F “ x) = (F “ x)
15	14	eqcomi 1522	. . . . . . . . . 10 ⊢ (F “ x) = (^◡^◡F “ x)
16	15	eleq1i 1580	. . . . . . . . 9 ⊢ ((F “ x) ∈ K ↔ (^◡^◡F “ x) ∈ K)
17	16	ralbii 1713	. . . . . . . 8 ⊢ (∀x ∈ J (F “ x) ∈ K ↔ ∀x ∈ J (^◡^◡F “ x) ∈ K)
18	17	biimpi 149	. . . . . . 7 ⊢ (∀x ∈ J (F “ x) ∈ K → ∀x ∈ J (^◡^◡F “ x) ∈ K)
19	18	3ad2ant2 807	. . . . . 6 ⊢ ((F:X–1-1-onto→Y ⋀ ∀x ∈ J (F “ x) ∈ K ⋀ ∀x ∈ K (^◡F “ x) ∈ J) → ∀x ∈ J (^◡^◡F “ x) ∈ K)
20	19	adantl 388	. . . . 5 ⊢ (((J ∈ Top ⋀ K ∈ Top ⋀ F ∈ A) ⋀ (F:X–1-1-onto→Y ⋀ ∀x ∈ J (F “ x) ∈ K ⋀ ∀x ∈ K (^◡F “ x) ∈ J)) → ∀x ∈ J (^◡^◡F “ x) ∈ K)
21	13, 20	jca 286	. . . 4 ⊢ (((J ∈ Top ⋀ K ∈ Top ⋀ F ∈ A) ⋀ (F:X–1-1-onto→Y ⋀ ∀x ∈ J (F “ x) ∈ K ⋀ ∀x ∈ K (^◡F “ x) ∈ J)) → (^◡F:Y–→X ⋀ ∀x ∈ J (^◡^◡F “ x) ∈ K))
22	2, 8, 21	3jca 825	. . 3 ⊢ (((J ∈ Top ⋀ K ∈ Top ⋀ F ∈ A) ⋀ (F:X–1-1-onto→Y ⋀ ∀x ∈ J (F “ x) ∈ K ⋀ ∀x ∈ K (^◡F “ x) ∈ J)) → (F:X–1-1-onto→Y ⋀ (F:X–→Y ⋀ ∀x ∈ K (^◡F “ x) ∈ J) ⋀ (^◡F:Y–→X ⋀ ∀x ∈ J (^◡^◡F “ x) ∈ K)))
23		3simp1 794	. . . . 5 ⊢ ((F:X–1-1-onto→Y ⋀ (F:X–→Y ⋀ ∀x ∈ K (^◡F “ x) ∈ J) ⋀ (^◡F:Y–→X ⋀ ∀x ∈ J (^◡^◡F “ x) ∈ K)) → F:X–1-1-onto→Y)
24	23	adantl 388	. . . 4 ⊢ (((J ∈ Top ⋀ K ∈ Top ⋀ F ∈ A) ⋀ (F:X–1-1-onto→Y ⋀ (F:X–→Y ⋀ ∀x ∈ K (^◡F “ x) ∈ J) ⋀ (^◡F:Y–→X ⋀ ∀x ∈ J (^◡^◡F “ x) ∈ K))) → F:X–1-1-onto→Y)
25		frel 3737	. . . . . . . . 9 ⊢ (F:X–→Y → Rel F)
26	14	a1i 8	. . . . . . . . . . . . . . 15 ⊢ (Rel F → (^◡^◡F “ x) = (F “ x))
27	26	eleq1d 1583	. . . . . . . . . . . . . 14 ⊢ (Rel F → ((^◡^◡F “ x) ∈ K ↔ (F “ x) ∈ K))
28	27	ralbidv 1709	. . . . . . . . . . . . 13 ⊢ (Rel F → (∀x ∈ J (^◡^◡F “ x) ∈ K ↔ ∀x ∈ J (F “ x) ∈ K))
29	28	biimpcd 153	. . . . . . . . . . . 12 ⊢ (∀x ∈ J (^◡^◡F “ x) ∈ K → (Rel F → ∀x ∈ J (F “ x) ∈ K))
30	29	adantl 388	. . . . . . . . . . 11 ⊢ ((^◡F:Y–→X ⋀ ∀x ∈ J (^◡^◡F “ x) ∈ K) → (Rel F → ∀x ∈ J (F “ x) ∈ K))
31	30	com12 11	. . . . . . . . . 10 ⊢ (Rel F → ((^◡F:Y–→X ⋀ ∀x ∈ J (^◡^◡F “ x) ∈ K) → ∀x ∈ J (F “ x) ∈ K))
32	31	a1d 12	. . . . . . . . 9 ⊢ (Rel F → (∀x ∈ K (^◡F “ x) ∈ J → ((^◡F:Y–→X ⋀ ∀x ∈ J (^◡^◡F “ x) ∈ K) → ∀x ∈ J (F “ x) ∈ K)))
33	25, 32	syl 10	. . . . . . . 8 ⊢ (F:X–→Y → (∀x ∈ K (^◡F “ x) ∈ J → ((^◡F:Y–→X ⋀ ∀x ∈ J (^◡^◡F “ x) ∈ K) → ∀x ∈ J (F “ x) ∈ K)))
34	33	imp 348	. . . . . . 7 ⊢ ((F:X–→Y ⋀ ∀x ∈ K (^◡F “ x) ∈ J) → ((^◡F:Y–→X ⋀ ∀x ∈ J (^◡^◡F “ x) ∈ K) → ∀x ∈ J (F “ x) ∈ K))
35	34	a1i 8	. . . . . 6 ⊢ (F:X–1-1-onto→Y → ((F:X–→Y ⋀ ∀x ∈ K (^◡F “ x) ∈ J) → ((^◡F:Y–→X ⋀ ∀x ∈ J (^◡^◡F “ x) ∈ K) → ∀x ∈ J (F “ x) ∈ K)))
36	35	3imp 833	. . . . 5 ⊢ ((F:X–1-1-onto→Y ⋀ (F:X–→Y ⋀ ∀x ∈ K (^◡F “ x) ∈ J) ⋀ (^◡F:Y–→X ⋀ ∀x ∈ J (^◡^◡F “ x) ∈ K)) → ∀x ∈ J (F “ x) ∈ K)
37	36	adantl 388	. . . 4 ⊢ (((J ∈ Top ⋀ K ∈ Top ⋀ F ∈ A) ⋀ (F:X–1-1-onto→Y ⋀ (F:X–→Y ⋀ ∀x ∈ K (^◡F “ x) ∈ J) ⋀ (^◡F:Y–→X ⋀ ∀x ∈ J (^◡^◡F “ x) ∈ K))) → ∀x ∈ J (F “ x) ∈ K)
38		simprr 415	. . . . 5 ⊢ (((J ∈ Top ⋀ K ∈ Top ⋀ F ∈ A) ⋀ (F:X–→Y ⋀ ∀x ∈ K (^◡F “ x) ∈ J)) → ∀x ∈ K (^◡F “ x) ∈ J)
39	38	3ad2antr2 819	. . . 4 ⊢ (((J ∈ Top ⋀ K ∈ Top ⋀ F ∈ A) ⋀ (F:X–1-1-onto→Y ⋀ (F:X–→Y ⋀ ∀x ∈ K (^◡F “ x) ∈ J) ⋀ (^◡F:Y–→X ⋀ ∀x ∈ J (^◡^◡F “ x) ∈ K))) → ∀x ∈ K (^◡F “ x) ∈ J)
40	24, 37, 39	3jca 825	. . 3 ⊢ (((J ∈ Top ⋀ K ∈ Top ⋀ F ∈ A) ⋀ (F:X–1-1-onto→Y ⋀ (F:X–→Y ⋀ ∀x ∈ K (^◡F “ x) ∈ J) ⋀ (^◡F:Y–→X ⋀ ∀x ∈ J (^◡^◡F “ x) ∈ K))) → (F:X–1-1-onto→Y ⋀ ∀x ∈ J (F “ x) ∈ K ⋀ ∀x ∈ K (^◡F “ x) ∈ J))
41	22, 40	impbida 522	. 2 ⊢ ((J ∈ Top ⋀ K ∈ Top ⋀ F ∈ A) → ((F:X–1-1-onto→Y ⋀ ∀x ∈ J (F “ x) ∈ K ⋀ ∀x ∈ K (^◡F “ x) ∈ J) ↔ (F:X–1-1-onto→Y ⋀ (F:X–→Y ⋀ ∀x ∈ K (^◡F “ x) ∈ J) ⋀ (^◡F:Y–→X ⋀ ∀x ∈ J (^◡^◡F “ x) ∈ K))))
42		hmeobc.1	. . 3 ⊢ X = ∪J
43		hmeobc.2	. . 3 ⊢ Y = ∪K
44	42, 43	ishomeo 11023	. 2 ⊢ ((J ∈ Top ⋀ K ∈ Top ⋀ F ∈ A) → (F ∈ (J Homeo K) ↔ (F:X–1-1-onto→Y ⋀ ∀x ∈ J (F “ x) ∈ K ⋀ ∀x ∈ K (^◡F “ x) ∈ J)))
45	42, 43	iscn 7968	. . . 4 ⊢ ((J ∈ Top ⋀ K ∈ Top) → (F ∈ (J Cn K) ↔ (F:X–→Y ⋀ ∀x ∈ K (^◡F “ x) ∈ J)))
46	45	3adant3 805	. . 3 ⊢ ((J ∈ Top ⋀ K ∈ Top ⋀ F ∈ A) → (F ∈ (J Cn K) ↔ (F:X–→Y ⋀ ∀x ∈ K (^◡F “ x) ∈ J)))
47	43, 42	iscn 7968	. . . . 5 ⊢ ((K ∈ Top ⋀ J ∈ Top) → (^◡F ∈ (K Cn J) ↔ (^◡F:Y–→X ⋀ ∀x ∈ J (^◡^◡F “ x) ∈ K)))
48	47	ancoms 438	. . . 4 ⊢ ((J ∈ Top ⋀ K ∈ Top) → (^◡F ∈ (K Cn J) ↔ (^◡F:Y–→X ⋀ ∀x ∈ J (^◡^◡F “ x) ∈ K)))
49	48	3adant3 805	. . 3 ⊢ ((J ∈ Top ⋀ K ∈ Top ⋀ F ∈ A) → (^◡F ∈ (K Cn J) ↔ (^◡F:Y–→X ⋀ ∀x ∈ J (^◡^◡F “ x) ∈ K)))
50	46, 49	3anbi23d 902	. 2 ⊢ ((J ∈ Top ⋀ K ∈ Top ⋀ F ∈ A) → ((F:X–1-1-onto→Y ⋀ F ∈ (J Cn K) ⋀ ^◡F ∈ (K Cn J)) ↔ (F:X–1-1-onto→Y ⋀ (F:X–→Y ⋀ ∀x ∈ K (^◡F “ x) ∈ J) ⋀ (^◡F:Y–→X ⋀ ∀x ∈ J (^◡^◡F “ x) ∈ K))))
51	41, 44, 50	3bitr4d 553	1 ⊢ ((J ∈ Top ⋀ K ∈ Top ⋀ F ∈ A) → (F ∈ (J Homeo K) ↔ (F:X–1-1-onto→Y ⋀ F ∈ (J Cn K) ⋀ ^◡F ∈ (K Cn J))))

Colors of variables: wff set class

Syntax hints: → wi 3 ↔ wb 144 ⋀ wa 221 ⋀ w3a 781 = wceq 992 ∈ wcel 994 ∀wral 1691 ∪cuni 2569 ^◡ccnv 3250 “ cima 3254 Rel wrel 3256 –→wf 3259 –1-1-onto→wf1o 3262 (class class class)co 4021 Topctop 7800 Cn ccn 7962 Homeo chomeosm 11019

This theorem is referenced by: hmeoclda 11475 comptoppr 11495 conntoppr 11504 hmeocnv 11959

This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 998 ax-gen 999 ax-8 1000 ax-9 1001 ax-10 1002 ax-11 1003 ax-12 1004 ax-13 1005 ax-14 1006 ax-17 1007 ax-4 1009 ax-5o 1011 ax-6o 1014 ax-9o 1159 ax-10o 1177 ax-16 1247 ax-11o 1255 ax-ext 1500 ax-rep 2767 ax-sep 2777 ax-pow 2818 ax-pr 2855 ax-un 3089

This theorem depends on definitions: df-bi 145 df-or 222 df-an 223 df-3an 783 df-ex 1017 df-sb 1209 df-eu 1421 df-mo 1422 df-clab 1506 df-cleq 1511 df-clel 1514 df-ne 1630 df-ral 1695 df-rex 1696 df-rab 1698 df-v 1858 df-sbc 1987 df-csb 2052 df-dif 2101 df-un 2102 df-in 2103 df-ss 2105 df-nul 2333 df-pw 2459 df-sn 2470 df-pr 2471 df-op 2474 df-uni 2570 df-br 2693 df-opab 2741 df-id 2913 df-xp 3265 df-rel 3266 df-cnv 3267 df-co 3268 df-dm 3269 df-rn 3270 df-res 3271 df-ima 3272 df-fun 3273 df-fn 3274 df-f 3275 df-f1 3276 df-fo 3277 df-f1o 3278 df-fv 3279 df-opr 4023 df-oprab 4024 df-map 4465 df-cn 7964 df-homeo 11021