cvmliftlem4

Description: Lemma for cvmlift . The function Q will be our lifted path, defined piecewise on each section [ ( M - 1 ) / N , M / N ] for M e. ( 1 ... N ) . For M = 0 , it is a "seed" value which makes the rest of the recursion work, a singleton function mapping 0 to P . (Contributed by Mario Carneiro, 15-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 (.))$
	cvmliftlem.q	$⊢ Q = seq 0 ((x \in V, m \in ℕ ⟼ (z \in [\frac{m - 1}{N}, \frac{m}{N}] ⟼ {({F ↾}_{(ι b \in 2^{nd} (T (m)) \| x (\frac{m - 1}{N}) \in b)})}^{-1} (G (z)))), (({I ↾}_{ℕ}) \cup \{⟨0, \{⟨0, P⟩\}⟩\}))$
Assertion	cvmliftlem4	$⊢ Q (0) = \{⟨0, P⟩\}$

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		cvmliftlem.q	$⊢ Q = seq 0 ((x \in V, m \in ℕ ⟼ (z \in [\frac{m - 1}{N}, \frac{m}{N}] ⟼ {({F ↾}_{(ι b \in 2^{nd} (T (m)) \| x (\frac{m - 1}{N}) \in b)})}^{-1} (G (z)))), (({I ↾}_{ℕ}) \cup \{⟨0, \{⟨0, P⟩\}⟩\}))$
13	12	fveq1i	$⊢ Q (0) = seq 0 ((x \in V, m \in ℕ ⟼ (z \in [\frac{m - 1}{N}, \frac{m}{N}] ⟼ {({F ↾}_{(ι b \in 2^{nd} (T (m)) \| x (\frac{m - 1}{N}) \in b)})}^{-1} (G (z)))), (({I ↾}_{ℕ}) \cup \{⟨0, \{⟨0, P⟩\}⟩\})) (0)$
14		0z	$⊢ 0 \in ℤ$
15		seq1	$⊢ 0 \in ℤ \to seq 0 ((x \in V, m \in ℕ ⟼ (z \in [\frac{m - 1}{N}, \frac{m}{N}] ⟼ {({F ↾}_{(ι b \in 2^{nd} (T (m)) \| x (\frac{m - 1}{N}) \in b)})}^{-1} (G (z)))), (({I ↾}_{ℕ}) \cup \{⟨0, \{⟨0, P⟩\}⟩\})) (0) = (({I ↾}_{ℕ}) \cup \{⟨0, \{⟨0, P⟩\}⟩\}) (0)$
16	14 15	ax-mp	$⊢ seq 0 ((x \in V, m \in ℕ ⟼ (z \in [\frac{m - 1}{N}, \frac{m}{N}] ⟼ {({F ↾}_{(ι b \in 2^{nd} (T (m)) \| x (\frac{m - 1}{N}) \in b)})}^{-1} (G (z)))), (({I ↾}_{ℕ}) \cup \{⟨0, \{⟨0, P⟩\}⟩\})) (0) = (({I ↾}_{ℕ}) \cup \{⟨0, \{⟨0, P⟩\}⟩\}) (0)$
17	13 16	eqtri	$⊢ Q (0) = (({I ↾}_{ℕ}) \cup \{⟨0, \{⟨0, P⟩\}⟩\}) (0)$
18		fnresi	$⊢ ({I ↾}_{ℕ}) Fn ℕ$
19		c0ex	$⊢ 0 \in V$
20		snex	$⊢ \{⟨0, P⟩\} \in V$
21	19 20	fnsn	$⊢ \{⟨0, \{⟨0, P⟩\}⟩\} Fn \{0\}$
22		0nnn	$⊢ \neg 0 \in ℕ$
23		disjsn	$⊢ ℕ \cap \{0\} = \emptyset \leftrightarrow \neg 0 \in ℕ$
24	22 23	mpbir	$⊢ ℕ \cap \{0\} = \emptyset$
25	19	snid	$⊢ 0 \in \{0\}$
26	24 25	pm3.2i	$⊢ (ℕ \cap \{0\} = \emptyset \land 0 \in \{0\})$
27		fvun2	$⊢ (({I ↾}_{ℕ}) Fn ℕ \land \{⟨0, \{⟨0, P⟩\}⟩\} Fn \{0\} \land (ℕ \cap \{0\} = \emptyset \land 0 \in \{0\})) \to (({I ↾}_{ℕ}) \cup \{⟨0, \{⟨0, P⟩\}⟩\}) (0) = \{⟨0, \{⟨0, P⟩\}⟩\} (0)$
28	18 21 26 27	mp3an	$⊢ (({I ↾}_{ℕ}) \cup \{⟨0, \{⟨0, P⟩\}⟩\}) (0) = \{⟨0, \{⟨0, P⟩\}⟩\} (0)$
29	17 28	eqtri	$⊢ Q (0) = \{⟨0, \{⟨0, P⟩\}⟩\} (0)$
30	19 20	fvsn	$⊢ \{⟨0, \{⟨0, P⟩\}⟩\} (0) = \{⟨0, P⟩\}$
31	29 30	eqtri	$⊢ Q (0) = \{⟨0, P⟩\}$

Metamath Proof Explorer

Theorem cvmliftlem4

Proof