Metamath Proof Explorer

Theorem cvmliftlem15

Description: Lemma for cvmlift . Discharge the assumptions of cvmliftlem14 . The set of all open subsets u of the unit interval such that G " u is contained in an even covering of some open set in J is a cover of II by the definition of a covering map, so by the Lebesgue number lemma lebnumii , there is a subdivision of the closed unit interval into N equal parts such that each part is entirely contained within one such open set of J . Then using finite choice ac6sfi to uniformly select one such subset and one even covering of each subset, we are ready to finish the proof with cvmliftlem14 . (Contributed by Mario Carneiro, 14-Feb-2015)

Ref Expression
Hypotheses cvmliftlem.1 ⊢ 𝑆 = ( 𝑘 ∈ 𝐽 ↦ { 𝑠 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ∣ ( ∪ 𝑠 = ( ◡ 𝐹 “ 𝑘 ) ∧ ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝐹 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ) } )
cvmliftlem.b ⊢ 𝐵 = ∪ 𝐶
cvmliftlem.x ⊢ 𝑋 = ∪ 𝐽
cvmliftlem.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) )
cvmliftlem.g ⊢ ( 𝜑 → 𝐺 ∈ ( II Cn 𝐽 ) )
cvmliftlem.p ⊢ ( 𝜑 → 𝑃 ∈ 𝐵 )
cvmliftlem.e ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑃 ) = ( 𝐺 ‘ 0 ) )
Assertion cvmliftlem15 ( 𝜑 → ∃! 𝑓 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑓 ) = 𝐺 ∧ ( 𝑓 ‘ 0 ) = 𝑃 ) )

Proof

