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

Theorem oldlim 33660
 Description: The value of the old set at a limit ordinal. (Contributed by Scott Fenton, 8-Aug-2024.)
Assertion
Ref Expression
oldlim ((Lim 𝐴𝐴𝑉) → ( O ‘𝐴) = ( O “ 𝐴))

Proof of Theorem oldlim
Dummy variables 𝑥 𝑏 𝑐 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simprl 770 . . . . . . . . 9 (((Lim 𝐴𝐴𝑉) ∧ (𝑐𝐴𝑥 ∈ ( M ‘𝑐))) → 𝑐𝐴)
2 limsuc 7569 . . . . . . . . . 10 (Lim 𝐴 → (𝑐𝐴 ↔ suc 𝑐𝐴))
32ad2antrr 725 . . . . . . . . 9 (((Lim 𝐴𝐴𝑉) ∧ (𝑐𝐴𝑥 ∈ ( M ‘𝑐))) → (𝑐𝐴 ↔ suc 𝑐𝐴))
41, 3mpbid 235 . . . . . . . 8 (((Lim 𝐴𝐴𝑉) ∧ (𝑐𝐴𝑥 ∈ ( M ‘𝑐))) → suc 𝑐𝐴)
5 simprr 772 . . . . . . . . 9 (((Lim 𝐴𝐴𝑉) ∧ (𝑐𝐴𝑥 ∈ ( M ‘𝑐))) → 𝑥 ∈ ( M ‘𝑐))
6 limord 6233 . . . . . . . . . . . . 13 (Lim 𝐴 → Ord 𝐴)
7 elex 3428 . . . . . . . . . . . . 13 (𝐴𝑉𝐴 ∈ V)
86, 7anim12i 615 . . . . . . . . . . . 12 ((Lim 𝐴𝐴𝑉) → (Ord 𝐴𝐴 ∈ V))
9 elon2 6185 . . . . . . . . . . . 12 (𝐴 ∈ On ↔ (Ord 𝐴𝐴 ∈ V))
108, 9sylibr 237 . . . . . . . . . . 11 ((Lim 𝐴𝐴𝑉) → 𝐴 ∈ On)
11 onelon 6199 . . . . . . . . . . 11 ((𝐴 ∈ On ∧ 𝑐𝐴) → 𝑐 ∈ On)
1210, 1, 11syl2an2r 684 . . . . . . . . . 10 (((Lim 𝐴𝐴𝑉) ∧ (𝑐𝐴𝑥 ∈ ( M ‘𝑐))) → 𝑐 ∈ On)
13 madeoldsuc 33658 . . . . . . . . . 10 (𝑐 ∈ On → ( M ‘𝑐) = ( O ‘suc 𝑐))
1412, 13syl 17 . . . . . . . . 9 (((Lim 𝐴𝐴𝑉) ∧ (𝑐𝐴𝑥 ∈ ( M ‘𝑐))) → ( M ‘𝑐) = ( O ‘suc 𝑐))
155, 14eleqtrd 2854 . . . . . . . 8 (((Lim 𝐴𝐴𝑉) ∧ (𝑐𝐴𝑥 ∈ ( M ‘𝑐))) → 𝑥 ∈ ( O ‘suc 𝑐))
16 fveq2 6663 . . . . . . . . . 10 (𝑏 = suc 𝑐 → ( O ‘𝑏) = ( O ‘suc 𝑐))
1716eleq2d 2837 . . . . . . . . 9 (𝑏 = suc 𝑐 → (𝑥 ∈ ( O ‘𝑏) ↔ 𝑥 ∈ ( O ‘suc 𝑐)))
1817rspcev 3543 . . . . . . . 8 ((suc 𝑐𝐴𝑥 ∈ ( O ‘suc 𝑐)) → ∃𝑏𝐴 𝑥 ∈ ( O ‘𝑏))
194, 15, 18syl2anc 587 . . . . . . 7 (((Lim 𝐴𝐴𝑉) ∧ (𝑐𝐴𝑥 ∈ ( M ‘𝑐))) → ∃𝑏𝐴 𝑥 ∈ ( O ‘𝑏))
2019expr 460 . . . . . 6 (((Lim 𝐴𝐴𝑉) ∧ 𝑐𝐴) → (𝑥 ∈ ( M ‘𝑐) → ∃𝑏𝐴 𝑥 ∈ ( O ‘𝑏)))
2120rexlimdva 3208 . . . . 5 ((Lim 𝐴𝐴𝑉) → (∃𝑐𝐴 𝑥 ∈ ( M ‘𝑐) → ∃𝑏𝐴 𝑥 ∈ ( O ‘𝑏)))
22 simprl 770 . . . . . . . 8 (((Lim 𝐴𝐴𝑉) ∧ (𝑏𝐴𝑥 ∈ ( O ‘𝑏))) → 𝑏𝐴)
23 onelon 6199 . . . . . . . . . . 11 ((𝐴 ∈ On ∧ 𝑏𝐴) → 𝑏 ∈ On)
2410, 22, 23syl2an2r 684 . . . . . . . . . 10 (((Lim 𝐴𝐴𝑉) ∧ (𝑏𝐴𝑥 ∈ ( O ‘𝑏))) → 𝑏 ∈ On)
25 oldssmade 33651 . . . . . . . . . 10 (𝑏 ∈ On → ( O ‘𝑏) ⊆ ( M ‘𝑏))
2624, 25syl 17 . . . . . . . . 9 (((Lim 𝐴𝐴𝑉) ∧ (𝑏𝐴𝑥 ∈ ( O ‘𝑏))) → ( O ‘𝑏) ⊆ ( M ‘𝑏))
27 simprr 772 . . . . . . . . 9 (((Lim 𝐴𝐴𝑉) ∧ (𝑏𝐴𝑥 ∈ ( O ‘𝑏))) → 𝑥 ∈ ( O ‘𝑏))
2826, 27sseldd 3895 . . . . . . . 8 (((Lim 𝐴𝐴𝑉) ∧ (𝑏𝐴𝑥 ∈ ( O ‘𝑏))) → 𝑥 ∈ ( M ‘𝑏))
29 fveq2 6663 . . . . . . . . . 10 (𝑐 = 𝑏 → ( M ‘𝑐) = ( M ‘𝑏))
3029eleq2d 2837 . . . . . . . . 9 (𝑐 = 𝑏 → (𝑥 ∈ ( M ‘𝑐) ↔ 𝑥 ∈ ( M ‘𝑏)))
3130rspcev 3543 . . . . . . . 8 ((𝑏𝐴𝑥 ∈ ( M ‘𝑏)) → ∃𝑐𝐴 𝑥 ∈ ( M ‘𝑐))
3222, 28, 31syl2anc 587 . . . . . . 7 (((Lim 𝐴𝐴𝑉) ∧ (𝑏𝐴𝑥 ∈ ( O ‘𝑏))) → ∃𝑐𝐴 𝑥 ∈ ( M ‘𝑐))
3332expr 460 . . . . . 6 (((Lim 𝐴𝐴𝑉) ∧ 𝑏𝐴) → (𝑥 ∈ ( O ‘𝑏) → ∃𝑐𝐴 𝑥 ∈ ( M ‘𝑐)))
3433rexlimdva 3208 . . . . 5 ((Lim 𝐴𝐴𝑉) → (∃𝑏𝐴 𝑥 ∈ ( O ‘𝑏) → ∃𝑐𝐴 𝑥 ∈ ( M ‘𝑐)))
3521, 34impbid 215 . . . 4 ((Lim 𝐴𝐴𝑉) → (∃𝑐𝐴 𝑥 ∈ ( M ‘𝑐) ↔ ∃𝑏𝐴 𝑥 ∈ ( O ‘𝑏)))
36 elold 33643 . . . . 5 (𝐴 ∈ On → (𝑥 ∈ ( O ‘𝐴) ↔ ∃𝑐𝐴 𝑥 ∈ ( M ‘𝑐)))
3710, 36syl 17 . . . 4 ((Lim 𝐴𝐴𝑉) → (𝑥 ∈ ( O ‘𝐴) ↔ ∃𝑐𝐴 𝑥 ∈ ( M ‘𝑐)))
38 eliun 4890 . . . . 5 (𝑥 𝑏𝐴 ( O ‘𝑏) ↔ ∃𝑏𝐴 𝑥 ∈ ( O ‘𝑏))
3938a1i 11 . . . 4 ((Lim 𝐴𝐴𝑉) → (𝑥 𝑏𝐴 ( O ‘𝑏) ↔ ∃𝑏𝐴 𝑥 ∈ ( O ‘𝑏)))
4035, 37, 393bitr4d 314 . . 3 ((Lim 𝐴𝐴𝑉) → (𝑥 ∈ ( O ‘𝐴) ↔ 𝑥 𝑏𝐴 ( O ‘𝑏)))
4140eqrdv 2756 . 2 ((Lim 𝐴𝐴𝑉) → ( O ‘𝐴) = 𝑏𝐴 ( O ‘𝑏))
42 oldf 33635 . . 3 O :On⟶𝒫 No
43 ffun 6506 . . 3 ( O :On⟶𝒫 No → Fun O )
44 funiunfv 7005 . . 3 (Fun O → 𝑏𝐴 ( O ‘𝑏) = ( O “ 𝐴))
4542, 43, 44mp2b 10 . 2 𝑏𝐴 ( O ‘𝑏) = ( O “ 𝐴)
4641, 45eqtrdi 2809 1 ((Lim 𝐴𝐴𝑉) → ( O ‘𝐴) = ( O “ 𝐴))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538   ∈ wcel 2111  ∃wrex 3071  Vcvv 3409   ⊆ wss 3860  𝒫 cpw 4497  ∪ cuni 4801  ∪ ciun 4886   “ cima 5531  Ord word 6173  Oncon0 6174  Lim wlim 6175  suc csuc 6176  Fun wfun 6334  ⟶wf 6336  ‘cfv 6340   No csur 33440   M cmade 33620   O cold 33621 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-rep 5160  ax-sep 5173  ax-nul 5180  ax-pow 5238  ax-pr 5302  ax-un 7465 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ne 2952  df-ral 3075  df-rex 3076  df-reu 3077  df-rmo 3078  df-rab 3079  df-v 3411  df-sbc 3699  df-csb 3808  df-dif 3863  df-un 3865  df-in 3867  df-ss 3877  df-pss 3879  df-nul 4228  df-if 4424  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4802  df-int 4842  df-iun 4888  df-br 5037  df-opab 5099  df-mpt 5117  df-tr 5143  df-id 5434  df-eprel 5439  df-po 5447  df-so 5448  df-fr 5487  df-we 5489  df-xp 5534  df-rel 5535  df-cnv 5536  df-co 5537  df-dm 5538  df-rn 5539  df-res 5540  df-ima 5541  df-pred 6131  df-ord 6177  df-on 6178  df-lim 6179  df-suc 6180  df-iota 6299  df-fun 6342  df-fn 6343  df-f 6344  df-f1 6345  df-fo 6346  df-f1o 6347  df-fv 6348  df-riota 7114  df-ov 7159  df-oprab 7160  df-mpo 7161  df-wrecs 7963  df-recs 8024  df-1o 8118  df-2o 8119  df-no 33443  df-slt 33444  df-bday 33445  df-sslt 33573  df-scut 33575  df-made 33625  df-old 33626 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator