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

Theorem addsbdaylem 28069
Description: Lemma for addsbday 28070. (Contributed by Scott Fenton, 13-Aug-2025.)
Hypotheses
Ref Expression
addsbdaylem.1 (𝜑𝐴 No )
addsbdaylem.2 (𝜑 → ∀𝑦𝑂 ∈ (( L ‘𝐵) ∪ ( R ‘𝐵))( bday ‘(𝐴 +s 𝑦𝑂)) ⊆ (( bday 𝐴) +no ( bday 𝑦𝑂)))
addsbdaylem.3 𝑆 ⊆ (( L ‘𝐵) ∪ ( R ‘𝐵))
Assertion
Ref Expression
addsbdaylem (𝜑 → ( bday “ {𝑧 ∣ ∃𝑦𝐿𝑆 𝑧 = (𝐴 +s 𝑦𝐿)}) ⊆ (( bday 𝐴) +no ( bday 𝐵)))
Distinct variable groups:   𝐴,𝑦𝑂,𝑦𝐿,𝑧   𝐵,𝑦𝑂,𝑦𝐿,𝑧   𝜑,𝑦𝐿,𝑧   𝑧,𝑆
Allowed substitution hints:   𝜑(𝑦𝑂)   𝑆(𝑦𝑂,𝑦𝐿)

