Mathbox for Scott Fenton < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  noetainflem2 Structured version   Visualization version   GIF version

Theorem noetainflem2 33506
 Description: Lemma for noeta 33511. The restriction of 𝑊 to the domain of 𝑇 is 𝑇. (Contributed by Scott Fenton, 9-Aug-2024.)
Hypotheses
Ref Expression
noetainflem.1 𝑇 = if(∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥, ((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥), 1o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))))
noetainflem.2 𝑊 = (𝑇 ∪ ((suc ( bday 𝐴) ∖ dom 𝑇) × {2o}))
Assertion
Ref Expression
noetainflem2 ((𝐵 No 𝐵 ∈ V) → (𝑊 ↾ dom 𝑇) = 𝑇)
Distinct variable group:   𝐵,𝑔,𝑢,𝑣,𝑥,𝑦
Allowed substitution hints:   𝐴(𝑥,𝑦,𝑣,𝑢,𝑔)   𝑇(𝑥,𝑦,𝑣,𝑢,𝑔)   𝑊(𝑥,𝑦,𝑣,𝑢,𝑔)

Proof of Theorem noetainflem2
StepHypRef Expression
1 noetainflem.2 . . . 4 𝑊 = (𝑇 ∪ ((suc ( bday 𝐴) ∖ dom 𝑇) × {2o}))
21reseq1i 5819 . . 3 (𝑊 ↾ dom 𝑇) = ((𝑇 ∪ ((suc ( bday 𝐴) ∖ dom 𝑇) × {2o})) ↾ dom 𝑇)
3 resundir 5838 . . 3 ((𝑇 ∪ ((suc ( bday 𝐴) ∖ dom 𝑇) × {2o})) ↾ dom 𝑇) = ((𝑇 ↾ dom 𝑇) ∪ (((suc ( bday 𝐴) ∖ dom 𝑇) × {2o}) ↾ dom 𝑇))
42, 3eqtri 2781 . 2 (𝑊 ↾ dom 𝑇) = ((𝑇 ↾ dom 𝑇) ∪ (((suc ( bday 𝐴) ∖ dom 𝑇) × {2o}) ↾ dom 𝑇))
5 noetainflem.1 . . . . . . 7 𝑇 = if(∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥, ((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥), 1o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))))
65noinfno 33486 . . . . . 6 ((𝐵 No 𝐵 ∈ V) → 𝑇 No )
7 nofun 33417 . . . . . 6 (𝑇 No → Fun 𝑇)
86, 7syl 17 . . . . 5 ((𝐵 No 𝐵 ∈ V) → Fun 𝑇)
9 funrel 6352 . . . . 5 (Fun 𝑇 → Rel 𝑇)
10 resdm 5868 . . . . 5 (Rel 𝑇 → (𝑇 ↾ dom 𝑇) = 𝑇)
118, 9, 103syl 18 . . . 4 ((𝐵 No 𝐵 ∈ V) → (𝑇 ↾ dom 𝑇) = 𝑇)
12 dmres 5845 . . . . . . 7 dom (((suc ( bday 𝐴) ∖ dom 𝑇) × {2o}) ↾ dom 𝑇) = (dom 𝑇 ∩ dom ((suc ( bday 𝐴) ∖ dom 𝑇) × {2o}))
13 2oex 8122 . . . . . . . . . . 11 2o ∈ V
1413snnz 4669 . . . . . . . . . 10 {2o} ≠ ∅
15 dmxp 5770 . . . . . . . . . 10 ({2o} ≠ ∅ → dom ((suc ( bday 𝐴) ∖ dom 𝑇) × {2o}) = (suc ( bday 𝐴) ∖ dom 𝑇))
1614, 15ax-mp 5 . . . . . . . . 9 dom ((suc ( bday 𝐴) ∖ dom 𝑇) × {2o}) = (suc ( bday 𝐴) ∖ dom 𝑇)
1716ineq2i 4114 . . . . . . . 8 (dom 𝑇 ∩ dom ((suc ( bday 𝐴) ∖ dom 𝑇) × {2o})) = (dom 𝑇 ∩ (suc ( bday 𝐴) ∖ dom 𝑇))
18 disjdif 4368 . . . . . . . 8 (dom 𝑇 ∩ (suc ( bday 𝐴) ∖ dom 𝑇)) = ∅
1917, 18eqtri 2781 . . . . . . 7 (dom 𝑇 ∩ dom ((suc ( bday 𝐴) ∖ dom 𝑇) × {2o})) = ∅
2012, 19eqtri 2781 . . . . . 6 dom (((suc ( bday 𝐴) ∖ dom 𝑇) × {2o}) ↾ dom 𝑇) = ∅
21 relres 5852 . . . . . . 7 Rel (((suc ( bday 𝐴) ∖ dom 𝑇) × {2o}) ↾ dom 𝑇)
22 reldm0 5769 . . . . . . 7 (Rel (((suc ( bday 𝐴) ∖ dom 𝑇) × {2o}) ↾ dom 𝑇) → ((((suc ( bday 𝐴) ∖ dom 𝑇) × {2o}) ↾ dom 𝑇) = ∅ ↔ dom (((suc ( bday 𝐴) ∖ dom 𝑇) × {2o}) ↾ dom 𝑇) = ∅))
2321, 22ax-mp 5 . . . . . 6 ((((suc ( bday 𝐴) ∖ dom 𝑇) × {2o}) ↾ dom 𝑇) = ∅ ↔ dom (((suc ( bday 𝐴) ∖ dom 𝑇) × {2o}) ↾ dom 𝑇) = ∅)
2420, 23mpbir 234 . . . . 5 (((suc ( bday 𝐴) ∖ dom 𝑇) × {2o}) ↾ dom 𝑇) = ∅
2524a1i 11 . . . 4 ((𝐵 No 𝐵 ∈ V) → (((suc ( bday 𝐴) ∖ dom 𝑇) × {2o}) ↾ dom 𝑇) = ∅)
2611, 25uneq12d 4069 . . 3 ((𝐵 No 𝐵 ∈ V) → ((𝑇 ↾ dom 𝑇) ∪ (((suc ( bday 𝐴) ∖ dom 𝑇) × {2o}) ↾ dom 𝑇)) = (𝑇 ∪ ∅))
27 un0 4286 . . 3 (𝑇 ∪ ∅) = 𝑇
2826, 27eqtrdi 2809 . 2 ((𝐵 No 𝐵 ∈ V) → ((𝑇 ↾ dom 𝑇) ∪ (((suc ( bday 𝐴) ∖ dom 𝑇) × {2o}) ↾ dom 𝑇)) = 𝑇)
294, 28syl5eq 2805 1 ((𝐵 No 𝐵 ∈ V) → (𝑊 ↾ dom 𝑇) = 𝑇)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   ∧ w3a 1084   = wceq 1538   ∈ wcel 2111  {cab 2735   ≠ wne 2951  ∀wral 3070  ∃wrex 3071  Vcvv 3409   ∖ cdif 3855   ∪ cun 3856   ∩ cin 3857   ⊆ wss 3858  ∅c0 4225  ifcif 4420  {csn 4522  ⟨cop 4528  ∪ cuni 4798   class class class wbr 5032   ↦ cmpt 5112   × cxp 5522  dom cdm 5524   ↾ cres 5526   “ cima 5527  Rel wrel 5529  suc csuc 6171  ℩cio 6292  Fun wfun 6329  ‘cfv 6335  ℩crio 7107  1oc1o 8105  2oc2o 8106   No csur 33408
 Copyright terms: Public domain W3C validator