Theorem cvmliftlem11

Description: Lemma for cvmlift . (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 ) )
	cvmliftlem.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
	cvmliftlem.t	⊢ ( 𝜑 → 𝑇 : ( 1 ... 𝑁 ) ⟶ ∪ 𝑗 ∈ 𝐽 ( { 𝑗 } × ( 𝑆 ‘ 𝑗 ) ) )
	cvmliftlem.a	⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 1 ... 𝑁 ) ( 𝐺 “ ( ( ( 𝑘 − 1 ) / 𝑁 ) [,] ( 𝑘 / 𝑁 ) ) ) ⊆ ( 1st ‘ ( 𝑇 ‘ 𝑘 ) ) )
	cvmliftlem.l	⊢ 𝐿 = ( topGen ‘ ran (,) )
	cvmliftlem.q	⊢ 𝑄 = seq 0 ( ( 𝑥 ∈ V , 𝑚 ∈ ℕ ↦ ( 𝑧 ∈ ( ( ( 𝑚 − 1 ) / 𝑁 ) [,] ( 𝑚 / 𝑁 ) ) ↦ ( ◡ ( 𝐹 ↾ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑚 ) ) ( 𝑥 ‘ ( ( 𝑚 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ) ‘ ( 𝐺 ‘ 𝑧 ) ) ) ) , ( ( I ↾ ℕ ) ∪ { ⟨ 0 , { ⟨ 0 , 𝑃 ⟩ } ⟩ } ) )
	cvmliftlem.k	⊢ 𝐾 = ∪ 𝑘 ∈ ( 1 ... 𝑁 ) ( 𝑄 ‘ 𝑘 )
Assertion	cvmliftlem11	⊢ ( 𝜑 → ( 𝐾 ∈ ( II Cn 𝐶 ) ∧ ( 𝐹 ∘ 𝐾 ) = 𝐺 ) )

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		cvmliftlem.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
9		cvmliftlem.t	⊢ ( 𝜑 → 𝑇 : ( 1 ... 𝑁 ) ⟶ ∪ 𝑗 ∈ 𝐽 ( { 𝑗 } × ( 𝑆 ‘ 𝑗 ) ) )
10		cvmliftlem.a	⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 1 ... 𝑁 ) ( 𝐺 “ ( ( ( 𝑘 − 1 ) / 𝑁 ) [,] ( 𝑘 / 𝑁 ) ) ) ⊆ ( 1st ‘ ( 𝑇 ‘ 𝑘 ) ) )
11		cvmliftlem.l	⊢ 𝐿 = ( topGen ‘ ran (,) )
12		cvmliftlem.q	⊢ 𝑄 = seq 0 ( ( 𝑥 ∈ V , 𝑚 ∈ ℕ ↦ ( 𝑧 ∈ ( ( ( 𝑚 − 1 ) / 𝑁 ) [,] ( 𝑚 / 𝑁 ) ) ↦ ( ◡ ( 𝐹 ↾ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑚 ) ) ( 𝑥 ‘ ( ( 𝑚 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ) ‘ ( 𝐺 ‘ 𝑧 ) ) ) ) , ( ( I ↾ ℕ ) ∪ { ⟨ 0 , { ⟨ 0 , 𝑃 ⟩ } ⟩ } ) )
13		cvmliftlem.k	⊢ 𝐾 = ∪ 𝑘 ∈ ( 1 ... 𝑁 ) ( 𝑄 ‘ 𝑘 )
14		biid	⊢ ( ( ( 𝑛 ∈ ℕ ∧ ( 𝑛 + 1 ) ∈ ( 1 ... 𝑁 ) ) ∧ ( ∪ 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝑄 ‘ 𝑘 ) ∈ ( ( 𝐿 ↾t ( 0 [,] ( 𝑛 / 𝑁 ) ) ) Cn 𝐶 ) ∧ ( 𝐹 ∘ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝑄 ‘ 𝑘 ) ) = ( 𝐺 ↾ ( 0 [,] ( 𝑛 / 𝑁 ) ) ) ) ) ↔ ( ( 𝑛 ∈ ℕ ∧ ( 𝑛 + 1 ) ∈ ( 1 ... 𝑁 ) ) ∧ ( ∪ 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝑄 ‘ 𝑘 ) ∈ ( ( 𝐿 ↾t ( 0 [,] ( 𝑛 / 𝑁 ) ) ) Cn 𝐶 ) ∧ ( 𝐹 ∘ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝑄 ‘ 𝑘 ) ) = ( 𝐺 ↾ ( 0 [,] ( 𝑛 / 𝑁 ) ) ) ) ) )
15	1 2 3 4 5 6 7 8 9 10 11 12 13 14	cvmliftlem10	⊢ ( 𝜑 → ( 𝐾 ∈ ( ( 𝐿 ↾t ( 0 [,] ( 𝑁 / 𝑁 ) ) ) Cn 𝐶 ) ∧ ( 𝐹 ∘ 𝐾 ) = ( 𝐺 ↾ ( 0 [,] ( 𝑁 / 𝑁 ) ) ) ) )
16	15	simpld	⊢ ( 𝜑 → 𝐾 ∈ ( ( 𝐿 ↾t ( 0 [,] ( 𝑁 / 𝑁 ) ) ) Cn 𝐶 ) )
17	11	a1i	⊢ ( 𝜑 → 𝐿 = ( topGen ‘ ran (,) ) )
18	8	nncnd	⊢ ( 𝜑 → 𝑁 ∈ ℂ )
19	8	nnne0d	⊢ ( 𝜑 → 𝑁 ≠ 0 )
20	18 19	dividd	⊢ ( 𝜑 → ( 𝑁 / 𝑁 ) = 1 )
21	20	oveq2d	⊢ ( 𝜑 → ( 0 [,] ( 𝑁 / 𝑁 ) ) = ( 0 [,] 1 ) )
22	17 21	oveq12d	⊢ ( 𝜑 → ( 𝐿 ↾t ( 0 [,] ( 𝑁 / 𝑁 ) ) ) = ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] 1 ) ) )
23		dfii2	⊢ II = ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] 1 ) )
24	22 23	eqtr4di	⊢ ( 𝜑 → ( 𝐿 ↾t ( 0 [,] ( 𝑁 / 𝑁 ) ) ) = II )
25	24	oveq1d	⊢ ( 𝜑 → ( ( 𝐿 ↾t ( 0 [,] ( 𝑁 / 𝑁 ) ) ) Cn 𝐶 ) = ( II Cn 𝐶 ) )
26	16 25	eleqtrd	⊢ ( 𝜑 → 𝐾 ∈ ( II Cn 𝐶 ) )
27	15	simprd	⊢ ( 𝜑 → ( 𝐹 ∘ 𝐾 ) = ( 𝐺 ↾ ( 0 [,] ( 𝑁 / 𝑁 ) ) ) )
28	21	reseq2d	⊢ ( 𝜑 → ( 𝐺 ↾ ( 0 [,] ( 𝑁 / 𝑁 ) ) ) = ( 𝐺 ↾ ( 0 [,] 1 ) ) )
29		iiuni	⊢ ( 0 [,] 1 ) = ∪ II
30	29 3	cnf	⊢ ( 𝐺 ∈ ( II Cn 𝐽 ) → 𝐺 : ( 0 [,] 1 ) ⟶ 𝑋 )
31		ffn	⊢ ( 𝐺 : ( 0 [,] 1 ) ⟶ 𝑋 → 𝐺 Fn ( 0 [,] 1 ) )
32		fnresdm	⊢ ( 𝐺 Fn ( 0 [,] 1 ) → ( 𝐺 ↾ ( 0 [,] 1 ) ) = 𝐺 )
33	5 30 31 32	4syl	⊢ ( 𝜑 → ( 𝐺 ↾ ( 0 [,] 1 ) ) = 𝐺 )
34	27 28 33	3eqtrd	⊢ ( 𝜑 → ( 𝐹 ∘ 𝐾 ) = 𝐺 )
35	26 34	jca	⊢ ( 𝜑 → ( 𝐾 ∈ ( II Cn 𝐶 ) ∧ ( 𝐹 ∘ 𝐾 ) = 𝐺 ) )