Metamath Proof Explorer

Theorem cvmsf1o

Description: F , localized to an element of an even covering of U , is a bijection. (Contributed by Mario Carneiro, 14-Feb-2015)

Ref Expression
Hypothesis cvmcov.1 ⊢ 𝑆 = ( 𝑘 ∈ 𝐽 ↦ { 𝑠 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ∣ ( ∪ 𝑠 = ( ◡ 𝐹 “ 𝑘 ) ∧ ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝐹 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ) } )
Assertion cvmsf1o ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) ∧ 𝐴 ∈ 𝑇 ) → ( 𝐹 ↾ 𝐴 ) : 𝐴 –1-1-onto→ 𝑈 )

Proof

Step Hyp Ref Expression
1 cvmcov.1 ⊢ 𝑆 = ( 𝑘 ∈ 𝐽 ↦ { 𝑠 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ∣ ( ∪ 𝑠 = ( ◡ 𝐹 “ 𝑘 ) ∧ ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝐹 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ) } )
2 cvmtop1 ⊢ ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) → 𝐶 ∈ Top )
3 2 3ad2ant1 ⊢ ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) ∧ 𝐴 ∈ 𝑇 ) → 𝐶 ∈ Top )
4 eqid ⊢ ∪ 𝐶 = ∪ 𝐶
5 4 toptopon ⊢ ( 𝐶 ∈ Top ↔ 𝐶 ∈ ( TopOn ‘ ∪ 𝐶 ) )
6 3 5 sylib ⊢ ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) ∧ 𝐴 ∈ 𝑇 ) → 𝐶 ∈ ( TopOn ‘ ∪ 𝐶 ) )
7 1 cvmsss ⊢ ( 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) → 𝑇 ⊆ 𝐶 )
8 7 3ad2ant2 ⊢ ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) ∧ 𝐴 ∈ 𝑇 ) → 𝑇 ⊆ 𝐶 )
9 simp3 ⊢ ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) ∧ 𝐴 ∈ 𝑇 ) → 𝐴 ∈ 𝑇 )
10 8 9 sseldd ⊢ ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) ∧ 𝐴 ∈ 𝑇 ) → 𝐴 ∈ 𝐶 )
11 elssuni ⊢ ( 𝐴 ∈ 𝐶 → 𝐴 ⊆ ∪ 𝐶 )
12 10 11 syl ⊢ ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) ∧ 𝐴 ∈ 𝑇 ) → 𝐴 ⊆ ∪ 𝐶 )
13 resttopon ⊢ ( ( 𝐶 ∈ ( TopOn ‘ ∪ 𝐶 ) ∧ 𝐴 ⊆ ∪ 𝐶 ) → ( 𝐶 ↾t 𝐴 ) ∈ ( TopOn ‘ 𝐴 ) )
14 6 12 13 syl2anc ⊢ ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) ∧ 𝐴 ∈ 𝑇 ) → ( 𝐶 ↾t 𝐴 ) ∈ ( TopOn ‘ 𝐴 ) )
15 cvmtop2 ⊢ ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) → 𝐽 ∈ Top )
16 15 3ad2ant1 ⊢ ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) ∧ 𝐴 ∈ 𝑇 ) → 𝐽 ∈ Top )
17 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
18 17 toptopon ⊢ ( 𝐽 ∈ Top ↔ 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) )
19 16 18 sylib ⊢ ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) ∧ 𝐴 ∈ 𝑇 ) → 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) )
20 1 cvmsrcl ⊢ ( 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) → 𝑈 ∈ 𝐽 )
21 20 3ad2ant2 ⊢ ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) ∧ 𝐴 ∈ 𝑇 ) → 𝑈 ∈ 𝐽 )
22 elssuni ⊢ ( 𝑈 ∈ 𝐽 → 𝑈 ⊆ ∪ 𝐽 )
23 21 22 syl ⊢ ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) ∧ 𝐴 ∈ 𝑇 ) → 𝑈 ⊆ ∪ 𝐽 )
24 resttopon ⊢ ( ( 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) ∧ 𝑈 ⊆ ∪ 𝐽 ) → ( 𝐽 ↾t 𝑈 ) ∈ ( TopOn ‘ 𝑈 ) )
25 19 23 24 syl2anc ⊢ ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) ∧ 𝐴 ∈ 𝑇 ) → ( 𝐽 ↾t 𝑈 ) ∈ ( TopOn ‘ 𝑈 ) )
26 1 cvmshmeo ⊢ ( ( 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) ∧ 𝐴 ∈ 𝑇 ) → ( 𝐹 ↾ 𝐴 ) ∈ ( ( 𝐶 ↾t 𝐴 ) Homeo ( 𝐽 ↾t 𝑈 ) ) )
27 26 3adant1 ⊢ ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) ∧ 𝐴 ∈ 𝑇 ) → ( 𝐹 ↾ 𝐴 ) ∈ ( ( 𝐶 ↾t 𝐴 ) Homeo ( 𝐽 ↾t 𝑈 ) ) )
28 hmeof1o2 ⊢ ( ( ( 𝐶 ↾t 𝐴 ) ∈ ( TopOn ‘ 𝐴 ) ∧ ( 𝐽 ↾t 𝑈 ) ∈ ( TopOn ‘ 𝑈 ) ∧ ( 𝐹 ↾ 𝐴 ) ∈ ( ( 𝐶 ↾t 𝐴 ) Homeo ( 𝐽 ↾t 𝑈 ) ) ) → ( 𝐹 ↾ 𝐴 ) : 𝐴 –1-1-onto→ 𝑈 )
29 14 25 27 28 syl3anc ⊢ ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑇 ∈ ( 𝑆 ‘ 𝑈 ) ∧ 𝐴 ∈ 𝑇 ) → ( 𝐹 ↾ 𝐴 ) : 𝐴 –1-1-onto→ 𝑈 )