Mathbox for Mario Carneiro < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  cvmliftlem4 Structured version   Visualization version   GIF version

Theorem cvmliftlem4 32759
 Description: Lemma for cvmlift 32770. The function 𝑄 will be our lifted path, defined piecewise on each section [(𝑀 − 1) / 𝑁, 𝑀 / 𝑁] for 𝑀 ∈ (1...𝑁). For 𝑀 = 0, it is a "seed" value which makes the rest of the recursion work, a singleton function mapping 0 to 𝑃. (Contributed by Mario Carneiro, 15-Feb-2015.)
Hypotheses
Ref Expression
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 𝑄 = seq0((𝑥 ∈ V, 𝑚 ∈ ℕ ↦ (𝑧 ∈ (((𝑚 − 1) / 𝑁)[,](𝑚 / 𝑁)) ↦ ((𝐹 ↾ (𝑏 ∈ (2nd ‘(𝑇𝑚))(𝑥‘((𝑚 − 1) / 𝑁)) ∈ 𝑏))‘(𝐺𝑧)))), (( I ↾ ℕ) ∪ {⟨0, {⟨0, 𝑃⟩}⟩}))
Assertion
Ref Expression
cvmliftlem4 (𝑄‘0) = {⟨0, 𝑃⟩}
Distinct variable groups:   𝑣,𝑏,𝑧,𝐵   𝑗,𝑏,𝑘,𝑚,𝑠,𝑢,𝑥,𝐹,𝑣,𝑧   𝑧,𝐿   𝑃,𝑏,𝑘,𝑚,𝑢,𝑣,𝑥,𝑧   𝐶,𝑏,𝑗,𝑘,𝑠,𝑢,𝑣,𝑧   𝜑,𝑗,𝑠,𝑥,𝑧   𝑁,𝑏,𝑘,𝑚,𝑢,𝑣,𝑥,𝑧   𝑆,𝑏,𝑗,𝑘,𝑠,𝑢,𝑣,𝑥,𝑧   𝑗,𝑋   𝐺,𝑏,𝑗,𝑘,𝑚,𝑠,𝑢,𝑣,𝑥,𝑧   𝑇,𝑏,𝑗,𝑘,𝑚,𝑠,𝑢,𝑣,𝑥,𝑧   𝐽,𝑏,𝑗,𝑘,𝑠,𝑢,𝑣,𝑥,𝑧   𝑄,𝑏,𝑘,𝑚,𝑢,𝑣,𝑥,𝑧
Allowed substitution hints:   𝜑(𝑣,𝑢,𝑘,𝑚,𝑏)   𝐵(𝑥,𝑢,𝑗,𝑘,𝑚,𝑠)   𝐶(𝑥,𝑚)   𝑃(𝑗,𝑠)   𝑄(𝑗,𝑠)   𝑆(𝑚)   𝐽(𝑚)   𝐿(𝑥,𝑣,𝑢,𝑗,𝑘,𝑚,𝑠,𝑏)   𝑁(𝑗,𝑠)   𝑋(𝑥,𝑧,𝑣,𝑢,𝑘,𝑚,𝑠,𝑏)

