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

Theorem noetalem4 32093
 Description: Lemma for noeta 32095. Bound the birthday of 𝑍 above. (Contributed by Scott Fenton, 6-Dec-2021.)
Hypotheses
Ref Expression
noetalem.1 𝑆 = if(∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦, ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2𝑜⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))))
noetalem.2 𝑍 = (𝑆 ∪ ((suc ( bday 𝐵) ∖ dom 𝑆) × {1𝑜}))
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 𝑦), 2𝑜⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))))
21nosupno 32076 . . . . . 6 ((𝐴 No 𝐴 ∈ V) → 𝑆 No )
3 bdayval 32028 . . . . . 6 (𝑆 No → ( bday 𝑆) = dom 𝑆)
42, 3syl 17 . . . . 5 ((𝐴 No 𝐴 ∈ V) → ( bday 𝑆) = dom 𝑆)
51nosupbday 32078 . . . . 5 ((𝐴 No 𝐴 ∈ V) → ( bday 𝑆) ⊆ suc ( bday 𝐴))
64, 5eqsstr3d 3746 . . . 4 ((𝐴 No 𝐴 ∈ V) → dom 𝑆 ⊆ suc ( bday 𝐴))
76adantr 472 . . 3 (((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) → dom 𝑆 ⊆ suc ( bday 𝐴))
8 unss1 3890 . . 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 807 . . . . 5 (((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) → 𝐴 No )
11 simplr 809 . . . . 5 (((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) → 𝐴 ∈ V)
12 simprr 813 . . . . 5 (((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) → 𝐵 ∈ V)
13 noetalem.2 . . . . . 6 𝑍 = (𝑆 ∪ ((suc ( bday 𝐵) ∖ dom 𝑆) × {1𝑜}))
141, 13noetalem1 32090 . . . . 5 ((𝐴 No 𝐴 ∈ V ∧ 𝐵 ∈ V) → 𝑍 No )
1510, 11, 12, 14syl3anc 1439 . . . 4 (((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) → 𝑍 No )
16 bdayval 32028 . . . 4 (𝑍 No → ( bday 𝑍) = dom 𝑍)
1715, 16syl 17 . . 3 (((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) → ( bday 𝑍) = dom 𝑍)
1813dmeqi 5432 . . . 4 dom 𝑍 = dom (𝑆 ∪ ((suc ( bday 𝐵) ∖ dom 𝑆) × {1𝑜}))
19 dmun 5438 . . . . 5 dom (𝑆 ∪ ((suc ( bday 𝐵) ∖ dom 𝑆) × {1𝑜})) = (dom 𝑆 ∪ dom ((suc ( bday 𝐵) ∖ dom 𝑆) × {1𝑜}))
20 1on 7687 . . . . . . . . . 10 1𝑜 ∈ On
2120elexi 3317 . . . . . . . . 9 1𝑜 ∈ V
2221snnz 4415 . . . . . . . 8 {1𝑜} ≠ ∅
23 dmxp 5451 . . . . . . . 8 ({1𝑜} ≠ ∅ → dom ((suc ( bday 𝐵) ∖ dom 𝑆) × {1𝑜}) = (suc ( bday 𝐵) ∖ dom 𝑆))
2422, 23ax-mp 5 . . . . . . 7 dom ((suc ( bday 𝐵) ∖ dom 𝑆) × {1𝑜}) = (suc ( bday 𝐵) ∖ dom 𝑆)
2524uneq2i 3872 . . . . . 6 (dom 𝑆 ∪ dom ((suc ( bday 𝐵) ∖ dom 𝑆) × {1𝑜})) = (dom 𝑆 ∪ (suc ( bday 𝐵) ∖ dom 𝑆))
26 undif2 4152 . . . . . 6 (dom 𝑆 ∪ (suc ( bday 𝐵) ∖ dom 𝑆)) = (dom 𝑆 ∪ suc ( bday 𝐵))
2725, 26eqtri 2746 . . . . 5 (dom 𝑆 ∪ dom ((suc ( bday 𝐵) ∖ dom 𝑆) × {1𝑜})) = (dom 𝑆 ∪ suc ( bday 𝐵))
2819, 27eqtri 2746 . . . 4 dom (𝑆 ∪ ((suc ( bday 𝐵) ∖ dom 𝑆) × {1𝑜})) = (dom 𝑆 ∪ suc ( bday 𝐵))
2918, 28eqtri 2746 . . 3 dom 𝑍 = (dom 𝑆 ∪ suc ( bday 𝐵))
3017, 29syl6eq 2774 . 2 (((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) → ( bday 𝑍) = (dom 𝑆 ∪ suc ( bday 𝐵)))
31 imaundi 5655 . . . . . . 7 ( bday “ (𝐴𝐵)) = (( bday 𝐴) ∪ ( bday 𝐵))
3231unieqi 4553 . . . . . 6 ( bday “ (𝐴𝐵)) = (( bday 𝐴) ∪ ( bday 𝐵))
33 uniun 4564 . . . . . 6 (( bday 𝐴) ∪ ( bday 𝐵)) = ( ( bday 𝐴) ∪ ( bday 𝐵))
3432, 33eqtri 2746 . . . . 5 ( bday “ (𝐴𝐵)) = ( ( bday 𝐴) ∪ ( bday 𝐵))
35 suceq 5903 . . . . 5 ( ( bday “ (𝐴𝐵)) = ( ( bday 𝐴) ∪ ( bday 𝐵)) → suc ( bday “ (𝐴𝐵)) = suc ( ( bday 𝐴) ∪ ( bday 𝐵)))
3634, 35ax-mp 5 . . . 4 suc ( bday “ (𝐴𝐵)) = suc ( ( bday 𝐴) ∪ ( bday 𝐵))
37 imassrn 5587 . . . . . . 7 ( bday 𝐴) ⊆ ran bday
38 bdayfo 32055 . . . . . . . 8 bday : No onto→On
39 forn 6231 . . . . . . . 8 ( bday : No onto→On → ran bday = On)
4038, 39ax-mp 5 . . . . . . 7 ran bday = On
4137, 40sseqtri 3743 . . . . . 6 ( bday 𝐴) ⊆ On
42 ssorduni 7102 . . . . . 6 (( bday 𝐴) ⊆ On → Ord ( bday 𝐴))
4341, 42ax-mp 5 . . . . 5 Ord ( bday 𝐴)
44 imassrn 5587 . . . . . . 7 ( bday 𝐵) ⊆ ran bday
4544, 40sseqtri 3743 . . . . . 6 ( bday 𝐵) ⊆ On
46 ssorduni 7102 . . . . . 6 (( bday 𝐵) ⊆ On → Ord ( bday 𝐵))
4745, 46ax-mp 5 . . . . 5 Ord ( bday 𝐵)
48 ordsucun 7142 . . . . 5 ((Ord ( bday 𝐴) ∧ Ord ( bday 𝐵)) → suc ( ( bday 𝐴) ∪ ( bday 𝐵)) = (suc ( bday 𝐴) ∪ suc ( bday 𝐵)))
4943, 47, 48mp2an 710 . . . 4 suc ( ( bday 𝐴) ∪ ( bday 𝐵)) = (suc ( bday 𝐴) ∪ suc ( bday 𝐵))
5036, 49eqtri 2746 . . 3 suc ( bday “ (𝐴𝐵)) = (suc ( bday 𝐴) ∪ suc ( bday 𝐵))
5150a1i 11 . 2 (((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) → suc ( bday “ (𝐴𝐵)) = (suc ( bday 𝐴) ∪ suc ( bday 𝐵)))
529, 30, 513sstr4d 3754 1 (((𝐴 No 𝐴 ∈ V) ∧ (𝐵 No 𝐵 ∈ V)) → ( bday 𝑍) ⊆ suc ( bday “ (𝐴𝐵)))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 383   ∧ w3a 1072   = wceq 1596   ∈ wcel 2103  {cab 2710   ≠ wne 2896  ∀wral 3014  ∃wrex 3015  Vcvv 3304   ∖ cdif 3677   ∪ cun 3678   ⊆ wss 3680  ∅c0 4023  ifcif 4194  {csn 4285  ⟨cop 4291  ∪ cuni 4544   class class class wbr 4760   ↦ cmpt 4837   × cxp 5216  dom cdm 5218  ran crn 5219   ↾ cres 5220   “ cima 5221  Ord word 5835  Oncon0 5836  suc csuc 5838  ℩cio 5962  –onto→wfo 5999  ‘cfv 6001  ℩crio 6725  1𝑜c1o 7673  2𝑜c2o 7674   No csur 32020
 Copyright terms: Public domain W3C validator