cvmliftlem1

Description: Lemma for cvmlift . In cvmliftlem15 , we picked an N large enough so that the sections ( G " [ ( k - 1 ) / N , k / N ] ) are all contained in an even covering, and the function T enumerates these even coverings. So 1st( TM ) is a neighborhood of ( G " [ ( M - 1 ) / N , M / N ] ) , and 2nd( TM ) is an even covering of 1st( TM ) , which is to say a disjoint union of open sets in C whose image is 1st( TM ) . (Contributed by Mario Carneiro, 14-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)$
Assertion	cvmliftlem1	$⊢ (φ \land ψ) \to 2^{nd} (T (M)) \in S (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		relxp	$⊢ Rel (\{j\} \times S (j))$
14	13	rgenw	$⊢ \forall j \in J Rel (\{j\} \times S (j))$
15		reliun	$⊢ Rel ⋃_{j \in J} (\{j\} \times S (j)) \leftrightarrow \forall j \in J Rel (\{j\} \times S (j))$
16	14 15	mpbir	$⊢ Rel ⋃_{j \in J} (\{j\} \times S (j))$
17	9	adantr	$⊢ (φ \land ψ) \to T : (1 \dots N) ⟶ ⋃_{j \in J} (\{j\} \times S (j))$
18	17 12	ffvelrnd	$⊢ (φ \land ψ) \to T (M) \in ⋃_{j \in J} (\{j\} \times S (j))$
19		1st2nd	$⊢ (Rel ⋃_{j \in J} (\{j\} \times S (j)) \land T (M) \in ⋃_{j \in J} (\{j\} \times S (j))) \to T (M) = ⟨1^{st} (T (M)), 2^{nd} (T (M))⟩$
20	16 18 19	sylancr	$⊢ (φ \land ψ) \to T (M) = ⟨1^{st} (T (M)), 2^{nd} (T (M))⟩$
21	20 18	eqeltrrd	$⊢ (φ \land ψ) \to ⟨1^{st} (T (M)), 2^{nd} (T (M))⟩ \in ⋃_{j \in J} (\{j\} \times S (j))$
22		fveq2	$⊢ j = 1^{st} (T (M)) \to S (j) = S (1^{st} (T (M)))$
23	22	opeliunxp2	$⊢ ⟨1^{st} (T (M)), 2^{nd} (T (M))⟩ \in ⋃_{j \in J} (\{j\} \times S (j)) \leftrightarrow (1^{st} (T (M)) \in J \land 2^{nd} (T (M)) \in S (1^{st} (T (M))))$
24	23	simprbi	$⊢ ⟨1^{st} (T (M)), 2^{nd} (T (M))⟩ \in ⋃_{j \in J} (\{j\} \times S (j)) \to 2^{nd} (T (M)) \in S (1^{st} (T (M)))$
25	21 24	syl	$⊢ (φ \land ψ) \to 2^{nd} (T (M)) \in S (1^{st} (T (M)))$

Metamath Proof Explorer

Theorem cvmliftlem1

Proof