Step Hyp Ref Expression
1 cvmliftlem.1 ⊢ 𝑆 = ( 𝑘 ∈ 𝐽 ↦ { 𝑠 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ∣ ( ∪ 𝑠 = ( ◡ 𝐹 “ 𝑘 ) ∧ ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝐹 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ) } )
2 cvmliftlem.b ⊢ 𝐵 = ∪ 𝐶
3 cvmliftlem.x ⊢ 𝑋 = ∪ 𝐽
4 cvmliftlem.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) )
5 cvmliftlem.g ⊢ ( 𝜑 → 𝐺 ∈ ( II Cn 𝐽 ) )
6 cvmliftlem.p ⊢ ( 𝜑 → 𝑃 ∈ 𝐵 )
7 cvmliftlem.e ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑃 ) = ( 𝐺 ‘ 0 ) )
8 ssrab2 ⊢ { 𝑢 ∈ II ∣ ∃ 𝑗 ∈ 𝐽 ∃ 𝑠 ∈ ( 𝑆 ‘ 𝑗 ) ( 𝐺 “ 𝑢 ) ⊆ 𝑗 } ⊆ II
9 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑗 ∈ 𝐽 ∧ ( ( 𝐺 ‘ 𝑥 ) ∈ 𝑗 ∧ ( 𝑆 ‘ 𝑗 ) ≠ ∅ ) ) ) → 𝐺 ∈ ( II Cn 𝐽 ) )
10 simprl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑗 ∈ 𝐽 ∧ ( ( 𝐺 ‘ 𝑥 ) ∈ 𝑗 ∧ ( 𝑆 ‘ 𝑗 ) ≠ ∅ ) ) ) → 𝑗 ∈ 𝐽 )
11 cnima ⊢ ( ( 𝐺 ∈ ( II Cn 𝐽 ) ∧ 𝑗 ∈ 𝐽 ) → ( ◡ 𝐺 “ 𝑗 ) ∈ II )
12 9 10 11 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑗 ∈ 𝐽 ∧ ( ( 𝐺 ‘ 𝑥 ) ∈ 𝑗 ∧ ( 𝑆 ‘ 𝑗 ) ≠ ∅ ) ) ) → ( ◡ 𝐺 “ 𝑗 ) ∈ II )
13 simplr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑗 ∈ 𝐽 ∧ ( ( 𝐺 ‘ 𝑥 ) ∈ 𝑗 ∧ ( 𝑆 ‘ 𝑗 ) ≠ ∅ ) ) ) → 𝑥 ∈ ( 0 [,] 1 ) )
14 simprrl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑗 ∈ 𝐽 ∧ ( ( 𝐺 ‘ 𝑥 ) ∈ 𝑗 ∧ ( 𝑆 ‘ 𝑗 ) ≠ ∅ ) ) ) → ( 𝐺 ‘ 𝑥 ) ∈ 𝑗 )
15 iiuni ⊢ ( 0 [,] 1 ) = ∪ II
16 15 3 cnf ⊢ ( 𝐺 ∈ ( II Cn 𝐽 ) → 𝐺 : ( 0 [,] 1 ) ⟶ 𝑋 )
17 5 16 syl ⊢ ( 𝜑 → 𝐺 : ( 0 [,] 1 ) ⟶ 𝑋 )
18 17 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑗 ∈ 𝐽 ∧ ( ( 𝐺 ‘ 𝑥 ) ∈ 𝑗 ∧ ( 𝑆 ‘ 𝑗 ) ≠ ∅ ) ) ) → 𝐺 : ( 0 [,] 1 ) ⟶ 𝑋 )
19 ffn ⊢ ( 𝐺 : ( 0 [,] 1 ) ⟶ 𝑋 → 𝐺 Fn ( 0 [,] 1 ) )
20 elpreima ⊢ ( 𝐺 Fn ( 0 [,] 1 ) → ( 𝑥 ∈ ( ◡ 𝐺 “ 𝑗 ) ↔ ( 𝑥 ∈ ( 0 [,] 1 ) ∧ ( 𝐺 ‘ 𝑥 ) ∈ 𝑗 ) ) )
21 18 19 20 3syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑗 ∈ 𝐽 ∧ ( ( 𝐺 ‘ 𝑥 ) ∈ 𝑗 ∧ ( 𝑆 ‘ 𝑗 ) ≠ ∅ ) ) ) → ( 𝑥 ∈ ( ◡ 𝐺 “ 𝑗 ) ↔ ( 𝑥 ∈ ( 0 [,] 1 ) ∧ ( 𝐺 ‘ 𝑥 ) ∈ 𝑗 ) ) )
22 13 14 21 mpbir2and ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑗 ∈ 𝐽 ∧ ( ( 𝐺 ‘ 𝑥 ) ∈ 𝑗 ∧ ( 𝑆 ‘ 𝑗 ) ≠ ∅ ) ) ) → 𝑥 ∈ ( ◡ 𝐺 “ 𝑗 ) )
23 simprrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑗 ∈ 𝐽 ∧ ( ( 𝐺 ‘ 𝑥 ) ∈ 𝑗 ∧ ( 𝑆 ‘ 𝑗 ) ≠ ∅ ) ) ) → ( 𝑆 ‘ 𝑗 ) ≠ ∅ )
24 ffun ⊢ ( 𝐺 : ( 0 [,] 1 ) ⟶ 𝑋 → Fun 𝐺 )
25 funimacnv ⊢ ( Fun 𝐺 → ( 𝐺 “ ( ◡ 𝐺 “ 𝑗 ) ) = ( 𝑗 ∩ ran 𝐺 ) )
26 18 24 25 3syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑗 ∈ 𝐽 ∧ ( ( 𝐺 ‘ 𝑥 ) ∈ 𝑗 ∧ ( 𝑆 ‘ 𝑗 ) ≠ ∅ ) ) ) → ( 𝐺 “ ( ◡ 𝐺 “ 𝑗 ) ) = ( 𝑗 ∩ ran 𝐺 ) )
27 inss1 ⊢ ( 𝑗 ∩ ran 𝐺 ) ⊆ 𝑗
28 26 27 eqsstrdi ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑗 ∈ 𝐽 ∧ ( ( 𝐺 ‘ 𝑥 ) ∈ 𝑗 ∧ ( 𝑆 ‘ 𝑗 ) ≠ ∅ ) ) ) → ( 𝐺 “ ( ◡ 𝐺 “ 𝑗 ) ) ⊆ 𝑗 )
29 28 ralrimivw ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑗 ∈ 𝐽 ∧ ( ( 𝐺 ‘ 𝑥 ) ∈ 𝑗 ∧ ( 𝑆 ‘ 𝑗 ) ≠ ∅ ) ) ) → ∀ 𝑠 ∈ ( 𝑆 ‘ 𝑗 ) ( 𝐺 “ ( ◡ 𝐺 “ 𝑗 ) ) ⊆ 𝑗 )
30 r19.2z ⊢ ( ( ( 𝑆 ‘ 𝑗 ) ≠ ∅ ∧ ∀ 𝑠 ∈ ( 𝑆 ‘ 𝑗 ) ( 𝐺 “ ( ◡ 𝐺 “ 𝑗 ) ) ⊆ 𝑗 ) → ∃ 𝑠 ∈ ( 𝑆 ‘ 𝑗 ) ( 𝐺 “ ( ◡ 𝐺 “ 𝑗 ) ) ⊆ 𝑗 )
31 23 29 30 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑗 ∈ 𝐽 ∧ ( ( 𝐺 ‘ 𝑥 ) ∈ 𝑗 ∧ ( 𝑆 ‘ 𝑗 ) ≠ ∅ ) ) ) → ∃ 𝑠 ∈ ( 𝑆 ‘ 𝑗 ) ( 𝐺 “ ( ◡ 𝐺 “ 𝑗 ) ) ⊆ 𝑗 )
32 eleq2 ⊢ ( 𝑢 = ( ◡ 𝐺 “ 𝑗 ) → ( 𝑥 ∈ 𝑢 ↔ 𝑥 ∈ ( ◡ 𝐺 “ 𝑗 ) ) )
33 imaeq2 ⊢ ( 𝑢 = ( ◡ 𝐺 “ 𝑗 ) → ( 𝐺 “ 𝑢 ) = ( 𝐺 “ ( ◡ 𝐺 “ 𝑗 ) ) )
34 33 sseq1d ⊢ ( 𝑢 = ( ◡ 𝐺 “ 𝑗 ) → ( ( 𝐺 “ 𝑢 ) ⊆ 𝑗 ↔ ( 𝐺 “ ( ◡ 𝐺 “ 𝑗 ) ) ⊆ 𝑗 ) )
35 34 rexbidv ⊢ ( 𝑢 = ( ◡ 𝐺 “ 𝑗 ) → ( ∃ 𝑠 ∈ ( 𝑆 ‘ 𝑗 ) ( 𝐺 “ 𝑢 ) ⊆ 𝑗 ↔ ∃ 𝑠 ∈ ( 𝑆 ‘ 𝑗 ) ( 𝐺 “ ( ◡ 𝐺 “ 𝑗 ) ) ⊆ 𝑗 ) )
36 32 35 anbi12d ⊢ ( 𝑢 = ( ◡ 𝐺 “ 𝑗 ) → ( ( 𝑥 ∈ 𝑢 ∧ ∃ 𝑠 ∈ ( 𝑆 ‘ 𝑗 ) ( 𝐺 “ 𝑢 ) ⊆ 𝑗 ) ↔ ( 𝑥 ∈ ( ◡ 𝐺 “ 𝑗 ) ∧ ∃ 𝑠 ∈ ( 𝑆 ‘ 𝑗 ) ( 𝐺 “ ( ◡ 𝐺 “ 𝑗 ) ) ⊆ 𝑗 ) ) )
37 36 rspcev ⊢ ( ( ( ◡ 𝐺 “ 𝑗 ) ∈ II ∧ ( 𝑥 ∈ ( ◡ 𝐺 “ 𝑗 ) ∧ ∃ 𝑠 ∈ ( 𝑆 ‘ 𝑗 ) ( 𝐺 “ ( ◡ 𝐺 “ 𝑗 ) ) ⊆ 𝑗 ) ) → ∃ 𝑢 ∈ II ( 𝑥 ∈ 𝑢 ∧ ∃ 𝑠 ∈ ( 𝑆 ‘ 𝑗 ) ( 𝐺 “ 𝑢 ) ⊆ 𝑗 ) )
38 12 22 31 37 syl12anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑗 ∈ 𝐽 ∧ ( ( 𝐺 ‘ 𝑥 ) ∈ 𝑗 ∧ ( 𝑆 ‘ 𝑗 ) ≠ ∅ ) ) ) → ∃ 𝑢 ∈ II ( 𝑥 ∈ 𝑢 ∧ ∃ 𝑠 ∈ ( 𝑆 ‘ 𝑗 ) ( 𝐺 “ 𝑢 ) ⊆ 𝑗 ) )
39 4 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 [,] 1 ) ) → 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) )
40 17 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 [,] 1 ) ) → ( 𝐺 ‘ 𝑥 ) ∈ 𝑋 )
41 1 3 cvmcov ⊢ ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ ( 𝐺 ‘ 𝑥 ) ∈ 𝑋 ) → ∃ 𝑗 ∈ 𝐽 ( ( 𝐺 ‘ 𝑥 ) ∈ 𝑗 ∧ ( 𝑆 ‘ 𝑗 ) ≠ ∅ ) )
42 39 40 41 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 [,] 1 ) ) → ∃ 𝑗 ∈ 𝐽 ( ( 𝐺 ‘ 𝑥 ) ∈ 𝑗 ∧ ( 𝑆 ‘ 𝑗 ) ≠ ∅ ) )
43 38 42 reximddv ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 [,] 1 ) ) → ∃ 𝑗 ∈ 𝐽 ∃ 𝑢 ∈ II ( 𝑥 ∈ 𝑢 ∧ ∃ 𝑠 ∈ ( 𝑆 ‘ 𝑗 ) ( 𝐺 “ 𝑢 ) ⊆ 𝑗 ) )
44 r19.42v ⊢ ( ∃ 𝑗 ∈ 𝐽 ( 𝑥 ∈ 𝑢 ∧ ∃ 𝑠 ∈ ( 𝑆 ‘ 𝑗 ) ( 𝐺 “ 𝑢 ) ⊆ 𝑗 ) ↔ ( 𝑥 ∈ 𝑢 ∧ ∃ 𝑗 ∈ 𝐽 ∃ 𝑠 ∈ ( 𝑆 ‘ 𝑗 ) ( 𝐺 “ 𝑢 ) ⊆ 𝑗 ) )
45 44 rexbii ⊢ ( ∃ 𝑢 ∈ II ∃ 𝑗 ∈ 𝐽 ( 𝑥 ∈ 𝑢 ∧ ∃ 𝑠 ∈ ( 𝑆 ‘ 𝑗 ) ( 𝐺 “ 𝑢 ) ⊆ 𝑗 ) ↔ ∃ 𝑢 ∈ II ( 𝑥 ∈ 𝑢 ∧ ∃ 𝑗 ∈ 𝐽 ∃ 𝑠 ∈ ( 𝑆 ‘ 𝑗 ) ( 𝐺 “ 𝑢 ) ⊆ 𝑗 ) )
46 rexcom ⊢ ( ∃ 𝑗 ∈ 𝐽 ∃ 𝑢 ∈ II ( 𝑥 ∈ 𝑢 ∧ ∃ 𝑠 ∈ ( 𝑆 ‘ 𝑗 ) ( 𝐺 “ 𝑢 ) ⊆ 𝑗 ) ↔ ∃ 𝑢 ∈ II ∃ 𝑗 ∈ 𝐽 ( 𝑥 ∈ 𝑢 ∧ ∃ 𝑠 ∈ ( 𝑆 ‘ 𝑗 ) ( 𝐺 “ 𝑢 ) ⊆ 𝑗 ) )
47 elunirab ⊢ ( 𝑥 ∈ ∪ { 𝑢 ∈ II ∣ ∃ 𝑗 ∈ 𝐽 ∃ 𝑠 ∈ ( 𝑆 ‘ 𝑗 ) ( 𝐺 “ 𝑢 ) ⊆ 𝑗 } ↔ ∃ 𝑢 ∈ II ( 𝑥 ∈ 𝑢 ∧ ∃ 𝑗 ∈ 𝐽 ∃ 𝑠 ∈ ( 𝑆 ‘ 𝑗 ) ( 𝐺 “ 𝑢 ) ⊆ 𝑗 ) )
48 45 46 47 3bitr4i ⊢ ( ∃ 𝑗 ∈ 𝐽 ∃ 𝑢 ∈ II ( 𝑥 ∈ 𝑢 ∧ ∃ 𝑠 ∈ ( 𝑆 ‘ 𝑗 ) ( 𝐺 “ 𝑢 ) ⊆ 𝑗 ) ↔ 𝑥 ∈ ∪ { 𝑢 ∈ II ∣ ∃ 𝑗 ∈ 𝐽 ∃ 𝑠 ∈ ( 𝑆 ‘ 𝑗 ) ( 𝐺 “ 𝑢 ) ⊆ 𝑗 } )
49 43 48 sylib ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 [,] 1 ) ) → 𝑥 ∈ ∪ { 𝑢 ∈ II ∣ ∃ 𝑗 ∈ 𝐽 ∃ 𝑠 ∈ ( 𝑆 ‘ 𝑗 ) ( 𝐺 “ 𝑢 ) ⊆ 𝑗 } )
50 49 ex ⊢ ( 𝜑 → ( 𝑥 ∈ ( 0 [,] 1 ) → 𝑥 ∈ ∪ { 𝑢 ∈ II ∣ ∃ 𝑗 ∈ 𝐽 ∃ 𝑠 ∈ ( 𝑆 ‘ 𝑗 ) ( 𝐺 “ 𝑢 ) ⊆ 𝑗 } ) )
51 50 ssrdv ⊢ ( 𝜑 → ( 0 [,] 1 ) ⊆ ∪ { 𝑢 ∈ II ∣ ∃ 𝑗 ∈ 𝐽 ∃ 𝑠 ∈ ( 𝑆 ‘ 𝑗 ) ( 𝐺 “ 𝑢 ) ⊆ 𝑗 } )
52 uniss ⊢ ( { 𝑢 ∈ II ∣ ∃ 𝑗 ∈ 𝐽 ∃ 𝑠 ∈ ( 𝑆 ‘ 𝑗 ) ( 𝐺 “ 𝑢 ) ⊆ 𝑗 } ⊆ II → ∪ { 𝑢 ∈ II ∣ ∃ 𝑗 ∈ 𝐽 ∃ 𝑠 ∈ ( 𝑆 ‘ 𝑗 ) ( 𝐺 “ 𝑢 ) ⊆ 𝑗 } ⊆ ∪ II )
53 8 52 mp1i ⊢ ( 𝜑 → ∪ { 𝑢 ∈ II ∣ ∃ 𝑗 ∈ 𝐽 ∃ 𝑠 ∈ ( 𝑆 ‘ 𝑗 ) ( 𝐺 “ 𝑢 ) ⊆ 𝑗 } ⊆ ∪ II )
54 53 15 sseqtrrdi ⊢ ( 𝜑 → ∪ { 𝑢 ∈ II ∣ ∃ 𝑗 ∈ 𝐽 ∃ 𝑠 ∈ ( 𝑆 ‘ 𝑗 ) ( 𝐺 “ 𝑢 ) ⊆ 𝑗 } ⊆ ( 0 [,] 1 ) )
55 51 54 eqssd ⊢ ( 𝜑 → ( 0 [,] 1 ) = ∪ { 𝑢 ∈ II ∣ ∃ 𝑗 ∈ 𝐽 ∃ 𝑠 ∈ ( 𝑆 ‘ 𝑗 ) ( 𝐺 “ 𝑢 ) ⊆ 𝑗 } )
56 lebnumii ⊢ ( ( { 𝑢 ∈ II ∣ ∃ 𝑗 ∈ 𝐽 ∃ 𝑠 ∈ ( 𝑆 ‘ 𝑗 ) ( 𝐺 “ 𝑢 ) ⊆ 𝑗 } ⊆ II ∧ ( 0 [,] 1 ) = ∪ { 𝑢 ∈ II ∣ ∃ 𝑗 ∈ 𝐽 ∃ 𝑠 ∈ ( 𝑆 ‘ 𝑗 ) ( 𝐺 “ 𝑢 ) ⊆ 𝑗 } ) → ∃ 𝑛 ∈ ℕ ∀ 𝑘 ∈ ( 1 ... 𝑛 ) ∃ 𝑣 ∈ { 𝑢 ∈ II ∣ ∃ 𝑗 ∈ 𝐽 ∃ 𝑠 ∈ ( 𝑆 ‘ 𝑗 ) ( 𝐺 “ 𝑢 ) ⊆ 𝑗 } ( ( ( 𝑘 − 1 ) / 𝑛 ) [,] ( 𝑘 / 𝑛 ) ) ⊆ 𝑣 )
57 8 55 56 sylancr ⊢ ( 𝜑 → ∃ 𝑛 ∈ ℕ ∀ 𝑘 ∈ ( 1 ... 𝑛 ) ∃ 𝑣 ∈ { 𝑢 ∈ II ∣ ∃ 𝑗 ∈ 𝐽 ∃ 𝑠 ∈ ( 𝑆 ‘ 𝑗 ) ( 𝐺 “ 𝑢 ) ⊆ 𝑗 } ( ( ( 𝑘 − 1 ) / 𝑛 ) [,] ( 𝑘 / 𝑛 ) ) ⊆ 𝑣 )
58 fzfi ⊢ ( 1 ... 𝑛 ) ∈ Fin
59 imaeq2 ⊢ ( 𝑢 = 𝑣 → ( 𝐺 “ 𝑢 ) = ( 𝐺 “ 𝑣 ) )
60 59 sseq1d ⊢ ( 𝑢 = 𝑣 → ( ( 𝐺 “ 𝑢 ) ⊆ 𝑗 ↔ ( 𝐺 “ 𝑣 ) ⊆ 𝑗 ) )
61 60 2rexbidv ⊢ ( 𝑢 = 𝑣 → ( ∃ 𝑗 ∈ 𝐽 ∃ 𝑠 ∈ ( 𝑆 ‘ 𝑗 ) ( 𝐺 “ 𝑢 ) ⊆ 𝑗 ↔ ∃ 𝑗 ∈ 𝐽 ∃ 𝑠 ∈ ( 𝑆 ‘ 𝑗 ) ( 𝐺 “ 𝑣 ) ⊆ 𝑗 ) )
62 61 rexrab ⊢ ( ∃ 𝑣 ∈ { 𝑢 ∈ II ∣ ∃ 𝑗 ∈ 𝐽 ∃ 𝑠 ∈ ( 𝑆 ‘ 𝑗 ) ( 𝐺 “ 𝑢 ) ⊆ 𝑗 } ( ( ( 𝑘 − 1 ) / 𝑛 ) [,] ( 𝑘 / 𝑛 ) ) ⊆ 𝑣 ↔ ∃ 𝑣 ∈ II ( ∃ 𝑗 ∈ 𝐽 ∃ 𝑠 ∈ ( 𝑆 ‘ 𝑗 ) ( 𝐺 “ 𝑣 ) ⊆ 𝑗 ∧ ( ( ( 𝑘 − 1 ) / 𝑛 ) [,] ( 𝑘 / 𝑛 ) ) ⊆ 𝑣 ) )
63 vex ⊢ 𝑗 ∈ V
64 vex ⊢ 𝑠 ∈ V
65 63 64 op1std ⊢ ( 𝑢 = ⟨ 𝑗 , 𝑠 ⟩ → ( 1st ‘ 𝑢 ) = 𝑗 )
66 65 sseq2d ⊢ ( 𝑢 = ⟨ 𝑗 , 𝑠 ⟩ → ( ( 𝐺 “ 𝑣 ) ⊆ ( 1st ‘ 𝑢 ) ↔ ( 𝐺 “ 𝑣 ) ⊆ 𝑗 ) )
67 66 rexiunxp ⊢ ( ∃ 𝑢 ∈ ∪ 𝑗 ∈ 𝐽 ( { 𝑗 } × ( 𝑆 ‘ 𝑗 ) ) ( 𝐺 “ 𝑣 ) ⊆ ( 1st ‘ 𝑢 ) ↔ ∃ 𝑗 ∈ 𝐽 ∃ 𝑠 ∈ ( 𝑆 ‘ 𝑗 ) ( 𝐺 “ 𝑣 ) ⊆ 𝑗 )
68 imass2 ⊢ ( ( ( ( 𝑘 − 1 ) / 𝑛 ) [,] ( 𝑘 / 𝑛 ) ) ⊆ 𝑣 → ( 𝐺 “ ( ( ( 𝑘 − 1 ) / 𝑛 ) [,] ( 𝑘 / 𝑛 ) ) ) ⊆ ( 𝐺 “ 𝑣 ) )
69 sstr2 ⊢ ( ( 𝐺 “ ( ( ( 𝑘 − 1 ) / 𝑛 ) [,] ( 𝑘 / 𝑛 ) ) ) ⊆ ( 𝐺 “ 𝑣 ) → ( ( 𝐺 “ 𝑣 ) ⊆ ( 1st ‘ 𝑢 ) → ( 𝐺 “ ( ( ( 𝑘 − 1 ) / 𝑛 ) [,] ( 𝑘 / 𝑛 ) ) ) ⊆ ( 1st ‘ 𝑢 ) ) )
70 68 69 syl ⊢ ( ( ( ( 𝑘 − 1 ) / 𝑛 ) [,] ( 𝑘 / 𝑛 ) ) ⊆ 𝑣 → ( ( 𝐺 “ 𝑣 ) ⊆ ( 1st ‘ 𝑢 ) → ( 𝐺 “ ( ( ( 𝑘 − 1 ) / 𝑛 ) [,] ( 𝑘 / 𝑛 ) ) ) ⊆ ( 1st ‘ 𝑢 ) ) )
71 70 reximdv ⊢ ( ( ( ( 𝑘 − 1 ) / 𝑛 ) [,] ( 𝑘 / 𝑛 ) ) ⊆ 𝑣 → ( ∃ 𝑢 ∈ ∪ 𝑗 ∈ 𝐽 ( { 𝑗 } × ( 𝑆 ‘ 𝑗 ) ) ( 𝐺 “ 𝑣 ) ⊆ ( 1st ‘ 𝑢 ) → ∃ 𝑢 ∈ ∪ 𝑗 ∈ 𝐽 ( { 𝑗 } × ( 𝑆 ‘ 𝑗 ) ) ( 𝐺 “ ( ( ( 𝑘 − 1 ) / 𝑛 ) [,] ( 𝑘 / 𝑛 ) ) ) ⊆ ( 1st ‘ 𝑢 ) ) )
72 67 71 syl5bir ⊢ ( ( ( ( 𝑘 − 1 ) / 𝑛 ) [,] ( 𝑘 / 𝑛 ) ) ⊆ 𝑣 → ( ∃ 𝑗 ∈ 𝐽 ∃ 𝑠 ∈ ( 𝑆 ‘ 𝑗 ) ( 𝐺 “ 𝑣 ) ⊆ 𝑗 → ∃ 𝑢 ∈ ∪ 𝑗 ∈ 𝐽 ( { 𝑗 } × ( 𝑆 ‘ 𝑗 ) ) ( 𝐺 “ ( ( ( 𝑘 − 1 ) / 𝑛 ) [,] ( 𝑘 / 𝑛 ) ) ) ⊆ ( 1st ‘ 𝑢 ) ) )
73 72 impcom ⊢ ( ( ∃ 𝑗 ∈ 𝐽 ∃ 𝑠 ∈ ( 𝑆 ‘ 𝑗 ) ( 𝐺 “ 𝑣 ) ⊆ 𝑗 ∧ ( ( ( 𝑘 − 1 ) / 𝑛 ) [,] ( 𝑘 / 𝑛 ) ) ⊆ 𝑣 ) → ∃ 𝑢 ∈ ∪ 𝑗 ∈ 𝐽 ( { 𝑗 } × ( 𝑆 ‘ 𝑗 ) ) ( 𝐺 “ ( ( ( 𝑘 − 1 ) / 𝑛 ) [,] ( 𝑘 / 𝑛 ) ) ) ⊆ ( 1st ‘ 𝑢 ) )
74 73 rexlimivw ⊢ ( ∃ 𝑣 ∈ II ( ∃ 𝑗 ∈ 𝐽 ∃ 𝑠 ∈ ( 𝑆 ‘ 𝑗 ) ( 𝐺 “ 𝑣 ) ⊆ 𝑗 ∧ ( ( ( 𝑘 − 1 ) / 𝑛 ) [,] ( 𝑘 / 𝑛 ) ) ⊆ 𝑣 ) → ∃ 𝑢 ∈ ∪ 𝑗 ∈ 𝐽 ( { 𝑗 } × ( 𝑆 ‘ 𝑗 ) ) ( 𝐺 “ ( ( ( 𝑘 − 1 ) / 𝑛 ) [,] ( 𝑘 / 𝑛 ) ) ) ⊆ ( 1st ‘ 𝑢 ) )
75 62 74 sylbi ⊢ ( ∃ 𝑣 ∈ { 𝑢 ∈ II ∣ ∃ 𝑗 ∈ 𝐽 ∃ 𝑠 ∈ ( 𝑆 ‘ 𝑗 ) ( 𝐺 “ 𝑢 ) ⊆ 𝑗 } ( ( ( 𝑘 − 1 ) / 𝑛 ) [,] ( 𝑘 / 𝑛 ) ) ⊆ 𝑣 → ∃ 𝑢 ∈ ∪ 𝑗 ∈ 𝐽 ( { 𝑗 } × ( 𝑆 ‘ 𝑗 ) ) ( 𝐺 “ ( ( ( 𝑘 − 1 ) / 𝑛 ) [,] ( 𝑘 / 𝑛 ) ) ) ⊆ ( 1st ‘ 𝑢 ) )
76 75 ralimi ⊢ ( ∀ 𝑘 ∈ ( 1 ... 𝑛 ) ∃ 𝑣 ∈ { 𝑢 ∈ II ∣ ∃ 𝑗 ∈ 𝐽 ∃ 𝑠 ∈ ( 𝑆 ‘ 𝑗 ) ( 𝐺 “ 𝑢 ) ⊆ 𝑗 } ( ( ( 𝑘 − 1 ) / 𝑛 ) [,] ( 𝑘 / 𝑛 ) ) ⊆ 𝑣 → ∀ 𝑘 ∈ ( 1 ... 𝑛 ) ∃ 𝑢 ∈ ∪ 𝑗 ∈ 𝐽 ( { 𝑗 } × ( 𝑆 ‘ 𝑗 ) ) ( 𝐺 “ ( ( ( 𝑘 − 1 ) / 𝑛 ) [,] ( 𝑘 / 𝑛 ) ) ) ⊆ ( 1st ‘ 𝑢 ) )
77 fveq2 ⊢ ( 𝑢 = ( 𝑔 ‘ 𝑘 ) → ( 1st ‘ 𝑢 ) = ( 1st ‘ ( 𝑔 ‘ 𝑘 ) ) )
78 77 sseq2d ⊢ ( 𝑢 = ( 𝑔 ‘ 𝑘 ) → ( ( 𝐺 “ ( ( ( 𝑘 − 1 ) / 𝑛 ) [,] ( 𝑘 / 𝑛 ) ) ) ⊆ ( 1st ‘ 𝑢 ) ↔ ( 𝐺 “ ( ( ( 𝑘 − 1 ) / 𝑛 ) [,] ( 𝑘 / 𝑛 ) ) ) ⊆ ( 1st ‘ ( 𝑔 ‘ 𝑘 ) ) ) )
79 78 ac6sfi ⊢ ( ( ( 1 ... 𝑛 ) ∈ Fin ∧ ∀ 𝑘 ∈ ( 1 ... 𝑛 ) ∃ 𝑢 ∈ ∪ 𝑗 ∈ 𝐽 ( { 𝑗 } × ( 𝑆 ‘ 𝑗 ) ) ( 𝐺 “ ( ( ( 𝑘 − 1 ) / 𝑛 ) [,] ( 𝑘 / 𝑛 ) ) ) ⊆ ( 1st ‘ 𝑢 ) ) → ∃ 𝑔 ( 𝑔 : ( 1 ... 𝑛 ) ⟶ ∪ 𝑗 ∈ 𝐽 ( { 𝑗 } × ( 𝑆 ‘ 𝑗 ) ) ∧ ∀ 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝐺 “ ( ( ( 𝑘 − 1 ) / 𝑛 ) [,] ( 𝑘 / 𝑛 ) ) ) ⊆ ( 1st ‘ ( 𝑔 ‘ 𝑘 ) ) ) )
80 58 76 79 sylancr ⊢ ( ∀ 𝑘 ∈ ( 1 ... 𝑛 ) ∃ 𝑣 ∈ { 𝑢 ∈ II ∣ ∃ 𝑗 ∈ 𝐽 ∃ 𝑠 ∈ ( 𝑆 ‘ 𝑗 ) ( 𝐺 “ 𝑢 ) ⊆ 𝑗 } ( ( ( 𝑘 − 1 ) / 𝑛 ) [,] ( 𝑘 / 𝑛 ) ) ⊆ 𝑣 → ∃ 𝑔 ( 𝑔 : ( 1 ... 𝑛 ) ⟶ ∪ 𝑗 ∈ 𝐽 ( { 𝑗 } × ( 𝑆 ‘ 𝑗 ) ) ∧ ∀ 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝐺 “ ( ( ( 𝑘 − 1 ) / 𝑛 ) [,] ( 𝑘 / 𝑛 ) ) ) ⊆ ( 1st ‘ ( 𝑔 ‘ 𝑘 ) ) ) )
81 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑔 : ( 1 ... 𝑛 ) ⟶ ∪ 𝑗 ∈ 𝐽 ( { 𝑗 } × ( 𝑆 ‘ 𝑗 ) ) ∧ ∀ 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝐺 “ ( ( ( 𝑘 − 1 ) / 𝑛 ) [,] ( 𝑘 / 𝑛 ) ) ) ⊆ ( 1st ‘ ( 𝑔 ‘ 𝑘 ) ) ) ) → 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) )
82 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑔 : ( 1 ... 𝑛 ) ⟶ ∪ 𝑗 ∈ 𝐽 ( { 𝑗 } × ( 𝑆 ‘ 𝑗 ) ) ∧ ∀ 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝐺 “ ( ( ( 𝑘 − 1 ) / 𝑛 ) [,] ( 𝑘 / 𝑛 ) ) ) ⊆ ( 1st ‘ ( 𝑔 ‘ 𝑘 ) ) ) ) → 𝐺 ∈ ( II Cn 𝐽 ) )
83 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑔 : ( 1 ... 𝑛 ) ⟶ ∪ 𝑗 ∈ 𝐽 ( { 𝑗 } × ( 𝑆 ‘ 𝑗 ) ) ∧ ∀ 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝐺 “ ( ( ( 𝑘 − 1 ) / 𝑛 ) [,] ( 𝑘 / 𝑛 ) ) ) ⊆ ( 1st ‘ ( 𝑔 ‘ 𝑘 ) ) ) ) → 𝑃 ∈ 𝐵 )
84 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑔 : ( 1 ... 𝑛 ) ⟶ ∪ 𝑗 ∈ 𝐽 ( { 𝑗 } × ( 𝑆 ‘ 𝑗 ) ) ∧ ∀ 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝐺 “ ( ( ( 𝑘 − 1 ) / 𝑛 ) [,] ( 𝑘 / 𝑛 ) ) ) ⊆ ( 1st ‘ ( 𝑔 ‘ 𝑘 ) ) ) ) → ( 𝐹 ‘ 𝑃 ) = ( 𝐺 ‘ 0 ) )
85 simplr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑔 : ( 1 ... 𝑛 ) ⟶ ∪ 𝑗 ∈ 𝐽 ( { 𝑗 } × ( 𝑆 ‘ 𝑗 ) ) ∧ ∀ 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝐺 “ ( ( ( 𝑘 − 1 ) / 𝑛 ) [,] ( 𝑘 / 𝑛 ) ) ) ⊆ ( 1st ‘ ( 𝑔 ‘ 𝑘 ) ) ) ) → 𝑛 ∈ ℕ )
86 simprl ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑔 : ( 1 ... 𝑛 ) ⟶ ∪ 𝑗 ∈ 𝐽 ( { 𝑗 } × ( 𝑆 ‘ 𝑗 ) ) ∧ ∀ 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝐺 “ ( ( ( 𝑘 − 1 ) / 𝑛 ) [,] ( 𝑘 / 𝑛 ) ) ) ⊆ ( 1st ‘ ( 𝑔 ‘ 𝑘 ) ) ) ) → 𝑔 : ( 1 ... 𝑛 ) ⟶ ∪ 𝑗 ∈ 𝐽 ( { 𝑗 } × ( 𝑆 ‘ 𝑗 ) ) )
87 sneq ⊢ ( 𝑗 = 𝑎 → { 𝑗 } = { 𝑎 } )
88 fveq2 ⊢ ( 𝑗 = 𝑎 → ( 𝑆 ‘ 𝑗 ) = ( 𝑆 ‘ 𝑎 ) )
89 87 88 xpeq12d ⊢ ( 𝑗 = 𝑎 → ( { 𝑗 } × ( 𝑆 ‘ 𝑗 ) ) = ( { 𝑎 } × ( 𝑆 ‘ 𝑎 ) ) )
90 89 cbviunv ⊢ ∪ 𝑗 ∈ 𝐽 ( { 𝑗 } × ( 𝑆 ‘ 𝑗 ) ) = ∪ 𝑎 ∈ 𝐽 ( { 𝑎 } × ( 𝑆 ‘ 𝑎 ) )
91 feq3 ⊢ ( ∪ 𝑗 ∈ 𝐽 ( { 𝑗 } × ( 𝑆 ‘ 𝑗 ) ) = ∪ 𝑎 ∈ 𝐽 ( { 𝑎 } × ( 𝑆 ‘ 𝑎 ) ) → ( 𝑔 : ( 1 ... 𝑛 ) ⟶ ∪ 𝑗 ∈ 𝐽 ( { 𝑗 } × ( 𝑆 ‘ 𝑗 ) ) ↔ 𝑔 : ( 1 ... 𝑛 ) ⟶ ∪ 𝑎 ∈ 𝐽 ( { 𝑎 } × ( 𝑆 ‘ 𝑎 ) ) ) )
92 90 91 ax-mp ⊢ ( 𝑔 : ( 1 ... 𝑛 ) ⟶ ∪ 𝑗 ∈ 𝐽 ( { 𝑗 } × ( 𝑆 ‘ 𝑗 ) ) ↔ 𝑔 : ( 1 ... 𝑛 ) ⟶ ∪ 𝑎 ∈ 𝐽 ( { 𝑎 } × ( 𝑆 ‘ 𝑎 ) ) )
93 86 92 sylib ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑔 : ( 1 ... 𝑛 ) ⟶ ∪ 𝑗 ∈ 𝐽 ( { 𝑗 } × ( 𝑆 ‘ 𝑗 ) ) ∧ ∀ 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝐺 “ ( ( ( 𝑘 − 1 ) / 𝑛 ) [,] ( 𝑘 / 𝑛 ) ) ) ⊆ ( 1st ‘ ( 𝑔 ‘ 𝑘 ) ) ) ) → 𝑔 : ( 1 ... 𝑛 ) ⟶ ∪ 𝑎 ∈ 𝐽 ( { 𝑎 } × ( 𝑆 ‘ 𝑎 ) ) )
94 simprr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑔 : ( 1 ... 𝑛 ) ⟶ ∪ 𝑗 ∈ 𝐽 ( { 𝑗 } × ( 𝑆 ‘ 𝑗 ) ) ∧ ∀ 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝐺 “ ( ( ( 𝑘 − 1 ) / 𝑛 ) [,] ( 𝑘 / 𝑛 ) ) ) ⊆ ( 1st ‘ ( 𝑔 ‘ 𝑘 ) ) ) ) → ∀ 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝐺 “ ( ( ( 𝑘 − 1 ) / 𝑛 ) [,] ( 𝑘 / 𝑛 ) ) ) ⊆ ( 1st ‘ ( 𝑔 ‘ 𝑘 ) ) )
95 eqid ⊢ ( topGen ‘ ran (,) ) = ( topGen ‘ ran (,) )
96 2fveq3 ⊢ ( 𝑡 = 𝑧 → ( ◡ ( 𝐹 ↾ ( ℩ 𝑐 ∈ ( 2nd ‘ ( 𝑔 ‘ 𝑤 ) ) ( 𝑦 ‘ ( ( 𝑤 − 1 ) / 𝑛 ) ) ∈ 𝑐 ) ) ‘ ( 𝐺 ‘ 𝑡 ) ) = ( ◡ ( 𝐹 ↾ ( ℩ 𝑐 ∈ ( 2nd ‘ ( 𝑔 ‘ 𝑤 ) ) ( 𝑦 ‘ ( ( 𝑤 − 1 ) / 𝑛 ) ) ∈ 𝑐 ) ) ‘ ( 𝐺 ‘ 𝑧 ) ) )
97 96 cbvmptv ⊢ ( 𝑡 ∈ ( ( ( 𝑤 − 1 ) / 𝑛 ) [,] ( 𝑤 / 𝑛 ) ) ↦ ( ◡ ( 𝐹 ↾ ( ℩ 𝑐 ∈ ( 2nd ‘ ( 𝑔 ‘ 𝑤 ) ) ( 𝑦 ‘ ( ( 𝑤 − 1 ) / 𝑛 ) ) ∈ 𝑐 ) ) ‘ ( 𝐺 ‘ 𝑡 ) ) ) = ( 𝑧 ∈ ( ( ( 𝑤 − 1 ) / 𝑛 ) [,] ( 𝑤 / 𝑛 ) ) ↦ ( ◡ ( 𝐹 ↾ ( ℩ 𝑐 ∈ ( 2nd ‘ ( 𝑔 ‘ 𝑤 ) ) ( 𝑦 ‘ ( ( 𝑤 − 1 ) / 𝑛 ) ) ∈ 𝑐 ) ) ‘ ( 𝐺 ‘ 𝑧 ) ) )
98 eleq2 ⊢ ( 𝑐 = 𝑏 → ( ( 𝑦 ‘ ( ( 𝑤 − 1 ) / 𝑛 ) ) ∈ 𝑐 ↔ ( 𝑦 ‘ ( ( 𝑤 − 1 ) / 𝑛 ) ) ∈ 𝑏 ) )
99 98 cbvriotavw ⊢ ( ℩ 𝑐 ∈ ( 2nd ‘ ( 𝑔 ‘ 𝑤 ) ) ( 𝑦 ‘ ( ( 𝑤 − 1 ) / 𝑛 ) ) ∈ 𝑐 ) = ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑔 ‘ 𝑤 ) ) ( 𝑦 ‘ ( ( 𝑤 − 1 ) / 𝑛 ) ) ∈ 𝑏 )
100 fveq1 ⊢ ( 𝑦 = 𝑥 → ( 𝑦 ‘ ( ( 𝑤 − 1 ) / 𝑛 ) ) = ( 𝑥 ‘ ( ( 𝑤 − 1 ) / 𝑛 ) ) )
101 100 eleq1d ⊢ ( 𝑦 = 𝑥 → ( ( 𝑦 ‘ ( ( 𝑤 − 1 ) / 𝑛 ) ) ∈ 𝑏 ↔ ( 𝑥 ‘ ( ( 𝑤 − 1 ) / 𝑛 ) ) ∈ 𝑏 ) )
102 101 riotabidv ⊢ ( 𝑦 = 𝑥 → ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑔 ‘ 𝑤 ) ) ( 𝑦 ‘ ( ( 𝑤 − 1 ) / 𝑛 ) ) ∈ 𝑏 ) = ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑔 ‘ 𝑤 ) ) ( 𝑥 ‘ ( ( 𝑤 − 1 ) / 𝑛 ) ) ∈ 𝑏 ) )
103 99 102 syl5eq ⊢ ( 𝑦 = 𝑥 → ( ℩ 𝑐 ∈ ( 2nd ‘ ( 𝑔 ‘ 𝑤 ) ) ( 𝑦 ‘ ( ( 𝑤 − 1 ) / 𝑛 ) ) ∈ 𝑐 ) = ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑔 ‘ 𝑤 ) ) ( 𝑥 ‘ ( ( 𝑤 − 1 ) / 𝑛 ) ) ∈ 𝑏 ) )
104 103 reseq2d ⊢ ( 𝑦 = 𝑥 → ( 𝐹 ↾ ( ℩ 𝑐 ∈ ( 2nd ‘ ( 𝑔 ‘ 𝑤 ) ) ( 𝑦 ‘ ( ( 𝑤 − 1 ) / 𝑛 ) ) ∈ 𝑐 ) ) = ( 𝐹 ↾ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑔 ‘ 𝑤 ) ) ( 𝑥 ‘ ( ( 𝑤 − 1 ) / 𝑛 ) ) ∈ 𝑏 ) ) )
105 104 cnveqd ⊢ ( 𝑦 = 𝑥 → ◡ ( 𝐹 ↾ ( ℩ 𝑐 ∈ ( 2nd ‘ ( 𝑔 ‘ 𝑤 ) ) ( 𝑦 ‘ ( ( 𝑤 − 1 ) / 𝑛 ) ) ∈ 𝑐 ) ) = ◡ ( 𝐹 ↾ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑔 ‘ 𝑤 ) ) ( 𝑥 ‘ ( ( 𝑤 − 1 ) / 𝑛 ) ) ∈ 𝑏 ) ) )
106 105 fveq1d ⊢ ( 𝑦 = 𝑥 → ( ◡ ( 𝐹 ↾ ( ℩ 𝑐 ∈ ( 2nd ‘ ( 𝑔 ‘ 𝑤 ) ) ( 𝑦 ‘ ( ( 𝑤 − 1 ) / 𝑛 ) ) ∈ 𝑐 ) ) ‘ ( 𝐺 ‘ 𝑧 ) ) = ( ◡ ( 𝐹 ↾ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑔 ‘ 𝑤 ) ) ( 𝑥 ‘ ( ( 𝑤 − 1 ) / 𝑛 ) ) ∈ 𝑏 ) ) ‘ ( 𝐺 ‘ 𝑧 ) ) )
107 106 mpteq2dv ⊢ ( 𝑦 = 𝑥 → ( 𝑧 ∈ ( ( ( 𝑤 − 1 ) / 𝑛 ) [,] ( 𝑤 / 𝑛 ) ) ↦ ( ◡ ( 𝐹 ↾ ( ℩ 𝑐 ∈ ( 2nd ‘ ( 𝑔 ‘ 𝑤 ) ) ( 𝑦 ‘ ( ( 𝑤 − 1 ) / 𝑛 ) ) ∈ 𝑐 ) ) ‘ ( 𝐺 ‘ 𝑧 ) ) ) = ( 𝑧 ∈ ( ( ( 𝑤 − 1 ) / 𝑛 ) [,] ( 𝑤 / 𝑛 ) ) ↦ ( ◡ ( 𝐹 ↾ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑔 ‘ 𝑤 ) ) ( 𝑥 ‘ ( ( 𝑤 − 1 ) / 𝑛 ) ) ∈ 𝑏 ) ) ‘ ( 𝐺 ‘ 𝑧 ) ) ) )
108 97 107 syl5eq ⊢ ( 𝑦 = 𝑥 → ( 𝑡 ∈ ( ( ( 𝑤 − 1 ) / 𝑛 ) [,] ( 𝑤 / 𝑛 ) ) ↦ ( ◡ ( 𝐹 ↾ ( ℩ 𝑐 ∈ ( 2nd ‘ ( 𝑔 ‘ 𝑤 ) ) ( 𝑦 ‘ ( ( 𝑤 − 1 ) / 𝑛 ) ) ∈ 𝑐 ) ) ‘ ( 𝐺 ‘ 𝑡 ) ) ) = ( 𝑧 ∈ ( ( ( 𝑤 − 1 ) / 𝑛 ) [,] ( 𝑤 / 𝑛 ) ) ↦ ( ◡ ( 𝐹 ↾ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑔 ‘ 𝑤 ) ) ( 𝑥 ‘ ( ( 𝑤 − 1 ) / 𝑛 ) ) ∈ 𝑏 ) ) ‘ ( 𝐺 ‘ 𝑧 ) ) ) )
109 oveq1 ⊢ ( 𝑤 = 𝑚 → ( 𝑤 − 1 ) = ( 𝑚 − 1 ) )
110 109 oveq1d ⊢ ( 𝑤 = 𝑚 → ( ( 𝑤 − 1 ) / 𝑛 ) = ( ( 𝑚 − 1 ) / 𝑛 ) )
111 oveq1 ⊢ ( 𝑤 = 𝑚 → ( 𝑤 / 𝑛 ) = ( 𝑚 / 𝑛 ) )
112 110 111 oveq12d ⊢ ( 𝑤 = 𝑚 → ( ( ( 𝑤 − 1 ) / 𝑛 ) [,] ( 𝑤 / 𝑛 ) ) = ( ( ( 𝑚 − 1 ) / 𝑛 ) [,] ( 𝑚 / 𝑛 ) ) )
113 2fveq3 ⊢ ( 𝑤 = 𝑚 → ( 2nd ‘ ( 𝑔 ‘ 𝑤 ) ) = ( 2nd ‘ ( 𝑔 ‘ 𝑚 ) ) )
114 110 fveq2d ⊢ ( 𝑤 = 𝑚 → ( 𝑥 ‘ ( ( 𝑤 − 1 ) / 𝑛 ) ) = ( 𝑥 ‘ ( ( 𝑚 − 1 ) / 𝑛 ) ) )
115 114 eleq1d ⊢ ( 𝑤 = 𝑚 → ( ( 𝑥 ‘ ( ( 𝑤 − 1 ) / 𝑛 ) ) ∈ 𝑏 ↔ ( 𝑥 ‘ ( ( 𝑚 − 1 ) / 𝑛 ) ) ∈ 𝑏 ) )
116 113 115 riotaeqbidv ⊢ ( 𝑤 = 𝑚 → ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑔 ‘ 𝑤 ) ) ( 𝑥 ‘ ( ( 𝑤 − 1 ) / 𝑛 ) ) ∈ 𝑏 ) = ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑔 ‘ 𝑚 ) ) ( 𝑥 ‘ ( ( 𝑚 − 1 ) / 𝑛 ) ) ∈ 𝑏 ) )
117 116 reseq2d ⊢ ( 𝑤 = 𝑚 → ( 𝐹 ↾ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑔 ‘ 𝑤 ) ) ( 𝑥 ‘ ( ( 𝑤 − 1 ) / 𝑛 ) ) ∈ 𝑏 ) ) = ( 𝐹 ↾ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑔 ‘ 𝑚 ) ) ( 𝑥 ‘ ( ( 𝑚 − 1 ) / 𝑛 ) ) ∈ 𝑏 ) ) )
118 117 cnveqd ⊢ ( 𝑤 = 𝑚 → ◡ ( 𝐹 ↾ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑔 ‘ 𝑤 ) ) ( 𝑥 ‘ ( ( 𝑤 − 1 ) / 𝑛 ) ) ∈ 𝑏 ) ) = ◡ ( 𝐹 ↾ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑔 ‘ 𝑚 ) ) ( 𝑥 ‘ ( ( 𝑚 − 1 ) / 𝑛 ) ) ∈ 𝑏 ) ) )
119 118 fveq1d ⊢ ( 𝑤 = 𝑚 → ( ◡ ( 𝐹 ↾ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑔 ‘ 𝑤 ) ) ( 𝑥 ‘ ( ( 𝑤 − 1 ) / 𝑛 ) ) ∈ 𝑏 ) ) ‘ ( 𝐺 ‘ 𝑧 ) ) = ( ◡ ( 𝐹 ↾ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑔 ‘ 𝑚 ) ) ( 𝑥 ‘ ( ( 𝑚 − 1 ) / 𝑛 ) ) ∈ 𝑏 ) ) ‘ ( 𝐺 ‘ 𝑧 ) ) )
120 112 119 mpteq12dv ⊢ ( 𝑤 = 𝑚 → ( 𝑧 ∈ ( ( ( 𝑤 − 1 ) / 𝑛 ) [,] ( 𝑤 / 𝑛 ) ) ↦ ( ◡ ( 𝐹 ↾ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑔 ‘ 𝑤 ) ) ( 𝑥 ‘ ( ( 𝑤 − 1 ) / 𝑛 ) ) ∈ 𝑏 ) ) ‘ ( 𝐺 ‘ 𝑧 ) ) ) = ( 𝑧 ∈ ( ( ( 𝑚 − 1 ) / 𝑛 ) [,] ( 𝑚 / 𝑛 ) ) ↦ ( ◡ ( 𝐹 ↾ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑔 ‘ 𝑚 ) ) ( 𝑥 ‘ ( ( 𝑚 − 1 ) / 𝑛 ) ) ∈ 𝑏 ) ) ‘ ( 𝐺 ‘ 𝑧 ) ) ) )
121 108 120 cbvmpov ⊢ ( 𝑦 ∈ V , 𝑤 ∈ ℕ ↦ ( 𝑡 ∈ ( ( ( 𝑤 − 1 ) / 𝑛 ) [,] ( 𝑤 / 𝑛 ) ) ↦ ( ◡ ( 𝐹 ↾ ( ℩ 𝑐 ∈ ( 2nd ‘ ( 𝑔 ‘ 𝑤 ) ) ( 𝑦 ‘ ( ( 𝑤 − 1 ) / 𝑛 ) ) ∈ 𝑐 ) ) ‘ ( 𝐺 ‘ 𝑡 ) ) ) ) = ( 𝑥 ∈ V , 𝑚 ∈ ℕ ↦ ( 𝑧 ∈ ( ( ( 𝑚 − 1 ) / 𝑛 ) [,] ( 𝑚 / 𝑛 ) ) ↦ ( ◡ ( 𝐹 ↾ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑔 ‘ 𝑚 ) ) ( 𝑥 ‘ ( ( 𝑚 − 1 ) / 𝑛 ) ) ∈ 𝑏 ) ) ‘ ( 𝐺 ‘ 𝑧 ) ) ) )
122 seqeq2 ⊢ ( ( 𝑦 ∈ V , 𝑤 ∈ ℕ ↦ ( 𝑡 ∈ ( ( ( 𝑤 − 1 ) / 𝑛 ) [,] ( 𝑤 / 𝑛 ) ) ↦ ( ◡ ( 𝐹 ↾ ( ℩ 𝑐 ∈ ( 2nd ‘ ( 𝑔 ‘ 𝑤 ) ) ( 𝑦 ‘ ( ( 𝑤 − 1 ) / 𝑛 ) ) ∈ 𝑐 ) ) ‘ ( 𝐺 ‘ 𝑡 ) ) ) ) = ( 𝑥 ∈ V , 𝑚 ∈ ℕ ↦ ( 𝑧 ∈ ( ( ( 𝑚 − 1 ) / 𝑛 ) [,] ( 𝑚 / 𝑛 ) ) ↦ ( ◡ ( 𝐹 ↾ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑔 ‘ 𝑚 ) ) ( 𝑥 ‘ ( ( 𝑚 − 1 ) / 𝑛 ) ) ∈ 𝑏 ) ) ‘ ( 𝐺 ‘ 𝑧 ) ) ) ) → seq 0 ( ( 𝑦 ∈ V , 𝑤 ∈ ℕ ↦ ( 𝑡 ∈ ( ( ( 𝑤 − 1 ) / 𝑛 ) [,] ( 𝑤 / 𝑛 ) ) ↦ ( ◡ ( 𝐹 ↾ ( ℩ 𝑐 ∈ ( 2nd ‘ ( 𝑔 ‘ 𝑤 ) ) ( 𝑦 ‘ ( ( 𝑤 − 1 ) / 𝑛 ) ) ∈ 𝑐 ) ) ‘ ( 𝐺 ‘ 𝑡 ) ) ) ) , ( ( I ↾ ℕ ) ∪ { ⟨ 0 , { ⟨ 0 , 𝑃 ⟩ } ⟩ } ) ) = seq 0 ( ( 𝑥 ∈ V , 𝑚 ∈ ℕ ↦ ( 𝑧 ∈ ( ( ( 𝑚 − 1 ) / 𝑛 ) [,] ( 𝑚 / 𝑛 ) ) ↦ ( ◡ ( 𝐹 ↾ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑔 ‘ 𝑚 ) ) ( 𝑥 ‘ ( ( 𝑚 − 1 ) / 𝑛 ) ) ∈ 𝑏 ) ) ‘ ( 𝐺 ‘ 𝑧 ) ) ) ) , ( ( I ↾ ℕ ) ∪ { ⟨ 0 , { ⟨ 0 , 𝑃 ⟩ } ⟩ } ) ) )
123 121 122 ax-mp ⊢ seq 0 ( ( 𝑦 ∈ V , 𝑤 ∈ ℕ ↦ ( 𝑡 ∈ ( ( ( 𝑤 − 1 ) / 𝑛 ) [,] ( 𝑤 / 𝑛 ) ) ↦ ( ◡ ( 𝐹 ↾ ( ℩ 𝑐 ∈ ( 2nd ‘ ( 𝑔 ‘ 𝑤 ) ) ( 𝑦 ‘ ( ( 𝑤 − 1 ) / 𝑛 ) ) ∈ 𝑐 ) ) ‘ ( 𝐺 ‘ 𝑡 ) ) ) ) , ( ( I ↾ ℕ ) ∪ { ⟨ 0 , { ⟨ 0 , 𝑃 ⟩ } ⟩ } ) ) = seq 0 ( ( 𝑥 ∈ V , 𝑚 ∈ ℕ ↦ ( 𝑧 ∈ ( ( ( 𝑚 − 1 ) / 𝑛 ) [,] ( 𝑚 / 𝑛 ) ) ↦ ( ◡ ( 𝐹 ↾ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑔 ‘ 𝑚 ) ) ( 𝑥 ‘ ( ( 𝑚 − 1 ) / 𝑛 ) ) ∈ 𝑏 ) ) ‘ ( 𝐺 ‘ 𝑧 ) ) ) ) , ( ( I ↾ ℕ ) ∪ { ⟨ 0 , { ⟨ 0 , 𝑃 ⟩ } ⟩ } ) )
124 eqid ⊢ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) ( seq 0 ( ( 𝑦 ∈ V , 𝑤 ∈ ℕ ↦ ( 𝑡 ∈ ( ( ( 𝑤 − 1 ) / 𝑛 ) [,] ( 𝑤 / 𝑛 ) ) ↦ ( ◡ ( 𝐹 ↾ ( ℩ 𝑐 ∈ ( 2nd ‘ ( 𝑔 ‘ 𝑤 ) ) ( 𝑦 ‘ ( ( 𝑤 − 1 ) / 𝑛 ) ) ∈ 𝑐 ) ) ‘ ( 𝐺 ‘ 𝑡 ) ) ) ) , ( ( I ↾ ℕ ) ∪ { ⟨ 0 , { ⟨ 0 , 𝑃 ⟩ } ⟩ } ) ) ‘ 𝑘 ) = ∪ 𝑘 ∈ ( 1 ... 𝑛 ) ( seq 0 ( ( 𝑦 ∈ V , 𝑤 ∈ ℕ ↦ ( 𝑡 ∈ ( ( ( 𝑤 − 1 ) / 𝑛 ) [,] ( 𝑤 / 𝑛 ) ) ↦ ( ◡ ( 𝐹 ↾ ( ℩ 𝑐 ∈ ( 2nd ‘ ( 𝑔 ‘ 𝑤 ) ) ( 𝑦 ‘ ( ( 𝑤 − 1 ) / 𝑛 ) ) ∈ 𝑐 ) ) ‘ ( 𝐺 ‘ 𝑡 ) ) ) ) , ( ( I ↾ ℕ ) ∪ { ⟨ 0 , { ⟨ 0 , 𝑃 ⟩ } ⟩ } ) ) ‘ 𝑘 )
125 1 2 3 81 82 83 84 85 93 94 95 123 124 cvmliftlem14 ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑔 : ( 1 ... 𝑛 ) ⟶ ∪ 𝑗 ∈ 𝐽 ( { 𝑗 } × ( 𝑆 ‘ 𝑗 ) ) ∧ ∀ 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝐺 “ ( ( ( 𝑘 − 1 ) / 𝑛 ) [,] ( 𝑘 / 𝑛 ) ) ) ⊆ ( 1st ‘ ( 𝑔 ‘ 𝑘 ) ) ) ) → ∃! 𝑓 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑓 ) = 𝐺 ∧ ( 𝑓 ‘ 0 ) = 𝑃 ) )
126 125 ex ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 𝑔 : ( 1 ... 𝑛 ) ⟶ ∪ 𝑗 ∈ 𝐽 ( { 𝑗 } × ( 𝑆 ‘ 𝑗 ) ) ∧ ∀ 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝐺 “ ( ( ( 𝑘 − 1 ) / 𝑛 ) [,] ( 𝑘 / 𝑛 ) ) ) ⊆ ( 1st ‘ ( 𝑔 ‘ 𝑘 ) ) ) → ∃! 𝑓 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑓 ) = 𝐺 ∧ ( 𝑓 ‘ 0 ) = 𝑃 ) ) )
127 126 exlimdv ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ∃ 𝑔 ( 𝑔 : ( 1 ... 𝑛 ) ⟶ ∪ 𝑗 ∈ 𝐽 ( { 𝑗 } × ( 𝑆 ‘ 𝑗 ) ) ∧ ∀ 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝐺 “ ( ( ( 𝑘 − 1 ) / 𝑛 ) [,] ( 𝑘 / 𝑛 ) ) ) ⊆ ( 1st ‘ ( 𝑔 ‘ 𝑘 ) ) ) → ∃! 𝑓 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑓 ) = 𝐺 ∧ ( 𝑓 ‘ 0 ) = 𝑃 ) ) )
128 80 127 syl5 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ∀ 𝑘 ∈ ( 1 ... 𝑛 ) ∃ 𝑣 ∈ { 𝑢 ∈ II ∣ ∃ 𝑗 ∈ 𝐽 ∃ 𝑠 ∈ ( 𝑆 ‘ 𝑗 ) ( 𝐺 “ 𝑢 ) ⊆ 𝑗 } ( ( ( 𝑘 − 1 ) / 𝑛 ) [,] ( 𝑘 / 𝑛 ) ) ⊆ 𝑣 → ∃! 𝑓 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑓 ) = 𝐺 ∧ ( 𝑓 ‘ 0 ) = 𝑃 ) ) )
129 128 rexlimdva ⊢ ( 𝜑 → ( ∃ 𝑛 ∈ ℕ ∀ 𝑘 ∈ ( 1 ... 𝑛 ) ∃ 𝑣 ∈ { 𝑢 ∈ II ∣ ∃ 𝑗 ∈ 𝐽 ∃ 𝑠 ∈ ( 𝑆 ‘ 𝑗 ) ( 𝐺 “ 𝑢 ) ⊆ 𝑗 } ( ( ( 𝑘 − 1 ) / 𝑛 ) [,] ( 𝑘 / 𝑛 ) ) ⊆ 𝑣 → ∃! 𝑓 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑓 ) = 𝐺 ∧ ( 𝑓 ‘ 0 ) = 𝑃 ) ) )
130 57 129 mpd ⊢ ( 𝜑 → ∃! 𝑓 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑓 ) = 𝐺 ∧ ( 𝑓 ‘ 0 ) = 𝑃 ) )