Proof of Theorem cvmliftlem4
StepHypRef Expression
1 cvmliftlem.q . . . . 5 𝑄 = seq0((𝑥 ∈ V, 𝑚 ∈ ℕ ↦ (𝑧 ∈ (((𝑚 − 1) / 𝑁)[,](𝑚 / 𝑁)) ↦ ((𝐹 ↾ (𝑏 ∈ (2nd ‘(𝑇𝑚))(𝑥‘((𝑚 − 1) / 𝑁)) ∈ 𝑏))‘(𝐺𝑧)))), (( I ↾ ℕ) ∪ {⟨0, {⟨0, 𝑃⟩}⟩}))
21fveq1i 6660 . . . 4 (𝑄‘0) = (seq0((𝑥 ∈ V, 𝑚 ∈ ℕ ↦ (𝑧 ∈ (((𝑚 − 1) / 𝑁)[,](𝑚 / 𝑁)) ↦ ((𝐹 ↾ (𝑏 ∈ (2nd ‘(𝑇𝑚))(𝑥‘((𝑚 − 1) / 𝑁)) ∈ 𝑏))‘(𝐺𝑧)))), (( I ↾ ℕ) ∪ {⟨0, {⟨0, 𝑃⟩}⟩}))‘0)
3 0z 12024 . . . . 5 0 ∈ ℤ
4 seq1 13424 . . . . 5 (0 ∈ ℤ → (seq0((𝑥 ∈ V, 𝑚 ∈ ℕ ↦ (𝑧 ∈ (((𝑚 − 1) / 𝑁)[,](𝑚 / 𝑁)) ↦ ((𝐹 ↾ (𝑏 ∈ (2nd ‘(𝑇𝑚))(𝑥‘((𝑚 − 1) / 𝑁)) ∈ 𝑏))‘(𝐺𝑧)))), (( I ↾ ℕ) ∪ {⟨0, {⟨0, 𝑃⟩}⟩}))‘0) = ((( I ↾ ℕ) ∪ {⟨0, {⟨0, 𝑃⟩}⟩})‘0))
53, 4ax-mp 5 . . . 4 (seq0((𝑥 ∈ V, 𝑚 ∈ ℕ ↦ (𝑧 ∈ (((𝑚 − 1) / 𝑁)[,](𝑚 / 𝑁)) ↦ ((𝐹 ↾ (𝑏 ∈ (2nd ‘(𝑇𝑚))(𝑥‘((𝑚 − 1) / 𝑁)) ∈ 𝑏))‘(𝐺𝑧)))), (( I ↾ ℕ) ∪ {⟨0, {⟨0, 𝑃⟩}⟩}))‘0) = ((( I ↾ ℕ) ∪ {⟨0, {⟨0, 𝑃⟩}⟩})‘0)
62, 5eqtri 2782 . . 3 (𝑄‘0) = ((( I ↾ ℕ) ∪ {⟨0, {⟨0, 𝑃⟩}⟩})‘0)
7 fnresi 6460 . . . 4 ( I ↾ ℕ) Fn ℕ
8 c0ex 10666 . . . . 5 0 ∈ V
9 snex 5301 . . . . 5 {⟨0, 𝑃⟩} ∈ V
108, 9fnsn 6394 . . . 4 {⟨0, {⟨0, 𝑃⟩}⟩} Fn {0}
11 0nnn 11703 . . . . . 6 ¬ 0 ∈ ℕ
12 disjsn 4605 . . . . . 6 ((ℕ ∩ {0}) = ∅ ↔ ¬ 0 ∈ ℕ)
1311, 12mpbir 234 . . . . 5 (ℕ ∩ {0}) = ∅
148snid 4559 . . . . 5 0 ∈ {0}
1513, 14pm3.2i 475 . . . 4 ((ℕ ∩ {0}) = ∅ ∧ 0 ∈ {0})
16 fvun2 6745 . . . 4 ((( I ↾ ℕ) Fn ℕ ∧ {⟨0, {⟨0, 𝑃⟩}⟩} Fn {0} ∧ ((ℕ ∩ {0}) = ∅ ∧ 0 ∈ {0})) → ((( I ↾ ℕ) ∪ {⟨0, {⟨0, 𝑃⟩}⟩})‘0) = ({⟨0, {⟨0, 𝑃⟩}⟩}‘0))
177, 10, 15, 16mp3an 1459 . . 3 ((( I ↾ ℕ) ∪ {⟨0, {⟨0, 𝑃⟩}⟩})‘0) = ({⟨0, {⟨0, 𝑃⟩}⟩}‘0)
186, 17eqtri 2782 . 2 (𝑄‘0) = ({⟨0, {⟨0, 𝑃⟩}⟩}‘0)
198, 9fvsn 6935 . 2 ({⟨0, {⟨0, 𝑃⟩}⟩}‘0) = {⟨0, 𝑃⟩}
2018, 19eqtri 2782 1 (𝑄‘0) = {⟨0, 𝑃⟩}
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 400   = wceq 1539   ∈ wcel 2112  ∀wral 3071  {crab 3075  Vcvv 3410   ∖ cdif 3856   ∪ cun 3857   ∩ cin 3858   ⊆ wss 3859  ∅c0 4226  𝒫 cpw 4495  {csn 4523  ⟨cop 4529  ∪ cuni 4799  ∪ ciun 4884   ↦ cmpt 5113   I cid 5430   × cxp 5523  ◡ccnv 5524  ran crn 5526   ↾ cres 5527   “ cima 5528   Fn wfn 6331  ⟶wf 6332  ‘cfv 6336  ℩crio 7108  (class class class)co 7151   ∈ cmpo 7153  1st c1st 7692  2nd c2nd 7693  0cc0 10568  1c1 10569   − cmin 10901   / cdiv 11328  ℕcn 11667  ℤcz 12013  (,)cioo 12772  [,]cicc 12775  ...cfz 12932  seqcseq 13411   ↾t crest 16745  topGenctg 16762   Cn ccn 21917  Homeochmeo 22446  IIcii 23569   CovMap ccvm 32726 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2730  ax-sep 5170  ax-nul 5177  ax-pow 5235  ax-pr 5299  ax-un 7460  ax-cnex 10624  ax-resscn 10625  ax-1cn 10626  ax-icn 10627  ax-addcl 10628  ax-addrcl 10629  ax-mulcl 10630  ax-mulrcl 10631  ax-mulcom 10632  ax-addass 10633  ax-mulass 10634  ax-distr 10635  ax-i2m1 10636  ax-1ne0 10637  ax-1rid 10638  ax-rnegex 10639  ax-rrecex 10640  ax-cnre 10641  ax-pre-lttri 10642  ax-pre-lttrn 10643  ax-pre-ltadd 10644  ax-pre-mulgt0 10645 This theorem depends on definitions:  df-bi 210  df-an 401  df-or 846  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2071  df-mo 2558  df-eu 2589  df-clab 2737  df-cleq 2751  df-clel 2831  df-nfc 2902  df-ne 2953  df-nel 3057  df-ral 3076  df-rex 3077  df-reu 3078  df-rab 3080  df-v 3412  df-sbc 3698  df-csb 3807  df-dif 3862  df-un 3864  df-in 3866  df-ss 3876  df-pss 3878  df-nul 4227  df-if 4422  df-pw 4497  df-sn 4524  df-pr 4526  df-tp 4528  df-op 4530  df-uni 4800  df-iun 4886  df-br 5034  df-opab 5096  df-mpt 5114  df-tr 5140  df-id 5431  df-eprel 5436  df-po 5444  df-so 5445  df-fr 5484  df-we 5486  df-xp 5531  df-rel 5532  df-cnv 5533  df-co 5534  df-dm 5535  df-rn 5536  df-res 5537  df-ima 5538  df-pred 6127  df-ord 6173  df-on 6174  df-lim 6175  df-suc 6176  df-iota 6295  df-fun 6338  df-fn 6339  df-f 6340  df-f1 6341  df-fo 6342  df-f1o 6343  df-fv 6344  df-riota 7109  df-ov 7154  df-oprab 7155  df-mpo 7156  df-om 7581  df-2nd 7695  df-wrecs 7958  df-recs 8019  df-rdg 8057  df-er 8300  df-en 8529  df-dom 8530  df-sdom 8531  df-pnf 10708  df-mnf 10709  df-xr 10710  df-ltxr 10711  df-le 10712  df-sub 10903  df-neg 10904  df-nn 11668  df-n0 11928  df-z 12014  df-uz 12276  df-seq 13412 This theorem is referenced by:  cvmliftlem7  32762  cvmliftlem13  32767
 Copyright terms: Public domain W3C validator