MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fin23lem29 Structured version   Visualization version   GIF version

Theorem fin23lem29 10335
Description: Lemma for fin23 10383. The residual is built from the same elements as the previous sequence. (Contributed by Stefan O'Rear, 2-Nov-2014.)
Hypotheses
Ref Expression
fin23lem.a 𝑈 = seqω((𝑖 ∈ ω, 𝑢 ∈ V ↦ if(((𝑡𝑖) ∩ 𝑢) = ∅, 𝑢, ((𝑡𝑖) ∩ 𝑢))), ran 𝑡)
fin23lem17.f 𝐹 = {𝑔 ∣ ∀𝑎 ∈ (𝒫 𝑔m ω)(∀𝑥 ∈ ω (𝑎‘suc 𝑥) ⊆ (𝑎𝑥) → ran 𝑎 ∈ ran 𝑎)}
fin23lem.b 𝑃 = {𝑣 ∈ ω ∣ ran 𝑈 ⊆ (𝑡𝑣)}
fin23lem.c 𝑄 = (𝑤 ∈ ω ↦ (𝑥𝑃 (𝑥𝑃) ≈ 𝑤))
fin23lem.d 𝑅 = (𝑤 ∈ ω ↦ (𝑥 ∈ (ω ∖ 𝑃)(𝑥 ∩ (ω ∖ 𝑃)) ≈ 𝑤))
fin23lem.e 𝑍 = if(𝑃 ∈ Fin, (𝑡𝑅), ((𝑧𝑃 ↦ ((𝑡𝑧) ∖ ran 𝑈)) ∘ 𝑄))
Assertion
Ref Expression
fin23lem29 ran 𝑍 ran 𝑡
Distinct variable groups:   𝑔,𝑖,𝑡,𝑢,𝑣,𝑥,𝑧,𝑎   𝐹,𝑎,𝑡   𝑤,𝑎,𝑥,𝑧,𝑃   𝑣,𝑎,𝑅,𝑖,𝑢   𝑈,𝑎,𝑖,𝑢,𝑣,𝑧   𝑍,𝑎   𝑔,𝑎
Allowed substitution hints:   𝑃(𝑣,𝑢,𝑡,𝑔,𝑖)   𝑄(𝑥,𝑧,𝑤,𝑣,𝑢,𝑡,𝑔,𝑖,𝑎)   𝑅(𝑥,𝑧,𝑤,𝑡,𝑔)   𝑈(𝑥,𝑤,𝑡,𝑔)   𝐹(𝑥,𝑧,𝑤,𝑣,𝑢,𝑔,𝑖)   𝑍(𝑥,𝑧,𝑤,𝑣,𝑢,𝑡,𝑔,𝑖)

Proof of Theorem fin23lem29
StepHypRef Expression
1 fin23lem.e . 2 𝑍 = if(𝑃 ∈ Fin, (𝑡𝑅), ((𝑧𝑃 ↦ ((𝑡𝑧) ∖ ran 𝑈)) ∘ 𝑄))
2 eqif 4569 . . 3 (𝑍 = if(𝑃 ∈ Fin, (𝑡𝑅), ((𝑧𝑃 ↦ ((𝑡𝑧) ∖ ran 𝑈)) ∘ 𝑄)) ↔ ((𝑃 ∈ Fin ∧ 𝑍 = (𝑡𝑅)) ∨ (¬ 𝑃 ∈ Fin ∧ 𝑍 = ((𝑧𝑃 ↦ ((𝑡𝑧) ∖ ran 𝑈)) ∘ 𝑄))))
32biimpi 215 . 2 (𝑍 = if(𝑃 ∈ Fin, (𝑡𝑅), ((𝑧𝑃 ↦ ((𝑡𝑧) ∖ ran 𝑈)) ∘ 𝑄)) → ((𝑃 ∈ Fin ∧ 𝑍 = (𝑡𝑅)) ∨ (¬ 𝑃 ∈ Fin ∧ 𝑍 = ((𝑧𝑃 ↦ ((𝑡𝑧) ∖ ran 𝑈)) ∘ 𝑄))))
4 rneq 5935 . . . . . 6 (𝑍 = (𝑡𝑅) → ran 𝑍 = ran (𝑡𝑅))
54unieqd 4922 . . . . 5 (𝑍 = (𝑡𝑅) → ran 𝑍 = ran (𝑡𝑅))
6 rncoss 5971 . . . . . 6 ran (𝑡𝑅) ⊆ ran 𝑡
76unissi 4917 . . . . 5 ran (𝑡𝑅) ⊆ ran 𝑡
85, 7eqsstrdi 4036 . . . 4 (𝑍 = (𝑡𝑅) → ran 𝑍 ran 𝑡)
98adantl 482 . . 3 ((𝑃 ∈ Fin ∧ 𝑍 = (𝑡𝑅)) → ran 𝑍 ran 𝑡)
10 rneq 5935 . . . . . 6 (𝑍 = ((𝑧𝑃 ↦ ((𝑡𝑧) ∖ ran 𝑈)) ∘ 𝑄) → ran 𝑍 = ran ((𝑧𝑃 ↦ ((𝑡𝑧) ∖ ran 𝑈)) ∘ 𝑄))
1110unieqd 4922 . . . . 5 (𝑍 = ((𝑧𝑃 ↦ ((𝑡𝑧) ∖ ran 𝑈)) ∘ 𝑄) → ran 𝑍 = ran ((𝑧𝑃 ↦ ((𝑡𝑧) ∖ ran 𝑈)) ∘ 𝑄))
12 rncoss 5971 . . . . . . 7 ran ((𝑧𝑃 ↦ ((𝑡𝑧) ∖ ran 𝑈)) ∘ 𝑄) ⊆ ran (𝑧𝑃 ↦ ((𝑡𝑧) ∖ ran 𝑈))
1312unissi 4917 . . . . . 6 ran ((𝑧𝑃 ↦ ((𝑡𝑧) ∖ ran 𝑈)) ∘ 𝑄) ⊆ ran (𝑧𝑃 ↦ ((𝑡𝑧) ∖ ran 𝑈))
14 unissb 4943 . . . . . . 7 ( ran (𝑧𝑃 ↦ ((𝑡𝑧) ∖ ran 𝑈)) ⊆ ran 𝑡 ↔ ∀𝑎 ∈ ran (𝑧𝑃 ↦ ((𝑡𝑧) ∖ ran 𝑈))𝑎 ran 𝑡)
15 abid 2713 . . . . . . . . 9 (𝑎 ∈ {𝑎 ∣ ∃𝑧𝑃 𝑎 = ((𝑡𝑧) ∖ ran 𝑈)} ↔ ∃𝑧𝑃 𝑎 = ((𝑡𝑧) ∖ ran 𝑈))
16 fvssunirn 6924 . . . . . . . . . . . . 13 (𝑡𝑧) ⊆ ran 𝑡
1716a1i 11 . . . . . . . . . . . 12 (𝑧𝑃 → (𝑡𝑧) ⊆ ran 𝑡)
1817ssdifssd 4142 . . . . . . . . . . 11 (𝑧𝑃 → ((𝑡𝑧) ∖ ran 𝑈) ⊆ ran 𝑡)
19 sseq1 4007 . . . . . . . . . . 11 (𝑎 = ((𝑡𝑧) ∖ ran 𝑈) → (𝑎 ran 𝑡 ↔ ((𝑡𝑧) ∖ ran 𝑈) ⊆ ran 𝑡))
2018, 19syl5ibrcom 246 . . . . . . . . . 10 (𝑧𝑃 → (𝑎 = ((𝑡𝑧) ∖ ran 𝑈) → 𝑎 ran 𝑡))
2120rexlimiv 3148 . . . . . . . . 9 (∃𝑧𝑃 𝑎 = ((𝑡𝑧) ∖ ran 𝑈) → 𝑎 ran 𝑡)
2215, 21sylbi 216 . . . . . . . 8 (𝑎 ∈ {𝑎 ∣ ∃𝑧𝑃 𝑎 = ((𝑡𝑧) ∖ ran 𝑈)} → 𝑎 ran 𝑡)
23 eqid 2732 . . . . . . . . 9 (𝑧𝑃 ↦ ((𝑡𝑧) ∖ ran 𝑈)) = (𝑧𝑃 ↦ ((𝑡𝑧) ∖ ran 𝑈))
2423rnmpt 5954 . . . . . . . 8 ran (𝑧𝑃 ↦ ((𝑡𝑧) ∖ ran 𝑈)) = {𝑎 ∣ ∃𝑧𝑃 𝑎 = ((𝑡𝑧) ∖ ran 𝑈)}
2522, 24eleq2s 2851 . . . . . . 7 (𝑎 ∈ ran (𝑧𝑃 ↦ ((𝑡𝑧) ∖ ran 𝑈)) → 𝑎 ran 𝑡)
2614, 25mprgbir 3068 . . . . . 6 ran (𝑧𝑃 ↦ ((𝑡𝑧) ∖ ran 𝑈)) ⊆ ran 𝑡
2713, 26sstri 3991 . . . . 5 ran ((𝑧𝑃 ↦ ((𝑡𝑧) ∖ ran 𝑈)) ∘ 𝑄) ⊆ ran 𝑡
2811, 27eqsstrdi 4036 . . . 4 (𝑍 = ((𝑧𝑃 ↦ ((𝑡𝑧) ∖ ran 𝑈)) ∘ 𝑄) → ran 𝑍 ran 𝑡)
2928adantl 482 . . 3 ((¬ 𝑃 ∈ Fin ∧ 𝑍 = ((𝑧𝑃 ↦ ((𝑡𝑧) ∖ ran 𝑈)) ∘ 𝑄)) → ran 𝑍 ran 𝑡)
309, 29jaoi 855 . 2 (((𝑃 ∈ Fin ∧ 𝑍 = (𝑡𝑅)) ∨ (¬ 𝑃 ∈ Fin ∧ 𝑍 = ((𝑧𝑃 ↦ ((𝑡𝑧) ∖ ran 𝑈)) ∘ 𝑄))) → ran 𝑍 ran 𝑡)
311, 3, 30mp2b 10 1 ran 𝑍 ran 𝑡
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 396  wo 845   = wceq 1541  wcel 2106  {cab 2709  wral 3061  wrex 3070  {crab 3432  Vcvv 3474  cdif 3945  cin 3947  wss 3948  c0 4322  ifcif 4528  𝒫 cpw 4602   cuni 4908   cint 4950   class class class wbr 5148  cmpt 5231  ran crn 5677  ccom 5680  suc csuc 6366  cfv 6543  crio 7363  (class class class)co 7408  cmpo 7410  ωcom 7854  seqωcseqom 8446  m cmap 8819  cen 8935  Fincfn 8938
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pr 5427
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-opab 5211  df-mpt 5232  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-iota 6495  df-fv 6551
This theorem is referenced by:  fin23lem31  10337
  Copyright terms: Public domain W3C validator