Metamath Proof Explorer

Theorem cvmfolem

Description: Lemma for cvmfo . (Contributed by Mario Carneiro, 13-Feb-2015)

Ref Expression
Hypotheses cvmcov.1 ⊢ 𝑆 = ( 𝑘 ∈ 𝐽 ↦ { 𝑠 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ∣ ( ∪ 𝑠 = ( ◡ 𝐹 “ 𝑘 ) ∧ ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝐹 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ) } )
cvmseu.1 ⊢ 𝐵 = ∪ 𝐶
cvmfolem.2 ⊢ 𝑋 = ∪ 𝐽
Assertion cvmfolem ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) → 𝐹 : 𝐵 –onto→ 𝑋 )

Proof

Step Hyp Ref Expression
1 cvmcov.1 ⊢ 𝑆 = ( 𝑘 ∈ 𝐽 ↦ { 𝑠 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ∣ ( ∪ 𝑠 = ( ◡ 𝐹 “ 𝑘 ) ∧ ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝐹 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ) } )
2 cvmseu.1 ⊢ 𝐵 = ∪ 𝐶
3 cvmfolem.2 ⊢ 𝑋 = ∪ 𝐽
4 cvmcn ⊢ ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) → 𝐹 ∈ ( 𝐶 Cn 𝐽 ) )
5 2 3 cnf ⊢ ( 𝐹 ∈ ( 𝐶 Cn 𝐽 ) → 𝐹 : 𝐵 ⟶ 𝑋 )
6 4 5 syl ⊢ ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) → 𝐹 : 𝐵 ⟶ 𝑋 )
7 1 3 cvmcov ⊢ ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑥 ∈ 𝑋 ) → ∃ 𝑧 ∈ 𝐽 ( 𝑥 ∈ 𝑧 ∧ ( 𝑆 ‘ 𝑧 ) ≠ ∅ ) )
8 7 ex ⊢ ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) → ( 𝑥 ∈ 𝑋 → ∃ 𝑧 ∈ 𝐽 ( 𝑥 ∈ 𝑧 ∧ ( 𝑆 ‘ 𝑧 ) ≠ ∅ ) ) )
9 n0 ⊢ ( ( 𝑆 ‘ 𝑧 ) ≠ ∅ ↔ ∃ 𝑤 𝑤 ∈ ( 𝑆 ‘ 𝑧 ) )
10 1 cvmsn0 ⊢ ( 𝑤 ∈ ( 𝑆 ‘ 𝑧 ) → 𝑤 ≠ ∅ )
11 10 ad2antll ⊢ ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑧 ∈ 𝐽 ) ∧ ( 𝑥 ∈ 𝑧 ∧ 𝑤 ∈ ( 𝑆 ‘ 𝑧 ) ) ) → 𝑤 ≠ ∅ )
12 n0 ⊢ ( 𝑤 ≠ ∅ ↔ ∃ 𝑡 𝑡 ∈ 𝑤 )
13 11 12 sylib ⊢ ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑧 ∈ 𝐽 ) ∧ ( 𝑥 ∈ 𝑧 ∧ 𝑤 ∈ ( 𝑆 ‘ 𝑧 ) ) ) → ∃ 𝑡 𝑡 ∈ 𝑤 )
14 simprlr ⊢ ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑧 ∈ 𝐽 ) ∧ ( ( 𝑥 ∈ 𝑧 ∧ 𝑤 ∈ ( 𝑆 ‘ 𝑧 ) ) ∧ 𝑡 ∈ 𝑤 ) ) → 𝑤 ∈ ( 𝑆 ‘ 𝑧 ) )
15 1 cvmsss ⊢ ( 𝑤 ∈ ( 𝑆 ‘ 𝑧 ) → 𝑤 ⊆ 𝐶 )
16 14 15 syl ⊢ ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑧 ∈ 𝐽 ) ∧ ( ( 𝑥 ∈ 𝑧 ∧ 𝑤 ∈ ( 𝑆 ‘ 𝑧 ) ) ∧ 𝑡 ∈ 𝑤 ) ) → 𝑤 ⊆ 𝐶 )
17 simprr ⊢ ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑧 ∈ 𝐽 ) ∧ ( ( 𝑥 ∈ 𝑧 ∧ 𝑤 ∈ ( 𝑆 ‘ 𝑧 ) ) ∧ 𝑡 ∈ 𝑤 ) ) → 𝑡 ∈ 𝑤 )
18 16 17 sseldd ⊢ ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑧 ∈ 𝐽 ) ∧ ( ( 𝑥 ∈ 𝑧 ∧ 𝑤 ∈ ( 𝑆 ‘ 𝑧 ) ) ∧ 𝑡 ∈ 𝑤 ) ) → 𝑡 ∈ 𝐶 )
19 elssuni ⊢ ( 𝑡 ∈ 𝐶 → 𝑡 ⊆ ∪ 𝐶 )
20 18 19 syl ⊢ ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑧 ∈ 𝐽 ) ∧ ( ( 𝑥 ∈ 𝑧 ∧ 𝑤 ∈ ( 𝑆 ‘ 𝑧 ) ) ∧ 𝑡 ∈ 𝑤 ) ) → 𝑡 ⊆ ∪ 𝐶 )
21 20 2 sseqtrrdi ⊢ ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑧 ∈ 𝐽 ) ∧ ( ( 𝑥 ∈ 𝑧 ∧ 𝑤 ∈ ( 𝑆 ‘ 𝑧 ) ) ∧ 𝑡 ∈ 𝑤 ) ) → 𝑡 ⊆ 𝐵 )
22 simpll ⊢ ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑧 ∈ 𝐽 ) ∧ ( ( 𝑥 ∈ 𝑧 ∧ 𝑤 ∈ ( 𝑆 ‘ 𝑧 ) ) ∧ 𝑡 ∈ 𝑤 ) ) → 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) )
23 1 cvmsf1o ⊢ ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑤 ∈ ( 𝑆 ‘ 𝑧 ) ∧ 𝑡 ∈ 𝑤 ) → ( 𝐹 ↾ 𝑡 ) : 𝑡 –1-1-onto→ 𝑧 )
24 22 14 17 23 syl3anc ⊢ ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑧 ∈ 𝐽 ) ∧ ( ( 𝑥 ∈ 𝑧 ∧ 𝑤 ∈ ( 𝑆 ‘ 𝑧 ) ) ∧ 𝑡 ∈ 𝑤 ) ) → ( 𝐹 ↾ 𝑡 ) : 𝑡 –1-1-onto→ 𝑧 )
25 f1ocnv ⊢ ( ( 𝐹 ↾ 𝑡 ) : 𝑡 –1-1-onto→ 𝑧 → ◡ ( 𝐹 ↾ 𝑡 ) : 𝑧 –1-1-onto→ 𝑡 )
26 f1of ⊢ ( ◡ ( 𝐹 ↾ 𝑡 ) : 𝑧 –1-1-onto→ 𝑡 → ◡ ( 𝐹 ↾ 𝑡 ) : 𝑧 ⟶ 𝑡 )
27 24 25 26 3syl ⊢ ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑧 ∈ 𝐽 ) ∧ ( ( 𝑥 ∈ 𝑧 ∧ 𝑤 ∈ ( 𝑆 ‘ 𝑧 ) ) ∧ 𝑡 ∈ 𝑤 ) ) → ◡ ( 𝐹 ↾ 𝑡 ) : 𝑧 ⟶ 𝑡 )
28 simprll ⊢ ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑧 ∈ 𝐽 ) ∧ ( ( 𝑥 ∈ 𝑧 ∧ 𝑤 ∈ ( 𝑆 ‘ 𝑧 ) ) ∧ 𝑡 ∈ 𝑤 ) ) → 𝑥 ∈ 𝑧 )
29 27 28 ffvelrnd ⊢ ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑧 ∈ 𝐽 ) ∧ ( ( 𝑥 ∈ 𝑧 ∧ 𝑤 ∈ ( 𝑆 ‘ 𝑧 ) ) ∧ 𝑡 ∈ 𝑤 ) ) → ( ◡ ( 𝐹 ↾ 𝑡 ) ‘ 𝑥 ) ∈ 𝑡 )
30 21 29 sseldd ⊢ ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑧 ∈ 𝐽 ) ∧ ( ( 𝑥 ∈ 𝑧 ∧ 𝑤 ∈ ( 𝑆 ‘ 𝑧 ) ) ∧ 𝑡 ∈ 𝑤 ) ) → ( ◡ ( 𝐹 ↾ 𝑡 ) ‘ 𝑥 ) ∈ 𝐵 )
31 f1ocnvfv2 ⊢ ( ( ( 𝐹 ↾ 𝑡 ) : 𝑡 –1-1-onto→ 𝑧 ∧ 𝑥 ∈ 𝑧 ) → ( ( 𝐹 ↾ 𝑡 ) ‘ ( ◡ ( 𝐹 ↾ 𝑡 ) ‘ 𝑥 ) ) = 𝑥 )
32 24 28 31 syl2anc ⊢ ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑧 ∈ 𝐽 ) ∧ ( ( 𝑥 ∈ 𝑧 ∧ 𝑤 ∈ ( 𝑆 ‘ 𝑧 ) ) ∧ 𝑡 ∈ 𝑤 ) ) → ( ( 𝐹 ↾ 𝑡 ) ‘ ( ◡ ( 𝐹 ↾ 𝑡 ) ‘ 𝑥 ) ) = 𝑥 )
33 fvres ⊢ ( ( ◡ ( 𝐹 ↾ 𝑡 ) ‘ 𝑥 ) ∈ 𝑡 → ( ( 𝐹 ↾ 𝑡 ) ‘ ( ◡ ( 𝐹 ↾ 𝑡 ) ‘ 𝑥 ) ) = ( 𝐹 ‘ ( ◡ ( 𝐹 ↾ 𝑡 ) ‘ 𝑥 ) ) )
34 29 33 syl ⊢ ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑧 ∈ 𝐽 ) ∧ ( ( 𝑥 ∈ 𝑧 ∧ 𝑤 ∈ ( 𝑆 ‘ 𝑧 ) ) ∧ 𝑡 ∈ 𝑤 ) ) → ( ( 𝐹 ↾ 𝑡 ) ‘ ( ◡ ( 𝐹 ↾ 𝑡 ) ‘ 𝑥 ) ) = ( 𝐹 ‘ ( ◡ ( 𝐹 ↾ 𝑡 ) ‘ 𝑥 ) ) )
35 32 34 eqtr3d ⊢ ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑧 ∈ 𝐽 ) ∧ ( ( 𝑥 ∈ 𝑧 ∧ 𝑤 ∈ ( 𝑆 ‘ 𝑧 ) ) ∧ 𝑡 ∈ 𝑤 ) ) → 𝑥 = ( 𝐹 ‘ ( ◡ ( 𝐹 ↾ 𝑡 ) ‘ 𝑥 ) ) )
36 fveq2 ⊢ ( 𝑦 = ( ◡ ( 𝐹 ↾ 𝑡 ) ‘ 𝑥 ) → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ ( ◡ ( 𝐹 ↾ 𝑡 ) ‘ 𝑥 ) ) )
37 36 rspceeqv ⊢ ( ( ( ◡ ( 𝐹 ↾ 𝑡 ) ‘ 𝑥 ) ∈ 𝐵 ∧ 𝑥 = ( 𝐹 ‘ ( ◡ ( 𝐹 ↾ 𝑡 ) ‘ 𝑥 ) ) ) → ∃ 𝑦 ∈ 𝐵 𝑥 = ( 𝐹 ‘ 𝑦 ) )
38 30 35 37 syl2anc ⊢ ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑧 ∈ 𝐽 ) ∧ ( ( 𝑥 ∈ 𝑧 ∧ 𝑤 ∈ ( 𝑆 ‘ 𝑧 ) ) ∧ 𝑡 ∈ 𝑤 ) ) → ∃ 𝑦 ∈ 𝐵 𝑥 = ( 𝐹 ‘ 𝑦 ) )
39 38 expr ⊢ ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑧 ∈ 𝐽 ) ∧ ( 𝑥 ∈ 𝑧 ∧ 𝑤 ∈ ( 𝑆 ‘ 𝑧 ) ) ) → ( 𝑡 ∈ 𝑤 → ∃ 𝑦 ∈ 𝐵 𝑥 = ( 𝐹 ‘ 𝑦 ) ) )
40 39 exlimdv ⊢ ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑧 ∈ 𝐽 ) ∧ ( 𝑥 ∈ 𝑧 ∧ 𝑤 ∈ ( 𝑆 ‘ 𝑧 ) ) ) → ( ∃ 𝑡 𝑡 ∈ 𝑤 → ∃ 𝑦 ∈ 𝐵 𝑥 = ( 𝐹 ‘ 𝑦 ) ) )
41 13 40 mpd ⊢ ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑧 ∈ 𝐽 ) ∧ ( 𝑥 ∈ 𝑧 ∧ 𝑤 ∈ ( 𝑆 ‘ 𝑧 ) ) ) → ∃ 𝑦 ∈ 𝐵 𝑥 = ( 𝐹 ‘ 𝑦 ) )
42 41 expr ⊢ ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑧 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝑧 ) → ( 𝑤 ∈ ( 𝑆 ‘ 𝑧 ) → ∃ 𝑦 ∈ 𝐵 𝑥 = ( 𝐹 ‘ 𝑦 ) ) )
43 42 exlimdv ⊢ ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑧 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝑧 ) → ( ∃ 𝑤 𝑤 ∈ ( 𝑆 ‘ 𝑧 ) → ∃ 𝑦 ∈ 𝐵 𝑥 = ( 𝐹 ‘ 𝑦 ) ) )
44 9 43 syl5bi ⊢ ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑧 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝑧 ) → ( ( 𝑆 ‘ 𝑧 ) ≠ ∅ → ∃ 𝑦 ∈ 𝐵 𝑥 = ( 𝐹 ‘ 𝑦 ) ) )
45 44 expimpd ⊢ ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑧 ∈ 𝐽 ) → ( ( 𝑥 ∈ 𝑧 ∧ ( 𝑆 ‘ 𝑧 ) ≠ ∅ ) → ∃ 𝑦 ∈ 𝐵 𝑥 = ( 𝐹 ‘ 𝑦 ) ) )
46 45 rexlimdva ⊢ ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) → ( ∃ 𝑧 ∈ 𝐽 ( 𝑥 ∈ 𝑧 ∧ ( 𝑆 ‘ 𝑧 ) ≠ ∅ ) → ∃ 𝑦 ∈ 𝐵 𝑥 = ( 𝐹 ‘ 𝑦 ) ) )
47 8 46 syld ⊢ ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) → ( 𝑥 ∈ 𝑋 → ∃ 𝑦 ∈ 𝐵 𝑥 = ( 𝐹 ‘ 𝑦 ) ) )
48 47 ralrimiv ⊢ ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) → ∀ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝐵 𝑥 = ( 𝐹 ‘ 𝑦 ) )
49 dffo3 ⊢ ( 𝐹 : 𝐵 –onto→ 𝑋 ↔ ( 𝐹 : 𝐵 ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝐵 𝑥 = ( 𝐹 ‘ 𝑦 ) ) )
50 6 48 49 sylanbrc ⊢ ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) → 𝐹 : 𝐵 –onto→ 𝑋 )