comptoppr - Mathbox for Jeff Hankins

Mathbox for Jeff Hankins

< Previous Next >
Related theorems
GIF version

Theorem comptoppr 11488

Description: Compactness is a topological property-that is, for any two homeomorphic topologies, either both are compact or neither is.

**Assertion**
Ref	Expression
comptoppr	⊢ ((J ∈ Top ⋀ K ∈ Top ⋀ J ~= K) → (J ∈ Comp ↔ K ∈ Comp))

**Proof of Theorem comptoppr**
Step	Hyp	Ref	Expression
1		hmph 11017	. . 3 ⊢ ((J ∈ Top ⋀ K ∈ Top) → (J ~= K ↔ ∃f f ∈ (J Homeo K)))
2		visset 1859	. . . . . 6 ⊢ f ∈ V
3		eqid 1518	. . . . . . 7 ⊢ ∪J = ∪J
4		eqid 1518	. . . . . . 7 ⊢ ∪K = ∪K
5	3, 4	hmeobc 11035	. . . . . 6 ⊢ ((J ∈ Top ⋀ K ∈ Top ⋀ f ∈ V) → (f ∈ (J Homeo K) ↔ (f:∪J–1-1-onto→∪K ⋀ f ∈ (J Cn K) ⋀ ^◡f ∈ (K Cn J))))
6	2, 5	mp3an3 911	. . . . 5 ⊢ ((J ∈ Top ⋀ K ∈ Top) → (f ∈ (J Homeo K) ↔ (f:∪J–1-1-onto→∪K ⋀ f ∈ (J Cn K) ⋀ ^◡f ∈ (K Cn J))))
7	3, 4	cncomp 11487	. . . . . . . . . . . . 13 ⊢ (((J ∈ Comp ⋀ K ∈ Top) ⋀ (f:∪J–onto→∪K ⋀ f ∈ (J Cn K))) → K ∈ Comp)
8	7	exp43 384	. . . . . . . . . . . 12 ⊢ (J ∈ Comp → (K ∈ Top → (f:∪J–onto→∪K → (f ∈ (J Cn K) → K ∈ Comp))))
9	8	com4l 39	. . . . . . . . . . 11 ⊢ (K ∈ Top → (f:∪J–onto→∪K → (f ∈ (J Cn K) → (J ∈ Comp → K ∈ Comp))))
10		f1ofo 3803	. . . . . . . . . . 11 ⊢ (f:∪J–1-1-onto→∪K → f:∪J–onto→∪K)
11	9, 10	syl5 21	. . . . . . . . . 10 ⊢ (K ∈ Top → (f:∪J–1-1-onto→∪K → (f ∈ (J Cn K) → (J ∈ Comp → K ∈ Comp))))
12	11	imp32 361	. . . . . . . . 9 ⊢ ((K ∈ Top ⋀ (f:∪J–1-1-onto→∪K ⋀ f ∈ (J Cn K))) → (J ∈ Comp → K ∈ Comp))
13	12	adantll 392	. . . . . . . 8 ⊢ (((J ∈ Top ⋀ K ∈ Top) ⋀ (f:∪J–1-1-onto→∪K ⋀ f ∈ (J Cn K))) → (J ∈ Comp → K ∈ Comp))
14	13	3adantr3 814	. . . . . . 7 ⊢ (((J ∈ Top ⋀ K ∈ Top) ⋀ (f:∪J–1-1-onto→∪K ⋀ f ∈ (J Cn K) ⋀ ^◡f ∈ (K Cn J))) → (J ∈ Comp → K ∈ Comp))
15	4, 3	cncomp 11487	. . . . . . . . . . . . 13 ⊢ (((K ∈ Comp ⋀ J ∈ Top) ⋀ (^◡f:∪K–onto→∪J ⋀ ^◡f ∈ (K Cn J))) → J ∈ Comp)
16	15	exp43 384	. . . . . . . . . . . 12 ⊢ (K ∈ Comp → (J ∈ Top → (^◡f:∪K–onto→∪J → (^◡f ∈ (K Cn J) → J ∈ Comp))))
17	16	com4l 39	. . . . . . . . . . 11 ⊢ (J ∈ Top → (^◡f:∪K–onto→∪J → (^◡f ∈ (K Cn J) → (K ∈ Comp → J ∈ Comp))))
18		f1ocnv 3809	. . . . . . . . . . . 12 ⊢ (f:∪J–1-1-onto→∪K → ^◡f:∪K–1-1-onto→∪J)
19		f1ofo 3803	. . . . . . . . . . . 12 ⊢ (^◡f:∪K–1-1-onto→∪J → ^◡f:∪K–onto→∪J)
20	18, 19	syl 10	. . . . . . . . . . 11 ⊢ (f:∪J–1-1-onto→∪K → ^◡f:∪K–onto→∪J)
21	17, 20	syl5 21	. . . . . . . . . 10 ⊢ (J ∈ Top → (f:∪J–1-1-onto→∪K → (^◡f ∈ (K Cn J) → (K ∈ Comp → J ∈ Comp))))
22	21	imp32 361	. . . . . . . . 9 ⊢ ((J ∈ Top ⋀ (f:∪J–1-1-onto→∪K ⋀ ^◡f ∈ (K Cn J))) → (K ∈ Comp → J ∈ Comp))
23	22	adantlr 393	. . . . . . . 8 ⊢ (((J ∈ Top ⋀ K ∈ Top) ⋀ (f:∪J–1-1-onto→∪K ⋀ ^◡f ∈ (K Cn J))) → (K ∈ Comp → J ∈ Comp))
24	23	3adantr2 813	. . . . . . 7 ⊢ (((J ∈ Top ⋀ K ∈ Top) ⋀ (f:∪J–1-1-onto→∪K ⋀ f ∈ (J Cn K) ⋀ ^◡f ∈ (K Cn J))) → (K ∈ Comp → J ∈ Comp))
25	14, 24	impbid 519	. . . . . 6 ⊢ (((J ∈ Top ⋀ K ∈ Top) ⋀ (f:∪J–1-1-onto→∪K ⋀ f ∈ (J Cn K) ⋀ ^◡f ∈ (K Cn J))) → (J ∈ Comp ↔ K ∈ Comp))
26	25	ex 371	. . . . 5 ⊢ ((J ∈ Top ⋀ K ∈ Top) → ((f:∪J–1-1-onto→∪K ⋀ f ∈ (J Cn K) ⋀ ^◡f ∈ (K Cn J)) → (J ∈ Comp ↔ K ∈ Comp)))
27	6, 26	sylbid 201	. . . 4 ⊢ ((J ∈ Top ⋀ K ∈ Top) → (f ∈ (J Homeo K) → (J ∈ Comp ↔ K ∈ Comp)))
28	27	19.23adv 1251	. . 3 ⊢ ((J ∈ Top ⋀ K ∈ Top) → (∃f f ∈ (J Homeo K) → (J ∈ Comp ↔ K ∈ Comp)))
29	1, 28	sylbid 201	. 2 ⊢ ((J ∈ Top ⋀ K ∈ Top) → (J ~= K → (J ∈ Comp ↔ K ∈ Comp)))
30	29	3impia 836	1 ⊢ ((J ∈ Top ⋀ K ∈ Top ⋀ J ~= K) → (J ∈ Comp ↔ K ∈ Comp))