Proof of Theorem addsbdaylem
Dummy variable 𝑤 is distinct from all other variables.
StepHypRef Expression
1 oveq2 7458 . . . . . . . . . 10 (𝑦𝑂 = 𝑦𝐿 → (𝐴 +s 𝑦𝑂) = (𝐴 +s 𝑦𝐿))
21fveq2d 6926 . . . . . . . . 9 (𝑦𝑂 = 𝑦𝐿 → ( bday ‘(𝐴 +s 𝑦𝑂)) = ( bday ‘(𝐴 +s 𝑦𝐿)))
3 fveq2 6922 . . . . . . . . . 10 (𝑦𝑂 = 𝑦𝐿 → ( bday 𝑦𝑂) = ( bday 𝑦𝐿))
43oveq2d 7466 . . . . . . . . 9 (𝑦𝑂 = 𝑦𝐿 → (( bday 𝐴) +no ( bday 𝑦𝑂)) = (( bday 𝐴) +no ( bday 𝑦𝐿)))
52, 4sseq12d 4042 . . . . . . . 8 (𝑦𝑂 = 𝑦𝐿 → (( bday ‘(𝐴 +s 𝑦𝑂)) ⊆ (( bday 𝐴) +no ( bday 𝑦𝑂)) ↔ ( bday ‘(𝐴 +s 𝑦𝐿)) ⊆ (( bday 𝐴) +no ( bday 𝑦𝐿))))
6 addsbdaylem.2 . . . . . . . . 9 (𝜑 → ∀𝑦𝑂 ∈ (( L ‘𝐵) ∪ ( R ‘𝐵))( bday ‘(𝐴 +s 𝑦𝑂)) ⊆ (( bday 𝐴) +no ( bday 𝑦𝑂)))
76adantr 480 . . . . . . . 8 ((𝜑𝑦𝐿𝑆) → ∀𝑦𝑂 ∈ (( L ‘𝐵) ∪ ( R ‘𝐵))( bday ‘(𝐴 +s 𝑦𝑂)) ⊆ (( bday 𝐴) +no ( bday 𝑦𝑂)))
8 addsbdaylem.3 . . . . . . . . . 10 𝑆 ⊆ (( L ‘𝐵) ∪ ( R ‘𝐵))
98sseli 4004 . . . . . . . . 9 (𝑦𝐿𝑆𝑦𝐿 ∈ (( L ‘𝐵) ∪ ( R ‘𝐵)))
109adantl 481 . . . . . . . 8 ((𝜑𝑦𝐿𝑆) → 𝑦𝐿 ∈ (( L ‘𝐵) ∪ ( R ‘𝐵)))
115, 7, 10rspcdva 3636 . . . . . . 7 ((𝜑𝑦𝐿𝑆) → ( bday ‘(𝐴 +s 𝑦𝐿)) ⊆ (( bday 𝐴) +no ( bday 𝑦𝐿)))
12 lrold 27955 . . . . . . . . . . . 12 (( L ‘𝐵) ∪ ( R ‘𝐵)) = ( O ‘( bday 𝐵))
138, 12sseqtri 4045 . . . . . . . . . . 11 𝑆 ⊆ ( O ‘( bday 𝐵))
1413sseli 4004 . . . . . . . . . 10 (𝑦𝐿𝑆𝑦𝐿 ∈ ( O ‘( bday 𝐵)))
15 oldbdayim 27947 . . . . . . . . . 10 (𝑦𝐿 ∈ ( O ‘( bday 𝐵)) → ( bday 𝑦𝐿) ∈ ( bday 𝐵))
1614, 15syl 17 . . . . . . . . 9 (𝑦𝐿𝑆 → ( bday 𝑦𝐿) ∈ ( bday 𝐵))
1716adantl 481 . . . . . . . 8 ((𝜑𝑦𝐿𝑆) → ( bday 𝑦𝐿) ∈ ( bday 𝐵))
18 bdayelon 27841 . . . . . . . . 9 ( bday 𝑦𝐿) ∈ On
19 bdayelon 27841 . . . . . . . . 9 ( bday 𝐵) ∈ On
20 bdayelon 27841 . . . . . . . . 9 ( bday 𝐴) ∈ On
21 naddel2 8746 . . . . . . . . 9 ((( bday 𝑦𝐿) ∈ On ∧ ( bday 𝐵) ∈ On ∧ ( bday 𝐴) ∈ On) → (( bday 𝑦𝐿) ∈ ( bday 𝐵) ↔ (( bday 𝐴) +no ( bday 𝑦𝐿)) ∈ (( bday 𝐴) +no ( bday 𝐵))))
2218, 19, 20, 21mp3an 1461 . . . . . . . 8 (( bday 𝑦𝐿) ∈ ( bday 𝐵) ↔ (( bday 𝐴) +no ( bday 𝑦𝐿)) ∈ (( bday 𝐴) +no ( bday 𝐵)))
2317, 22sylib 218 . . . . . . 7 ((𝜑𝑦𝐿𝑆) → (( bday 𝐴) +no ( bday 𝑦𝐿)) ∈ (( bday 𝐴) +no ( bday 𝐵)))
24 bdayelon 27841 . . . . . . . 8 ( bday ‘(𝐴 +s 𝑦𝐿)) ∈ On
25 naddcl 8735 . . . . . . . . 9 ((( bday 𝐴) ∈ On ∧ ( bday 𝐵) ∈ On) → (( bday 𝐴) +no ( bday 𝐵)) ∈ On)
2620, 19, 25mp2an 691 . . . . . . . 8 (( bday 𝐴) +no ( bday 𝐵)) ∈ On
27 ontr2 6444 . . . . . . . 8 ((( bday ‘(𝐴 +s 𝑦𝐿)) ∈ On ∧ (( bday 𝐴) +no ( bday 𝐵)) ∈ On) → ((( bday ‘(𝐴 +s 𝑦𝐿)) ⊆ (( bday 𝐴) +no ( bday 𝑦𝐿)) ∧ (( bday 𝐴) +no ( bday 𝑦𝐿)) ∈ (( bday 𝐴) +no ( bday 𝐵))) → ( bday ‘(𝐴 +s 𝑦𝐿)) ∈ (( bday 𝐴) +no ( bday 𝐵))))
2824, 26, 27mp2an 691 . . . . . . 7 ((( bday ‘(𝐴 +s 𝑦𝐿)) ⊆ (( bday 𝐴) +no ( bday 𝑦𝐿)) ∧ (( bday 𝐴) +no ( bday 𝑦𝐿)) ∈ (( bday 𝐴) +no ( bday 𝐵))) → ( bday ‘(𝐴 +s 𝑦𝐿)) ∈ (( bday 𝐴) +no ( bday 𝐵)))
2911, 23, 28syl2anc 583 . . . . . 6 ((𝜑𝑦𝐿𝑆) → ( bday ‘(𝐴 +s 𝑦𝐿)) ∈ (( bday 𝐴) +no ( bday 𝐵)))
30 fveq2 6922 . . . . . . 7 (𝑤 = (𝐴 +s 𝑦𝐿) → ( bday 𝑤) = ( bday ‘(𝐴 +s 𝑦𝐿)))
3130eleq1d 2829 . . . . . 6 (𝑤 = (𝐴 +s 𝑦𝐿) → (( bday 𝑤) ∈ (( bday 𝐴) +no ( bday 𝐵)) ↔ ( bday ‘(𝐴 +s 𝑦𝐿)) ∈ (( bday 𝐴) +no ( bday 𝐵))))
3229, 31syl5ibrcom 247 . . . . 5 ((𝜑𝑦𝐿𝑆) → (𝑤 = (𝐴 +s 𝑦𝐿) → ( bday 𝑤) ∈ (( bday 𝐴) +no ( bday 𝐵))))
3332rexlimdva 3161 . . . 4 (𝜑 → (∃𝑦𝐿𝑆 𝑤 = (𝐴 +s 𝑦𝐿) → ( bday 𝑤) ∈ (( bday 𝐴) +no ( bday 𝐵))))
3433alrimiv 1926 . . 3 (𝜑 → ∀𝑤(∃𝑦𝐿𝑆 𝑤 = (𝐴 +s 𝑦𝐿) → ( bday 𝑤) ∈ (( bday 𝐴) +no ( bday 𝐵))))
35 eqeq1 2744 . . . . 5 (𝑧 = 𝑤 → (𝑧 = (𝐴 +s 𝑦𝐿) ↔ 𝑤 = (𝐴 +s 𝑦𝐿)))
3635rexbidv 3185 . . . 4 (𝑧 = 𝑤 → (∃𝑦𝐿𝑆 𝑧 = (𝐴 +s 𝑦𝐿) ↔ ∃𝑦𝐿𝑆 𝑤 = (𝐴 +s 𝑦𝐿)))
3736ralab 3713 . . 3 (∀𝑤 ∈ {𝑧 ∣ ∃𝑦𝐿𝑆 𝑧 = (𝐴 +s 𝑦𝐿)} ( bday 𝑤) ∈ (( bday 𝐴) +no ( bday 𝐵)) ↔ ∀𝑤(∃𝑦𝐿𝑆 𝑤 = (𝐴 +s 𝑦𝐿) → ( bday 𝑤) ∈ (( bday 𝐴) +no ( bday 𝐵))))
3834, 37sylibr 234 . 2 (𝜑 → ∀𝑤 ∈ {𝑧 ∣ ∃𝑦𝐿𝑆 𝑧 = (𝐴 +s 𝑦𝐿)} ( bday 𝑤) ∈ (( bday 𝐴) +no ( bday 𝐵)))
39 bdayfun 27837 . . 3 Fun bday
40 addsbdaylem.1 . . . . . . . . 9 (𝜑𝐴 No )
4140adantr 480 . . . . . . . 8 ((𝜑𝑦𝐿𝑆) → 𝐴 No )
42 leftssno 27939 . . . . . . . . . . . 12 ( L ‘𝐵) ⊆ No
43 rightssno 27940 . . . . . . . . . . . 12 ( R ‘𝐵) ⊆ No
4442, 43unssi 4214 . . . . . . . . . . 11 (( L ‘𝐵) ∪ ( R ‘𝐵)) ⊆ No
458, 44sstri 4018 . . . . . . . . . 10 𝑆 No
4645sseli 4004 . . . . . . . . 9 (𝑦𝐿𝑆𝑦𝐿 No )
4746adantl 481 . . . . . . . 8 ((𝜑𝑦𝐿𝑆) → 𝑦𝐿 No )
4841, 47addscld 28033 . . . . . . 7 ((𝜑𝑦𝐿𝑆) → (𝐴 +s 𝑦𝐿) ∈ No )
49 eleq1 2832 . . . . . . 7 (𝑧 = (𝐴 +s 𝑦𝐿) → (𝑧 No ↔ (𝐴 +s 𝑦𝐿) ∈ No ))
5048, 49syl5ibrcom 247 . . . . . 6 ((𝜑𝑦𝐿𝑆) → (𝑧 = (𝐴 +s 𝑦𝐿) → 𝑧 No ))
5150rexlimdva 3161 . . . . 5 (𝜑 → (∃𝑦𝐿𝑆 𝑧 = (𝐴 +s 𝑦𝐿) → 𝑧 No ))
5251abssdv 4091 . . . 4 (𝜑 → {𝑧 ∣ ∃𝑦𝐿𝑆 𝑧 = (𝐴 +s 𝑦𝐿)} ⊆ No )
53 bdaydm 27839 . . . 4 dom bday = No
5452, 53sseqtrrdi 4060 . . 3 (𝜑 → {𝑧 ∣ ∃𝑦𝐿𝑆 𝑧 = (𝐴 +s 𝑦𝐿)} ⊆ dom bday )
55 funimass4 6988 . . 3 ((Fun bday ∧ {𝑧 ∣ ∃𝑦𝐿𝑆 𝑧 = (𝐴 +s 𝑦𝐿)} ⊆ dom bday ) → (( bday “ {𝑧 ∣ ∃𝑦𝐿𝑆 𝑧 = (𝐴 +s 𝑦𝐿)}) ⊆ (( bday 𝐴) +no ( bday 𝐵)) ↔ ∀𝑤 ∈ {𝑧 ∣ ∃𝑦𝐿𝑆 𝑧 = (𝐴 +s 𝑦𝐿)} ( bday 𝑤) ∈ (( bday 𝐴) +no ( bday 𝐵))))
5639, 54, 55sylancr 586 . 2 (𝜑 → (( bday “ {𝑧 ∣ ∃𝑦𝐿𝑆 𝑧 = (𝐴 +s 𝑦𝐿)}) ⊆ (( bday 𝐴) +no ( bday 𝐵)) ↔ ∀𝑤 ∈ {𝑧 ∣ ∃𝑦𝐿𝑆 𝑧 = (𝐴 +s 𝑦𝐿)} ( bday 𝑤) ∈ (( bday 𝐴) +no ( bday 𝐵))))
5738, 56mpbird 257 1 (𝜑 → ( bday “ {𝑧 ∣ ∃𝑦𝐿𝑆 𝑧 = (𝐴 +s 𝑦𝐿)}) ⊆ (( bday 𝐴) +no ( bday 𝐵)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  wal 1535   = wceq 1537  wcel 2108  {cab 2717  wral 3067  wrex 3076  cun 3974  wss 3976  dom cdm 5700  cima 5703  Oncon0 6397  Fun wfun 6569  cfv 6575  (class class class)co 7450   +no cnadd 8723   No csur 27704   bday cbday 27706   O cold 27902   L cleft 27904   R cright 27905   +s cadds 28012
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-rep 5303  ax-sep 5317  ax-nul 5324  ax-pow 5383  ax-pr 5447  ax-un 7772
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-ral 3068  df-rex 3077  df-rmo 3388  df-reu 3389  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-pss 3996  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-tp 4653  df-op 4655  df-uni 4932  df-int 4971  df-iun 5017  df-br 5167  df-opab 5229  df-mpt 5250  df-tr 5284  df-id 5593  df-eprel 5599  df-po 5607  df-so 5608  df-fr 5652  df-se 5653  df-we 5654  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-pred 6334  df-ord 6400  df-on 6401  df-suc 6403  df-iota 6527  df-fun 6577  df-fn 6578  df-f 6579  df-f1 6580  df-fo 6581  df-f1o 6582  df-fv 6583  df-riota 7406  df-ov 7453  df-oprab 7454  df-mpo 7455  df-1st 8032  df-2nd 8033  df-frecs 8324  df-wrecs 8355  df-recs 8429  df-1o 8524  df-2o 8525  df-nadd 8724  df-no 27707  df-slt 27708  df-bday 27709  df-sslt 27846  df-scut 27848  df-0s 27889  df-made 27906  df-old 27907  df-left 27909  df-right 27910  df-norec2 28002  df-adds 28013
This theorem is referenced by:  addsbday  28070
  Copyright terms: Public domain W3C validator