Theorem cvmliftlem3

Description: Lemma for cvmlift . Since 1st( TM ) is a neighborhood of ( G " W ) , every element A e. W satisfies ( GA ) e. ( 1st( TM ) ) . (Contributed by Mario Carneiro, 16-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 (,) )
	cvmliftlem1.m	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑀 ∈ ( 1 ... 𝑁 ) )
	cvmliftlem3.3	⊢ 𝑊 = ( ( ( 𝑀 − 1 ) / 𝑁 ) [,] ( 𝑀 / 𝑁 ) )
	cvmliftlem3.m	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝐴 ∈ 𝑊 )
Assertion	cvmliftlem3	⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝐺 ‘ 𝐴 ) ∈ ( 1st ‘ ( 𝑇 ‘ 𝑀 ) ) )

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		cvmliftlem1.m	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑀 ∈ ( 1 ... 𝑁 ) )
13		cvmliftlem3.3	⊢ 𝑊 = ( ( ( 𝑀 − 1 ) / 𝑁 ) [,] ( 𝑀 / 𝑁 ) )
14		cvmliftlem3.m	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝐴 ∈ 𝑊 )
15	10	adantr	⊢ ( ( 𝜑 ∧ 𝜓 ) → ∀ 𝑘 ∈ ( 1 ... 𝑁 ) ( 𝐺 “ ( ( ( 𝑘 − 1 ) / 𝑁 ) [,] ( 𝑘 / 𝑁 ) ) ) ⊆ ( 1st ‘ ( 𝑇 ‘ 𝑘 ) ) )
16		oveq1	⊢ ( 𝑘 = 𝑀 → ( 𝑘 − 1 ) = ( 𝑀 − 1 ) )
17	16	oveq1d	⊢ ( 𝑘 = 𝑀 → ( ( 𝑘 − 1 ) / 𝑁 ) = ( ( 𝑀 − 1 ) / 𝑁 ) )
18		oveq1	⊢ ( 𝑘 = 𝑀 → ( 𝑘 / 𝑁 ) = ( 𝑀 / 𝑁 ) )
19	17 18	oveq12d	⊢ ( 𝑘 = 𝑀 → ( ( ( 𝑘 − 1 ) / 𝑁 ) [,] ( 𝑘 / 𝑁 ) ) = ( ( ( 𝑀 − 1 ) / 𝑁 ) [,] ( 𝑀 / 𝑁 ) ) )
20	19 13	eqtr4di	⊢ ( 𝑘 = 𝑀 → ( ( ( 𝑘 − 1 ) / 𝑁 ) [,] ( 𝑘 / 𝑁 ) ) = 𝑊 )
21	20	imaeq2d	⊢ ( 𝑘 = 𝑀 → ( 𝐺 “ ( ( ( 𝑘 − 1 ) / 𝑁 ) [,] ( 𝑘 / 𝑁 ) ) ) = ( 𝐺 “ 𝑊 ) )
22		2fveq3	⊢ ( 𝑘 = 𝑀 → ( 1st ‘ ( 𝑇 ‘ 𝑘 ) ) = ( 1st ‘ ( 𝑇 ‘ 𝑀 ) ) )
23	21 22	sseq12d	⊢ ( 𝑘 = 𝑀 → ( ( 𝐺 “ ( ( ( 𝑘 − 1 ) / 𝑁 ) [,] ( 𝑘 / 𝑁 ) ) ) ⊆ ( 1st ‘ ( 𝑇 ‘ 𝑘 ) ) ↔ ( 𝐺 “ 𝑊 ) ⊆ ( 1st ‘ ( 𝑇 ‘ 𝑀 ) ) ) )
24	23	rspcv	⊢ ( 𝑀 ∈ ( 1 ... 𝑁 ) → ( ∀ 𝑘 ∈ ( 1 ... 𝑁 ) ( 𝐺 “ ( ( ( 𝑘 − 1 ) / 𝑁 ) [,] ( 𝑘 / 𝑁 ) ) ) ⊆ ( 1st ‘ ( 𝑇 ‘ 𝑘 ) ) → ( 𝐺 “ 𝑊 ) ⊆ ( 1st ‘ ( 𝑇 ‘ 𝑀 ) ) ) )
25	12 15 24	sylc	⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝐺 “ 𝑊 ) ⊆ ( 1st ‘ ( 𝑇 ‘ 𝑀 ) ) )
26		iiuni	⊢ ( 0 [,] 1 ) = ∪ II
27	26 3	cnf	⊢ ( 𝐺 ∈ ( II Cn 𝐽 ) → 𝐺 : ( 0 [,] 1 ) ⟶ 𝑋 )
28	5 27	syl	⊢ ( 𝜑 → 𝐺 : ( 0 [,] 1 ) ⟶ 𝑋 )
29	28	adantr	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝐺 : ( 0 [,] 1 ) ⟶ 𝑋 )
30	29	ffund	⊢ ( ( 𝜑 ∧ 𝜓 ) → Fun 𝐺 )
31	1 2 3 4 5 6 7 8 9 10 11 12 13	cvmliftlem2	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑊 ⊆ ( 0 [,] 1 ) )
32	29	fdmd	⊢ ( ( 𝜑 ∧ 𝜓 ) → dom 𝐺 = ( 0 [,] 1 ) )
33	31 32	sseqtrrd	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑊 ⊆ dom 𝐺 )
34		funfvima2	⊢ ( ( Fun 𝐺 ∧ 𝑊 ⊆ dom 𝐺 ) → ( 𝐴 ∈ 𝑊 → ( 𝐺 ‘ 𝐴 ) ∈ ( 𝐺 “ 𝑊 ) ) )
35	30 33 34	syl2anc	⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝐴 ∈ 𝑊 → ( 𝐺 ‘ 𝐴 ) ∈ ( 𝐺 “ 𝑊 ) ) )
36	14 35	mpd	⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝐺 ‘ 𝐴 ) ∈ ( 𝐺 “ 𝑊 ) )
37	25 36	sseldd	⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝐺 ‘ 𝐴 ) ∈ ( 1st ‘ ( 𝑇 ‘ 𝑀 ) ) )