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

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

Proof of Theorem noetasuplem2
StepHypRef Expression
1 noetasuplem.2 . . . 4 𝑍 = (𝑆 ∪ ((suc ( bday 𝐵) ∖ dom 𝑆) × {1o}))
21reseq1i 5819 . . 3 (𝑍 ↾ dom 𝑆) = ((𝑆 ∪ ((suc ( bday 𝐵) ∖ dom 𝑆) × {1o})) ↾ dom 𝑆)
3 resundir 5838 . . 3 ((𝑆 ∪ ((suc ( bday 𝐵) ∖ dom 𝑆) × {1o})) ↾ dom 𝑆) = ((𝑆 ↾ dom 𝑆) ∪ (((suc ( bday 𝐵) ∖ dom 𝑆) × {1o}) ↾ dom 𝑆))
4 dmres 5845 . . . . . 6 dom (((suc ( bday 𝐵) ∖ dom 𝑆) × {1o}) ↾ dom 𝑆) = (dom 𝑆 ∩ dom ((suc ( bday 𝐵) ∖ dom 𝑆) × {1o}))
5 1oex 8120 . . . . . . . . 9 1o ∈ V
65snnz 4669 . . . . . . . 8 {1o} ≠ ∅
7 dmxp 5770 . . . . . . . 8 ({1o} ≠ ∅ → dom ((suc ( bday 𝐵) ∖ dom 𝑆) × {1o}) = (suc ( bday 𝐵) ∖ dom 𝑆))
86, 7ax-mp 5 . . . . . . 7 dom ((suc ( bday 𝐵) ∖ dom 𝑆) × {1o}) = (suc ( bday 𝐵) ∖ dom 𝑆)
98ineq2i 4114 . . . . . 6 (dom 𝑆 ∩ dom ((suc ( bday 𝐵) ∖ dom 𝑆) × {1o})) = (dom 𝑆 ∩ (suc ( bday 𝐵) ∖ dom 𝑆))
10 disjdif 4368 . . . . . 6 (dom 𝑆 ∩ (suc ( bday 𝐵) ∖ dom 𝑆)) = ∅
114, 9, 103eqtri 2785 . . . . 5 dom (((suc ( bday 𝐵) ∖ dom 𝑆) × {1o}) ↾ dom 𝑆) = ∅
12 relres 5852 . . . . . 6 Rel (((suc ( bday 𝐵) ∖ dom 𝑆) × {1o}) ↾ dom 𝑆)
13 reldm0 5769 . . . . . 6 (Rel (((suc ( bday 𝐵) ∖ dom 𝑆) × {1o}) ↾ dom 𝑆) → ((((suc ( bday 𝐵) ∖ dom 𝑆) × {1o}) ↾ dom 𝑆) = ∅ ↔ dom (((suc ( bday 𝐵) ∖ dom 𝑆) × {1o}) ↾ dom 𝑆) = ∅))
1412, 13ax-mp 5 . . . . 5 ((((suc ( bday 𝐵) ∖ dom 𝑆) × {1o}) ↾ dom 𝑆) = ∅ ↔ dom (((suc ( bday 𝐵) ∖ dom 𝑆) × {1o}) ↾ dom 𝑆) = ∅)
1511, 14mpbir 234 . . . 4 (((suc ( bday 𝐵) ∖ dom 𝑆) × {1o}) ↾ dom 𝑆) = ∅
1615uneq2i 4065 . . 3 ((𝑆 ↾ dom 𝑆) ∪ (((suc ( bday 𝐵) ∖ dom 𝑆) × {1o}) ↾ dom 𝑆)) = ((𝑆 ↾ dom 𝑆) ∪ ∅)
172, 3, 163eqtri 2785 . 2 (𝑍 ↾ dom 𝑆) = ((𝑆 ↾ dom 𝑆) ∪ ∅)
18 noetasuplem.1 . . . . . . . 8 𝑆 = if(∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦, ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))))
1918nosupno 33471 . . . . . . 7 ((𝐴 No 𝐴 ∈ V) → 𝑆 No )
20193adant3 1129 . . . . . 6 ((𝐴 No 𝐴 ∈ V ∧ 𝐵 ∈ V) → 𝑆 No )
21 nofun 33417 . . . . . 6 (𝑆 No → Fun 𝑆)
2220, 21syl 17 . . . . 5 ((𝐴 No 𝐴 ∈ V ∧ 𝐵 ∈ V) → Fun 𝑆)
23 funrel 6352 . . . . 5 (Fun 𝑆 → Rel 𝑆)
24 resdm 5868 . . . . 5 (Rel 𝑆 → (𝑆 ↾ dom 𝑆) = 𝑆)
2522, 23, 243syl 18 . . . 4 ((𝐴 No 𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝑆 ↾ dom 𝑆) = 𝑆)
2625uneq1d 4067 . . 3 ((𝐴 No 𝐴 ∈ V ∧ 𝐵 ∈ V) → ((𝑆 ↾ dom 𝑆) ∪ ∅) = (𝑆 ∪ ∅))
27 un0 4286 . . 3 (𝑆 ∪ ∅) = 𝑆
2826, 27eqtrdi 2809 . 2 ((𝐴 No 𝐴 ∈ V ∧ 𝐵 ∈ V) → ((𝑆 ↾ dom 𝑆) ∪ ∅) = 𝑆)
2917, 28syl5eq 2805 1 ((𝐴 No 𝐴 ∈ V ∧ 𝐵 ∈ 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