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

Theorem fin23lem29 9557
Description: Lemma for fin23 9605. 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 𝐹 = {𝑔 ∣ ∀𝑎 ∈ (𝒫 𝑔𝑚 ω)(∀𝑥 ∈ ω (𝑎‘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 4388 . . 3 (𝑍 = if(𝑃 ∈ Fin, (𝑡𝑅), ((𝑧𝑃 ↦ ((𝑡𝑧) ∖ ran 𝑈)) ∘ 𝑄)) ↔ ((𝑃 ∈ Fin ∧ 𝑍 = (𝑡𝑅)) ∨ (¬ 𝑃 ∈ Fin ∧ 𝑍 = ((𝑧𝑃 ↦ ((𝑡𝑧) ∖ ran 𝑈)) ∘ 𝑄))))
32biimpi 208 . 2 (𝑍 = if(𝑃 ∈ Fin, (𝑡𝑅), ((𝑧𝑃 ↦ ((𝑡𝑧) ∖ ran 𝑈)) ∘ 𝑄)) → ((𝑃 ∈ Fin ∧ 𝑍 = (𝑡𝑅)) ∨ (¬ 𝑃 ∈ Fin ∧ 𝑍 = ((𝑧𝑃 ↦ ((𝑡𝑧) ∖ ran 𝑈)) ∘ 𝑄))))
4 rneq 5646 . . . . . 6 (𝑍 = (𝑡𝑅) → ran 𝑍 = ran (𝑡𝑅))
54unieqd 4720 . . . . 5 (𝑍 = (𝑡𝑅) → ran 𝑍 = ran (𝑡𝑅))
6 rncoss 5682 . . . . . 6 ran (𝑡𝑅) ⊆ ran 𝑡
76unissi 4733 . . . . 5 ran (𝑡𝑅) ⊆ ran 𝑡
85, 7syl6eqss 3910 . . . 4 (𝑍 = (𝑡𝑅) → ran 𝑍 ran 𝑡)
98adantl 474 . . 3 ((𝑃 ∈ Fin ∧ 𝑍 = (𝑡𝑅)) → ran 𝑍 ran 𝑡)
10 rneq 5646 . . . . . 6 (𝑍 = ((𝑧𝑃 ↦ ((𝑡𝑧) ∖ ran 𝑈)) ∘ 𝑄) → ran 𝑍 = ran ((𝑧𝑃 ↦ ((𝑡𝑧) ∖ ran 𝑈)) ∘ 𝑄))
1110unieqd 4720 . . . . 5 (𝑍 = ((𝑧𝑃 ↦ ((𝑡𝑧) ∖ ran 𝑈)) ∘ 𝑄) → ran 𝑍 = ran ((𝑧𝑃 ↦ ((𝑡𝑧) ∖ ran 𝑈)) ∘ 𝑄))
12 rncoss 5682 . . . . . . 7 ran ((𝑧𝑃 ↦ ((𝑡𝑧) ∖ ran 𝑈)) ∘ 𝑄) ⊆ ran (𝑧𝑃 ↦ ((𝑡𝑧) ∖ ran 𝑈))
1312unissi 4733 . . . . . 6 ran ((𝑧𝑃 ↦ ((𝑡𝑧) ∖ ran 𝑈)) ∘ 𝑄) ⊆ ran (𝑧𝑃 ↦ ((𝑡𝑧) ∖ ran 𝑈))
14 unissb 4741 . . . . . . 7 ( ran (𝑧𝑃 ↦ ((𝑡𝑧) ∖ ran 𝑈)) ⊆ ran 𝑡 ↔ ∀𝑎 ∈ ran (𝑧𝑃 ↦ ((𝑡𝑧) ∖ ran 𝑈))𝑎 ran 𝑡)
15 abid 2759 . . . . . . . . 9 (𝑎 ∈ {𝑎 ∣ ∃𝑧𝑃 𝑎 = ((𝑡𝑧) ∖ ran 𝑈)} ↔ ∃𝑧𝑃 𝑎 = ((𝑡𝑧) ∖ ran 𝑈))
16 fvssunirn 6526 . . . . . . . . . . . . 13 (𝑡𝑧) ⊆ ran 𝑡
1716a1i 11 . . . . . . . . . . . 12 (𝑧𝑃 → (𝑡𝑧) ⊆ ran 𝑡)
1817ssdifssd 4008 . . . . . . . . . . 11 (𝑧𝑃 → ((𝑡𝑧) ∖ ran 𝑈) ⊆ ran 𝑡)
19 sseq1 3881 . . . . . . . . . . 11 (𝑎 = ((𝑡𝑧) ∖ ran 𝑈) → (𝑎 ran 𝑡 ↔ ((𝑡𝑧) ∖ ran 𝑈) ⊆ ran 𝑡))
2018, 19syl5ibrcom 239 . . . . . . . . . 10 (𝑧𝑃 → (𝑎 = ((𝑡𝑧) ∖ ran 𝑈) → 𝑎 ran 𝑡))
2120rexlimiv 3222 . . . . . . . . 9 (∃𝑧𝑃 𝑎 = ((𝑡𝑧) ∖ ran 𝑈) → 𝑎 ran 𝑡)
2215, 21sylbi 209 . . . . . . . 8 (𝑎 ∈ {𝑎 ∣ ∃𝑧𝑃 𝑎 = ((𝑡𝑧) ∖ ran 𝑈)} → 𝑎 ran 𝑡)
23 eqid 2775 . . . . . . . . 9 (𝑧𝑃 ↦ ((𝑡𝑧) ∖ ran 𝑈)) = (𝑧𝑃 ↦ ((𝑡𝑧) ∖ ran 𝑈))
2423rnmpt 5667 . . . . . . . 8 ran (𝑧𝑃 ↦ ((𝑡𝑧) ∖ ran 𝑈)) = {𝑎 ∣ ∃𝑧𝑃 𝑎 = ((𝑡𝑧) ∖ ran 𝑈)}
2522, 24eleq2s 2881 . . . . . . 7 (𝑎 ∈ ran (𝑧𝑃 ↦ ((𝑡𝑧) ∖ ran 𝑈)) → 𝑎 ran 𝑡)
2614, 25mprgbir 3100 . . . . . 6 ran (𝑧𝑃 ↦ ((𝑡𝑧) ∖ ran 𝑈)) ⊆ ran 𝑡
2713, 26sstri 3866 . . . . 5 ran ((𝑧𝑃 ↦ ((𝑡𝑧) ∖ ran 𝑈)) ∘ 𝑄) ⊆ ran 𝑡
2811, 27syl6eqss 3910 . . . 4 (𝑍 = ((𝑧𝑃 ↦ ((𝑡𝑧) ∖ ran 𝑈)) ∘ 𝑄) → ran 𝑍 ran 𝑡)
2928adantl 474 . . 3 ((¬ 𝑃 ∈ Fin ∧ 𝑍 = ((𝑧𝑃 ↦ ((𝑡𝑧) ∖ ran 𝑈)) ∘ 𝑄)) → ran 𝑍 ran 𝑡)
309, 29jaoi 843 . 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 387  wo 833   = wceq 1507  wcel 2048  {cab 2755  wral 3085  wrex 3086  {crab 3089  Vcvv 3412  cdif 3825  cin 3827  wss 3828  c0 4177  ifcif 4348  𝒫 cpw 4420   cuni 4710   cint 4747   class class class wbr 4927  cmpt 5006  ran crn 5405  ccom 5408  suc csuc 6029  cfv 6186  crio 6934  (class class class)co 6974  cmpo 6976  ωcom 7394  seq𝜔cseqom 7883  𝑚 cmap 8202  cen 8299  Fincfn 8302
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1964  ax-8 2050  ax-9 2057  ax-10 2077  ax-11 2091  ax-12 2104  ax-13 2299  ax-ext 2747  ax-sep 5058  ax-nul 5065  ax-pow 5117  ax-pr 5184
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2014  df-mo 2544  df-eu 2580  df-clab 2756  df-cleq 2768  df-clel 2843  df-nfc 2915  df-ne 2965  df-ral 3090  df-rex 3091  df-rab 3094  df-v 3414  df-sbc 3681  df-dif 3831  df-un 3833  df-in 3835  df-ss 3842  df-nul 4178  df-if 4349  df-sn 4440  df-pr 4442  df-op 4446  df-uni 4711  df-br 4928  df-opab 4990  df-mpt 5007  df-cnv 5412  df-co 5413  df-dm 5414  df-rn 5415  df-iota 6150  df-fv 6194
This theorem is referenced by:  fin23lem31  9559
  Copyright terms: Public domain W3C validator