Theorem cvmcov2

Description: The covering map property can be restricted to an open subset. (Contributed by Mario Carneiro, 7-Jul-2015)

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

Proof

Step	Hyp	Ref	Expression
1		cvmcov.1	⊢ 𝑆 = ( 𝑘 ∈ 𝐽 ↦ { 𝑠 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ∣ ( ∪ 𝑠 = ( ◡ 𝐹 “ 𝑘 ) ∧ ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝐹 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ) } )
2		simp1	⊢ ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑈 ∈ 𝐽 ∧ 𝑃 ∈ 𝑈 ) → 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) )
3		simp3	⊢ ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑈 ∈ 𝐽 ∧ 𝑃 ∈ 𝑈 ) → 𝑃 ∈ 𝑈 )
4		simp2	⊢ ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑈 ∈ 𝐽 ∧ 𝑃 ∈ 𝑈 ) → 𝑈 ∈ 𝐽 )
5		elunii	⊢ ( ( 𝑃 ∈ 𝑈 ∧ 𝑈 ∈ 𝐽 ) → 𝑃 ∈ ∪ 𝐽 )
6	3 4 5	syl2anc	⊢ ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑈 ∈ 𝐽 ∧ 𝑃 ∈ 𝑈 ) → 𝑃 ∈ ∪ 𝐽 )
7		eqid	⊢ ∪ 𝐽 = ∪ 𝐽
8	1 7	cvmcov	⊢ ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑃 ∈ ∪ 𝐽 ) → ∃ 𝑦 ∈ 𝐽 ( 𝑃 ∈ 𝑦 ∧ ( 𝑆 ‘ 𝑦 ) ≠ ∅ ) )
9	2 6 8	syl2anc	⊢ ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑈 ∈ 𝐽 ∧ 𝑃 ∈ 𝑈 ) → ∃ 𝑦 ∈ 𝐽 ( 𝑃 ∈ 𝑦 ∧ ( 𝑆 ‘ 𝑦 ) ≠ ∅ ) )
10		inss2	⊢ ( 𝑦 ∩ 𝑈 ) ⊆ 𝑈
11		vex	⊢ 𝑦 ∈ V
12	11	inex1	⊢ ( 𝑦 ∩ 𝑈 ) ∈ V
13	12	elpw	⊢ ( ( 𝑦 ∩ 𝑈 ) ∈ 𝒫 𝑈 ↔ ( 𝑦 ∩ 𝑈 ) ⊆ 𝑈 )
14	10 13	mpbir	⊢ ( 𝑦 ∩ 𝑈 ) ∈ 𝒫 𝑈
15	14	a1i	⊢ ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑈 ∈ 𝐽 ∧ 𝑃 ∈ 𝑈 ) ∧ ( 𝑦 ∈ 𝐽 ∧ ( 𝑃 ∈ 𝑦 ∧ ( 𝑆 ‘ 𝑦 ) ≠ ∅ ) ) ) → ( 𝑦 ∩ 𝑈 ) ∈ 𝒫 𝑈 )
16		simprrl	⊢ ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑈 ∈ 𝐽 ∧ 𝑃 ∈ 𝑈 ) ∧ ( 𝑦 ∈ 𝐽 ∧ ( 𝑃 ∈ 𝑦 ∧ ( 𝑆 ‘ 𝑦 ) ≠ ∅ ) ) ) → 𝑃 ∈ 𝑦 )
17	3	adantr	⊢ ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑈 ∈ 𝐽 ∧ 𝑃 ∈ 𝑈 ) ∧ ( 𝑦 ∈ 𝐽 ∧ ( 𝑃 ∈ 𝑦 ∧ ( 𝑆 ‘ 𝑦 ) ≠ ∅ ) ) ) → 𝑃 ∈ 𝑈 )
18	16 17	elind	⊢ ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑈 ∈ 𝐽 ∧ 𝑃 ∈ 𝑈 ) ∧ ( 𝑦 ∈ 𝐽 ∧ ( 𝑃 ∈ 𝑦 ∧ ( 𝑆 ‘ 𝑦 ) ≠ ∅ ) ) ) → 𝑃 ∈ ( 𝑦 ∩ 𝑈 ) )
19		simprrr	⊢ ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑈 ∈ 𝐽 ∧ 𝑃 ∈ 𝑈 ) ∧ ( 𝑦 ∈ 𝐽 ∧ ( 𝑃 ∈ 𝑦 ∧ ( 𝑆 ‘ 𝑦 ) ≠ ∅ ) ) ) → ( 𝑆 ‘ 𝑦 ) ≠ ∅ )
20	2	adantr	⊢ ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑈 ∈ 𝐽 ∧ 𝑃 ∈ 𝑈 ) ∧ ( 𝑦 ∈ 𝐽 ∧ ( 𝑃 ∈ 𝑦 ∧ ( 𝑆 ‘ 𝑦 ) ≠ ∅ ) ) ) → 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) )
21		cvmtop2	⊢ ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) → 𝐽 ∈ Top )
22	20 21	syl	⊢ ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑈 ∈ 𝐽 ∧ 𝑃 ∈ 𝑈 ) ∧ ( 𝑦 ∈ 𝐽 ∧ ( 𝑃 ∈ 𝑦 ∧ ( 𝑆 ‘ 𝑦 ) ≠ ∅ ) ) ) → 𝐽 ∈ Top )
23		simprl	⊢ ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑈 ∈ 𝐽 ∧ 𝑃 ∈ 𝑈 ) ∧ ( 𝑦 ∈ 𝐽 ∧ ( 𝑃 ∈ 𝑦 ∧ ( 𝑆 ‘ 𝑦 ) ≠ ∅ ) ) ) → 𝑦 ∈ 𝐽 )
24	4	adantr	⊢ ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑈 ∈ 𝐽 ∧ 𝑃 ∈ 𝑈 ) ∧ ( 𝑦 ∈ 𝐽 ∧ ( 𝑃 ∈ 𝑦 ∧ ( 𝑆 ‘ 𝑦 ) ≠ ∅ ) ) ) → 𝑈 ∈ 𝐽 )
25		inopn	⊢ ( ( 𝐽 ∈ Top ∧ 𝑦 ∈ 𝐽 ∧ 𝑈 ∈ 𝐽 ) → ( 𝑦 ∩ 𝑈 ) ∈ 𝐽 )
26	22 23 24 25	syl3anc	⊢ ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑈 ∈ 𝐽 ∧ 𝑃 ∈ 𝑈 ) ∧ ( 𝑦 ∈ 𝐽 ∧ ( 𝑃 ∈ 𝑦 ∧ ( 𝑆 ‘ 𝑦 ) ≠ ∅ ) ) ) → ( 𝑦 ∩ 𝑈 ) ∈ 𝐽 )
27		inss1	⊢ ( 𝑦 ∩ 𝑈 ) ⊆ 𝑦
28	27	a1i	⊢ ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑈 ∈ 𝐽 ∧ 𝑃 ∈ 𝑈 ) ∧ ( 𝑦 ∈ 𝐽 ∧ ( 𝑃 ∈ 𝑦 ∧ ( 𝑆 ‘ 𝑦 ) ≠ ∅ ) ) ) → ( 𝑦 ∩ 𝑈 ) ⊆ 𝑦 )
29	1	cvmsss2	⊢ ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ ( 𝑦 ∩ 𝑈 ) ∈ 𝐽 ∧ ( 𝑦 ∩ 𝑈 ) ⊆ 𝑦 ) → ( ( 𝑆 ‘ 𝑦 ) ≠ ∅ → ( 𝑆 ‘ ( 𝑦 ∩ 𝑈 ) ) ≠ ∅ ) )
30	20 26 28 29	syl3anc	⊢ ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑈 ∈ 𝐽 ∧ 𝑃 ∈ 𝑈 ) ∧ ( 𝑦 ∈ 𝐽 ∧ ( 𝑃 ∈ 𝑦 ∧ ( 𝑆 ‘ 𝑦 ) ≠ ∅ ) ) ) → ( ( 𝑆 ‘ 𝑦 ) ≠ ∅ → ( 𝑆 ‘ ( 𝑦 ∩ 𝑈 ) ) ≠ ∅ ) )
31	19 30	mpd	⊢ ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑈 ∈ 𝐽 ∧ 𝑃 ∈ 𝑈 ) ∧ ( 𝑦 ∈ 𝐽 ∧ ( 𝑃 ∈ 𝑦 ∧ ( 𝑆 ‘ 𝑦 ) ≠ ∅ ) ) ) → ( 𝑆 ‘ ( 𝑦 ∩ 𝑈 ) ) ≠ ∅ )
32		eleq2	⊢ ( 𝑥 = ( 𝑦 ∩ 𝑈 ) → ( 𝑃 ∈ 𝑥 ↔ 𝑃 ∈ ( 𝑦 ∩ 𝑈 ) ) )
33		fveq2	⊢ ( 𝑥 = ( 𝑦 ∩ 𝑈 ) → ( 𝑆 ‘ 𝑥 ) = ( 𝑆 ‘ ( 𝑦 ∩ 𝑈 ) ) )
34	33	neeq1d	⊢ ( 𝑥 = ( 𝑦 ∩ 𝑈 ) → ( ( 𝑆 ‘ 𝑥 ) ≠ ∅ ↔ ( 𝑆 ‘ ( 𝑦 ∩ 𝑈 ) ) ≠ ∅ ) )
35	32 34	anbi12d	⊢ ( 𝑥 = ( 𝑦 ∩ 𝑈 ) → ( ( 𝑃 ∈ 𝑥 ∧ ( 𝑆 ‘ 𝑥 ) ≠ ∅ ) ↔ ( 𝑃 ∈ ( 𝑦 ∩ 𝑈 ) ∧ ( 𝑆 ‘ ( 𝑦 ∩ 𝑈 ) ) ≠ ∅ ) ) )
36	35	rspcev	⊢ ( ( ( 𝑦 ∩ 𝑈 ) ∈ 𝒫 𝑈 ∧ ( 𝑃 ∈ ( 𝑦 ∩ 𝑈 ) ∧ ( 𝑆 ‘ ( 𝑦 ∩ 𝑈 ) ) ≠ ∅ ) ) → ∃ 𝑥 ∈ 𝒫 𝑈 ( 𝑃 ∈ 𝑥 ∧ ( 𝑆 ‘ 𝑥 ) ≠ ∅ ) )
37	15 18 31 36	syl12anc	⊢ ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑈 ∈ 𝐽 ∧ 𝑃 ∈ 𝑈 ) ∧ ( 𝑦 ∈ 𝐽 ∧ ( 𝑃 ∈ 𝑦 ∧ ( 𝑆 ‘ 𝑦 ) ≠ ∅ ) ) ) → ∃ 𝑥 ∈ 𝒫 𝑈 ( 𝑃 ∈ 𝑥 ∧ ( 𝑆 ‘ 𝑥 ) ≠ ∅ ) )
38	9 37	rexlimddv	⊢ ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑈 ∈ 𝐽 ∧ 𝑃 ∈ 𝑈 ) → ∃ 𝑥 ∈ 𝒫 𝑈 ( 𝑃 ∈ 𝑥 ∧ ( 𝑆 ‘ 𝑥 ) ≠ ∅ ) )