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	$⊢ S = (k \in J ⟼ \{s \in (𝒫 C ∖ \{\emptyset\}) \| (⋃ s = F^{-1} [k] \land \forall u \in s (\forall v \in (s ∖ \{u\}) u \cap v = \emptyset \land {F ↾}_{u} \in ((C ↾_{𝑡} u) Homeo (J ↾_{𝑡} k))))\})$
	cvmliftlem.b	$⊢ B = ⋃ C$
	cvmliftlem.x	$⊢ X = ⋃ J$
	cvmliftlem.f	$⊢ φ \to F \in (C CovMap J)$
	cvmliftlem.g	$⊢ φ \to G \in (II Cn J)$
	cvmliftlem.p	$⊢ φ \to P \in B$
	cvmliftlem.e	$⊢ φ \to F (P) = G (0)$
	cvmliftlem.n	$⊢ φ \to N \in ℕ$
	cvmliftlem.t	$⊢ φ \to T : (1 \dots N) ⟶ ⋃_{j \in J} (\{j\} \times S (j))$
	cvmliftlem.a	$⊢ φ \to \forall k \in (1 \dots N) G [[\frac{k - 1}{N}, \frac{k}{N}]] \subseteq 1^{st} (T (k))$
	cvmliftlem.l	$⊢ L = topGen (ran (.))$
	cvmliftlem1.m	$⊢ (φ \land ψ) \to M \in (1 \dots N)$
	cvmliftlem3.3	$⊢ W = [\frac{M - 1}{N}, \frac{M}{N}]$
	cvmliftlem3.m	$⊢ (φ \land ψ) \to A \in W$
Assertion	cvmliftlem3	$⊢ (φ \land ψ) \to G (A) \in 1^{st} (T (M))$

Proof

Step	Hyp	Ref	Expression
1		cvmliftlem.1	$⊢ S = (k \in J ⟼ \{s \in (𝒫 C ∖ \{\emptyset\}) \| (⋃ s = F^{-1} [k] \land \forall u \in s (\forall v \in (s ∖ \{u\}) u \cap v = \emptyset \land {F ↾}_{u} \in ((C ↾_{𝑡} u) Homeo (J ↾_{𝑡} k))))\})$
2		cvmliftlem.b	$⊢ B = ⋃ C$
3		cvmliftlem.x	$⊢ X = ⋃ J$
4		cvmliftlem.f	$⊢ φ \to F \in (C CovMap J)$
5		cvmliftlem.g	$⊢ φ \to G \in (II Cn J)$
6		cvmliftlem.p	$⊢ φ \to P \in B$
7		cvmliftlem.e	$⊢ φ \to F (P) = G (0)$
8		cvmliftlem.n	$⊢ φ \to N \in ℕ$
9		cvmliftlem.t	$⊢ φ \to T : (1 \dots N) ⟶ ⋃_{j \in J} (\{j\} \times S (j))$
10		cvmliftlem.a	$⊢ φ \to \forall k \in (1 \dots N) G [[\frac{k - 1}{N}, \frac{k}{N}]] \subseteq 1^{st} (T (k))$
11		cvmliftlem.l	$⊢ L = topGen (ran (.))$
12		cvmliftlem1.m	$⊢ (φ \land ψ) \to M \in (1 \dots N)$
13		cvmliftlem3.3	$⊢ W = [\frac{M - 1}{N}, \frac{M}{N}]$
14		cvmliftlem3.m	$⊢ (φ \land ψ) \to A \in W$
15	10	adantr	$⊢ (φ \land ψ) \to \forall k \in (1 \dots N) G [[\frac{k - 1}{N}, \frac{k}{N}]] \subseteq 1^{st} (T (k))$
16		oveq1	$⊢ k = M \to k - 1 = M - 1$
17	16	oveq1d	$⊢ k = M \to \frac{k - 1}{N} = \frac{M - 1}{N}$
18		oveq1	$⊢ k = M \to \frac{k}{N} = \frac{M}{N}$
19	17 18	oveq12d	$⊢ k = M \to [\frac{k - 1}{N}, \frac{k}{N}] = [\frac{M - 1}{N}, \frac{M}{N}]$
20	19 13	eqtr4di	$⊢ k = M \to [\frac{k - 1}{N}, \frac{k}{N}] = W$
21	20	imaeq2d	$⊢ k = M \to G [[\frac{k - 1}{N}, \frac{k}{N}]] = G [W]$
22		2fveq3	$⊢ k = M \to 1^{st} (T (k)) = 1^{st} (T (M))$
23	21 22	sseq12d	$⊢ k = M \to (G [[\frac{k - 1}{N}, \frac{k}{N}]] \subseteq 1^{st} (T (k)) \leftrightarrow G [W] \subseteq 1^{st} (T (M)))$
24	23	rspcv	$⊢ M \in (1 \dots N) \to (\forall k \in (1 \dots N) G [[\frac{k - 1}{N}, \frac{k}{N}]] \subseteq 1^{st} (T (k)) \to G [W] \subseteq 1^{st} (T (M)))$
25	12 15 24	sylc	$⊢ (φ \land ψ) \to G [W] \subseteq 1^{st} (T (M))$
26		iiuni	$⊢ [0, 1] = ⋃ II$
27	26 3	cnf	$⊢ G \in (II Cn J) \to G : [0, 1] ⟶ X$
28	5 27	syl	$⊢ φ \to G : [0, 1] ⟶ X$
29	28	adantr	$⊢ (φ \land ψ) \to G : [0, 1] ⟶ X$
30	29	ffund	$⊢ (φ \land ψ) \to Fun G$
31	1 2 3 4 5 6 7 8 9 10 11 12 13	cvmliftlem2	$⊢ (φ \land ψ) \to W \subseteq [0, 1]$
32	29	fdmd	$⊢ (φ \land ψ) \to dom G = [0, 1]$
33	31 32	sseqtrrd	$⊢ (φ \land ψ) \to W \subseteq dom G$
34		funfvima2	$⊢ (Fun G \land W \subseteq dom G) \to (A \in W \to G (A) \in G [W])$
35	30 33 34	syl2anc	$⊢ (φ \land ψ) \to (A \in W \to G (A) \in G [W])$
36	14 35	mpd	$⊢ (φ \land ψ) \to G (A) \in G [W]$
37	25 36	sseldd	$⊢ (φ \land ψ) \to G (A) \in 1^{st} (T (M))$

Metamath Proof Explorer

Theorem cvmliftlem3

Proof