Colors of variables: wff set class

Syntax hints: → wi 3 ↔ wb 144 ⋀ wa 221 ⋀ w3a 781 ∈ wcel 994 ∃wex 1016 Vcvv 1857 ∪cuni 2569 class class class wbr 2692 ^◡ccnv 3250 –onto→wfo 3261 –1-1-onto→wf1o 3262 (class class class)co 4021 Topctop 7800 Cn ccn 7962 Homeo chomeosm 11006 ~= chomeo 11007 Compccomp 11105

This theorem is referenced by: reheibor 12074

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-nul 2784 ax-pow 2818 ax-pr 2855 ax-un 3089

This theorem depends on definitions: df-bi 145 df-or 222 df-an 223 df-3or 782 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-pss 2107 df-nul 2333 df-if 2416 df-pw 2459 df-sn 2470 df-pr 2471 df-tp 2473 df-op 2474 df-uni 2570 df-iun 2635 df-br 2693 df-opab 2741 df-tr 2755 df-eprel 2910 df-id 2913 df-po 2918 df-so 2929 df-fr 2947 df-we 2962 df-ord 2978 df-on 2979 df-lim 2980 df-suc 2981 df-om 3219 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-1o 4269 df-er 4401 df-map 4465 df-en 4509 df-dom 4510 df-fin 4512 df-cn 7964 df-homeo 11008 df-hmph 11016 df-comp 11106