Theorem compcov 11479

Description: An open cover of a compact topology has a finite subcover.

Hypothesis

Ref	Expression
compcov.1	⊢ X = ∪J

Assertion

Ref	Expression
compcov	⊢ ((J ∈ Comp ⋀ S ⊆ J ⋀ X = ∪S) → ∃s ∈ (℘S ∩ Fin)X = ∪s)

Distinct variable groups:   J,s   S,s

Proof of Theorem compcov

Step	Hyp	Ref	Expression
1		unieq 2576	. . . . . . 7 ⊢ (r = S → ∪r = ∪S)
2	1	eqeq2d 1529	. . . . . 6 ⊢ (r = S → (∪J = ∪r ↔ ∪J = ∪S))
3		pweq 2460	. . . . . . . 8 ⊢ (r = S → ℘r = ℘S)
4	3	ineq1d 2268	. . . . . . 7 ⊢ (r = S → (℘r ∩ Fin) = (℘S ∩ Fin))
5	4	rexeq1d 1836	. . . . . 6 ⊢ (r = S → (∃s ∈ (℘r ∩ Fin)∪J = ∪s ↔ ∃s ∈ (℘S ∩ Fin)∪J = ∪s))
6	2, 5	imbi12d 629	. . . . 5 ⊢ (r = S → ((∪J = ∪r → ∃s ∈ (℘r ∩ Fin)∪J = ∪s) ↔ (∪J = ∪S → ∃s ∈ (℘S ∩ Fin)∪J = ∪s)))
7	6	rcla4v 1919	. . . 4 ⊢ (S ∈ ℘J → (∀r ∈ ℘ J(∪J = ∪r → ∃s ∈ (℘r ∩ Fin)∪J = ∪s) → (∪J = ∪S → ∃s ∈ (℘S ∩ Fin)∪J = ∪s)))
8		pm3.27 321	. . . . 5 ⊢ ((J ∈ Comp ⋀ S ⊆ J) → S ⊆ J)
9		ssexg 2795	. . . . . . 7 ⊢ ((S ⊆ J ⋀ J ∈ Comp) → S ∈ V)
10	9	ancoms 438	. . . . . 6 ⊢ ((J ∈ Comp ⋀ S ⊆ J) → S ∈ V)
11		elpwg 2462	. . . . . 6 ⊢ (S ∈ V → (S ∈ ℘J ↔ S ⊆ J))
12	10, 11	syl 10	. . . . 5 ⊢ ((J ∈ Comp ⋀ S ⊆ J) → (S ∈ ℘J ↔ S ⊆ J))
13	8, 12	mpbird 194	. . . 4 ⊢ ((J ∈ Comp ⋀ S ⊆ J) → S ∈ ℘J)
14		iscomp 11107	. . . . . 6 ⊢ (J ∈ Comp ↔ (J ∈ Top ⋀ ∀r ∈ ℘ J(∪J = ∪r → ∃s ∈ (℘r ∩ Fin)∪J = ∪s)))
15	14	pm3.27bi 324	. . . . 5 ⊢ (J ∈ Comp → ∀r ∈ ℘ J(∪J = ∪r → ∃s ∈ (℘r ∩ Fin)∪J = ∪s))
16	15	adantr 389	. . . 4 ⊢ ((J ∈ Comp ⋀ S ⊆ J) → ∀r ∈ ℘ J(∪J = ∪r → ∃s ∈ (℘r ∩ Fin)∪J = ∪s))
17	7, 13, 16	sylc 68	. . 3 ⊢ ((J ∈ Comp ⋀ S ⊆ J) → (∪J = ∪S → ∃s ∈ (℘S ∩ Fin)∪J = ∪s))
18		compcov.1	. . . 4 ⊢ X = ∪J
19	18	eqeq1i 1525	. . 3 ⊢ (X = ∪S ↔ ∪J = ∪S)
20	18	eqeq1i 1525	. . . 4 ⊢ (X = ∪s ↔ ∪J = ∪s)
21	20	rexbii 1714	. . 3 ⊢ (∃s ∈ (℘S ∩ Fin)X = ∪s ↔ ∃s ∈ (℘S ∩ Fin)∪J = ∪s)
22	17, 19, 21	3imtr4g 556	. 2 ⊢ ((J ∈ Comp ⋀ S ⊆ J) → (X = ∪S → ∃s ∈ (℘S ∩ Fin)X = ∪s))
23	22	3impia 836	1 ⊢ ((J ∈ Comp ⋀ S ⊆ J ⋀ X = ∪S) → ∃s ∈ (℘S ∩ Fin)X = ∪s)

Syntax hints:   → wi 3   ↔ wb 144   ⋀ wa 221   ⋀ w3a 781   = wceq 992   ∈ wcel 994  ∀wral 1691  ∃wrex 1692  Vcvv 1857   ∩ cin 2098   ⊆ wss 2099  ℘cpw 2458  ∪cuni 2569  Fincfn 4508  Topctop 7800  Compccomp 11105

This theorem is referenced by:  cptclsscpt 11482  alexsublem1 11489  locfincomp 11568  comppfsc 11571

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-10 1002  ax-12 1004  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-sep 2777

This theorem depends on definitions:  df-bi 145  df-an 223  df-3an 783  df-ex 1017  df-sb 1209  df-clab 1506  df-cleq 1511  df-clel 1514  df-ral 1695  df-rex 1696  df-rab 1698  df-v 1858  df-in 2103  df-ss 2105  df-pw 2459  df-uni 2570  df-comp 11106

Copyright terms: Public domain