Theorem cvmcov

Description: Property of a covering map. In order to make the covering property more manageable, we define here the set S ( k ) of all even coverings of an open set k in the range. Then the covering property states that every point has a neighborhood which has an even covering. (Contributed by Mario Carneiro, 13-Feb-2015)

	Ref	Expression
Hypotheses	cvmcov.1	⊢ 𝑆 = ( 𝑘 ∈ 𝐽 ↦ { 𝑠 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ∣ ( ∪ 𝑠 = ( ◡ 𝐹 “ 𝑘 ) ∧ ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝐹 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ) } )
	cvmcov.2	⊢ 𝑋 = ∪ 𝐽
Assertion	cvmcov	⊢ ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑃 ∈ 𝑋 ) → ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝑆 ‘ 𝑥 ) ≠ ∅ ) )

Proof

Step	Hyp	Ref	Expression
1		cvmcov.1	⊢ 𝑆 = ( 𝑘 ∈ 𝐽 ↦ { 𝑠 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ∣ ( ∪ 𝑠 = ( ◡ 𝐹 “ 𝑘 ) ∧ ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝐹 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ) } )
2		cvmcov.2	⊢ 𝑋 = ∪ 𝐽
3	1 2	iscvm	⊢ ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ↔ ( ( 𝐶 ∈ Top ∧ 𝐽 ∈ Top ∧ 𝐹 ∈ ( 𝐶 Cn 𝐽 ) ) ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑘 ∈ 𝐽 ( 𝑥 ∈ 𝑘 ∧ ( 𝑆 ‘ 𝑘 ) ≠ ∅ ) ) )
4	3	simprbi	⊢ ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) → ∀ 𝑥 ∈ 𝑋 ∃ 𝑘 ∈ 𝐽 ( 𝑥 ∈ 𝑘 ∧ ( 𝑆 ‘ 𝑘 ) ≠ ∅ ) )
5		eleq1	⊢ ( 𝑥 = 𝑃 → ( 𝑥 ∈ 𝑘 ↔ 𝑃 ∈ 𝑘 ) )
6	5	anbi1d	⊢ ( 𝑥 = 𝑃 → ( ( 𝑥 ∈ 𝑘 ∧ ( 𝑆 ‘ 𝑘 ) ≠ ∅ ) ↔ ( 𝑃 ∈ 𝑘 ∧ ( 𝑆 ‘ 𝑘 ) ≠ ∅ ) ) )
7	6	rexbidv	⊢ ( 𝑥 = 𝑃 → ( ∃ 𝑘 ∈ 𝐽 ( 𝑥 ∈ 𝑘 ∧ ( 𝑆 ‘ 𝑘 ) ≠ ∅ ) ↔ ∃ 𝑘 ∈ 𝐽 ( 𝑃 ∈ 𝑘 ∧ ( 𝑆 ‘ 𝑘 ) ≠ ∅ ) ) )
8	7	rspcv	⊢ ( 𝑃 ∈ 𝑋 → ( ∀ 𝑥 ∈ 𝑋 ∃ 𝑘 ∈ 𝐽 ( 𝑥 ∈ 𝑘 ∧ ( 𝑆 ‘ 𝑘 ) ≠ ∅ ) → ∃ 𝑘 ∈ 𝐽 ( 𝑃 ∈ 𝑘 ∧ ( 𝑆 ‘ 𝑘 ) ≠ ∅ ) ) )
9	4 8	mpan9	⊢ ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑃 ∈ 𝑋 ) → ∃ 𝑘 ∈ 𝐽 ( 𝑃 ∈ 𝑘 ∧ ( 𝑆 ‘ 𝑘 ) ≠ ∅ ) )
10		nfv	⊢ Ⅎ 𝑘 𝑃 ∈ 𝑥
11		nfmpt1	⊢ Ⅎ 𝑘 ( 𝑘 ∈ 𝐽 ↦ { 𝑠 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ∣ ( ∪ 𝑠 = ( ◡ 𝐹 “ 𝑘 ) ∧ ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝐹 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ) } )
12	1 11	nfcxfr	⊢ Ⅎ 𝑘 𝑆
13		nfcv	⊢ Ⅎ 𝑘 𝑥
14	12 13	nffv	⊢ Ⅎ 𝑘 ( 𝑆 ‘ 𝑥 )
15		nfcv	⊢ Ⅎ 𝑘 ∅
16	14 15	nfne	⊢ Ⅎ 𝑘 ( 𝑆 ‘ 𝑥 ) ≠ ∅
17	10 16	nfan	⊢ Ⅎ 𝑘 ( 𝑃 ∈ 𝑥 ∧ ( 𝑆 ‘ 𝑥 ) ≠ ∅ )
18		nfv	⊢ Ⅎ 𝑥 ( 𝑃 ∈ 𝑘 ∧ ( 𝑆 ‘ 𝑘 ) ≠ ∅ )
19		eleq2w	⊢ ( 𝑥 = 𝑘 → ( 𝑃 ∈ 𝑥 ↔ 𝑃 ∈ 𝑘 ) )
20		fveq2	⊢ ( 𝑥 = 𝑘 → ( 𝑆 ‘ 𝑥 ) = ( 𝑆 ‘ 𝑘 ) )
21	20	neeq1d	⊢ ( 𝑥 = 𝑘 → ( ( 𝑆 ‘ 𝑥 ) ≠ ∅ ↔ ( 𝑆 ‘ 𝑘 ) ≠ ∅ ) )
22	19 21	anbi12d	⊢ ( 𝑥 = 𝑘 → ( ( 𝑃 ∈ 𝑥 ∧ ( 𝑆 ‘ 𝑥 ) ≠ ∅ ) ↔ ( 𝑃 ∈ 𝑘 ∧ ( 𝑆 ‘ 𝑘 ) ≠ ∅ ) ) )
23	17 18 22	cbvrexw	⊢ ( ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝑆 ‘ 𝑥 ) ≠ ∅ ) ↔ ∃ 𝑘 ∈ 𝐽 ( 𝑃 ∈ 𝑘 ∧ ( 𝑆 ‘ 𝑘 ) ≠ ∅ ) )
24	9 23	sylibr	⊢ ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑃 ∈ 𝑋 ) → ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝑆 ‘ 𝑥 ) ≠ ∅ ) )