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

Theorem noetalem4 33345
 Description: Lemma for noeta 33347. Bound the birthday of 𝑍 above. (Contributed by Scott Fenton, 6-Dec-2021.)
Hypotheses
Ref Expression
noetalem.1 𝑆 = if(∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦, ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))))
noetalem.2 𝑍 = (𝑆 ∪ ((suc ( bday 𝐵) ∖ dom 𝑆) × {1o}))
Assertion
Ref Expression
noetalem4 (((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) → ( bday 𝑍) ⊆ suc ( bday “ (𝐴𝐵)))
Distinct variable group:   𝐴,𝑔,𝑢,𝑣,𝑥,𝑦
Allowed substitution hints:   𝐵(𝑥,𝑦,𝑣,𝑢,𝑔)   𝑆(𝑥,𝑦,𝑣,𝑢,𝑔)   𝑍(𝑥,𝑦,𝑣,𝑢,𝑔)

Proof of Theorem noetalem4
StepHypRef Expression
1 noetalem.1 . . . . . . 7 𝑆 = if(∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦, ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))))
21nosupno 33328 . . . . . 6 ((𝐴 No 𝐴 ∈ V) → 𝑆 No )
3 bdayval 33280 . . . . . 6 (𝑆 No → ( bday 𝑆) = dom 𝑆)
42, 3syl 17 . . . . 5 ((𝐴 No 𝐴 ∈ V) → ( bday 𝑆) = dom 𝑆)
51nosupbday 33330 . . . . 5 ((𝐴 No 𝐴 ∈ V) → ( bday 𝑆) ⊆ suc ( bday 𝐴))
64, 5eqsstrrd 3954 . . . 4 ((𝐴 No 𝐴 ∈ V) → dom 𝑆 ⊆ suc ( bday 𝐴))
76adantr 484 . . 3 (((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) → dom 𝑆 ⊆ suc ( bday 𝐴))
8 unss1 4106 . . 3 (dom 𝑆 ⊆ suc ( bday 𝐴) → (dom 𝑆 ∪ suc ( bday 𝐵)) ⊆ (suc ( bday 𝐴) ∪ suc ( bday 𝐵)))
97, 8syl 17 . 2 (((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) → (dom 𝑆 ∪ suc ( bday 𝐵)) ⊆ (suc ( bday 𝐴) ∪ suc ( bday 𝐵)))
10 simpll 766 . . . . 5 (((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) → 𝐴 No )
11 simplr 768 . . . . 5 (((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) → 𝐴 ∈ V)
12 simprr 772 . . . . 5 (((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) → 𝐵 ∈ V)
13 noetalem.2 . . . . . 6 𝑍 = (𝑆 ∪ ((suc ( bday 𝐵) ∖ dom 𝑆) × {1o}))
141, 13noetalem1 33342 . . . . 5 ((𝐴 No 𝐴 ∈ V ∧ 𝐵 ∈ V) → 𝑍 No )
1510, 11, 12, 14syl3anc 1368 . . . 4 (((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) → 𝑍 No )
16 bdayval 33280 . . . 4 (𝑍 No → ( bday 𝑍) = dom 𝑍)
1715, 16syl 17 . . 3 (((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) → ( bday 𝑍) = dom 𝑍)
1813dmeqi 5737 . . . 4 dom 𝑍 = dom (𝑆 ∪ ((suc ( bday 𝐵) ∖ dom 𝑆) × {1o}))
19 dmun 5743 . . . . 5 dom (𝑆 ∪ ((suc ( bday 𝐵) ∖ dom 𝑆) × {1o})) = (dom 𝑆 ∪ dom ((suc ( bday 𝐵) ∖ dom 𝑆) × {1o}))
20 1oex 8095 . . . . . . . . 9 1o ∈ V
2120snnz 4672 . . . . . . . 8 {1o} ≠ ∅
22 dmxp 5763 . . . . . . . 8 ({1o} ≠ ∅ → dom ((suc ( bday 𝐵) ∖ dom 𝑆) × {1o}) = (suc ( bday 𝐵) ∖ dom 𝑆))
2321, 22ax-mp 5 . . . . . . 7 dom ((suc ( bday 𝐵) ∖ dom 𝑆) × {1o}) = (suc ( bday 𝐵) ∖ dom 𝑆)
2423uneq2i 4087 . . . . . 6 (dom 𝑆 ∪ dom ((suc ( bday 𝐵) ∖ dom 𝑆) × {1o})) = (dom 𝑆 ∪ (suc ( bday 𝐵) ∖ dom 𝑆))
25 undif2 4383 . . . . . 6 (dom 𝑆 ∪ (suc ( bday 𝐵) ∖ dom 𝑆)) = (dom 𝑆 ∪ suc ( bday 𝐵))
2624, 25eqtri 2821 . . . . 5 (dom 𝑆 ∪ dom ((suc ( bday 𝐵) ∖ dom 𝑆) × {1o})) = (dom 𝑆 ∪ suc ( bday 𝐵))
2719, 26eqtri 2821 . . . 4 dom (𝑆 ∪ ((suc ( bday 𝐵) ∖ dom 𝑆) × {1o})) = (dom 𝑆 ∪ suc ( bday 𝐵))
2818, 27eqtri 2821 . . 3 dom 𝑍 = (dom 𝑆 ∪ suc ( bday 𝐵))
2917, 28eqtrdi 2849 . 2 (((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) → ( bday 𝑍) = (dom 𝑆 ∪ suc ( bday 𝐵)))
30 imaundi 5975 . . . . . . 7 ( bday “ (𝐴𝐵)) = (( bday 𝐴) ∪ ( bday 𝐵))
3130unieqi 4813 . . . . . 6 ( bday “ (𝐴𝐵)) = (( bday 𝐴) ∪ ( bday 𝐵))
32 uniun 4823 . . . . . 6 (( bday 𝐴) ∪ ( bday 𝐵)) = ( ( bday 𝐴) ∪ ( bday 𝐵))
3331, 32eqtri 2821 . . . . 5 ( bday “ (𝐴𝐵)) = ( ( bday 𝐴) ∪ ( bday 𝐵))
34 suceq 6224 . . . . 5 ( ( bday “ (𝐴𝐵)) = ( ( bday 𝐴) ∪ ( bday 𝐵)) → suc ( bday “ (𝐴𝐵)) = suc ( ( bday 𝐴) ∪ ( bday 𝐵)))
3533, 34ax-mp 5 . . . 4 suc ( bday “ (𝐴𝐵)) = suc ( ( bday 𝐴) ∪ ( bday 𝐵))
36 imassrn 5907 . . . . . . 7 ( bday 𝐴) ⊆ ran bday
37 bdayfo 33307 . . . . . . . 8 bday : No onto→On
38 forn 6568 . . . . . . . 8 ( bday : No onto→On → ran bday = On)
3937, 38ax-mp 5 . . . . . . 7 ran bday = On
4036, 39sseqtri 3951 . . . . . 6 ( bday 𝐴) ⊆ On
41 ssorduni 7482 . . . . . 6 (( bday 𝐴) ⊆ On → Ord ( bday 𝐴))
4240, 41ax-mp 5 . . . . 5 Ord ( bday 𝐴)
43 imassrn 5907 . . . . . . 7 ( bday 𝐵) ⊆ ran bday
4443, 39sseqtri 3951 . . . . . 6 ( bday 𝐵) ⊆ On
45 ssorduni 7482 . . . . . 6 (( bday 𝐵) ⊆ On → Ord ( bday 𝐵))
4644, 45ax-mp 5 . . . . 5 Ord ( bday 𝐵)
47 ordsucun 7522 . . . . 5 ((Ord ( bday 𝐴) ∧ Ord ( bday 𝐵)) → suc ( ( bday 𝐴) ∪ ( bday 𝐵)) = (suc ( bday 𝐴) ∪ suc ( bday 𝐵)))
4842, 46, 47mp2an 691 . . . 4 suc ( ( bday 𝐴) ∪ ( bday 𝐵)) = (suc ( bday 𝐴) ∪ suc ( bday 𝐵))
4935, 48eqtri 2821 . . 3 suc ( bday “ (𝐴𝐵)) = (suc ( bday 𝐴) ∪ suc ( bday 𝐵))
5049a1i 11 . 2 (((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) → suc ( bday “ (𝐴𝐵)) = (suc ( bday 𝐴) ∪ suc ( bday 𝐵)))
519, 29, 503sstr4d 3962 1 (((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) → ( bday 𝑍) ⊆ suc ( bday “ (𝐴𝐵)))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 399   ∧ w3a 1084   = wceq 1538   ∈ wcel 2111  {cab 2776   ≠ wne 2987  ∀wral 3106  ∃wrex 3107  Vcvv 3441   ∖ cdif 3878   ∪ cun 3879   ⊆ wss 3881  ∅c0 4243  ifcif 4425  {csn 4525  ⟨cop 4531  ∪ cuni 4800   class class class wbr 5030   ↦ cmpt 5110   × cxp 5517  dom cdm 5519  ran crn 5520   ↾ cres 5521   “ cima 5522  Ord word 6158  Oncon0 6159  suc csuc 6161  ℩cio 6281  –onto→wfo 6322  ‘cfv 6324  ℩crio 7092  1oc1o 8080  2oc2o 8081   No csur 33272
 Copyright terms: Public domain W3C validator