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

Theorem smobeth 10523
Description: The beth function is strictly monotone. This function is not strictly the beth function, but rather bethA is the same as (cardβ€˜(𝑅1β€˜(Ο‰ +o 𝐴))), since conventionally we start counting at the first infinite level, and ignore the finite levels. (Contributed by Mario Carneiro, 6-Jun-2013.) (Revised by Mario Carneiro, 2-Jun-2015.)
Assertion
Ref Expression
smobeth Smo (card ∘ 𝑅1)

Proof of Theorem smobeth
Dummy variables π‘₯ 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 cardf2 9880 . . . . . . 7 card:{π‘₯ ∣ βˆƒπ‘¦ ∈ On 𝑦 β‰ˆ π‘₯}⟢On
2 ffun 6672 . . . . . . 7 (card:{π‘₯ ∣ βˆƒπ‘¦ ∈ On 𝑦 β‰ˆ π‘₯}⟢On β†’ Fun card)
31, 2ax-mp 5 . . . . . 6 Fun card
4 r1fnon 9704 . . . . . . 7 𝑅1 Fn On
5 fnfun 6603 . . . . . . 7 (𝑅1 Fn On β†’ Fun 𝑅1)
64, 5ax-mp 5 . . . . . 6 Fun 𝑅1
7 funco 6542 . . . . . 6 ((Fun card ∧ Fun 𝑅1) β†’ Fun (card ∘ 𝑅1))
83, 6, 7mp2an 691 . . . . 5 Fun (card ∘ 𝑅1)
9 funfn 6532 . . . . 5 (Fun (card ∘ 𝑅1) ↔ (card ∘ 𝑅1) Fn dom (card ∘ 𝑅1))
108, 9mpbi 229 . . . 4 (card ∘ 𝑅1) Fn dom (card ∘ 𝑅1)
11 rnco 6205 . . . . 5 ran (card ∘ 𝑅1) = ran (card β†Ύ ran 𝑅1)
12 resss 5963 . . . . . . 7 (card β†Ύ ran 𝑅1) βŠ† card
1312rnssi 5896 . . . . . 6 ran (card β†Ύ ran 𝑅1) βŠ† ran card
14 frn 6676 . . . . . . 7 (card:{π‘₯ ∣ βˆƒπ‘¦ ∈ On 𝑦 β‰ˆ π‘₯}⟢On β†’ ran card βŠ† On)
151, 14ax-mp 5 . . . . . 6 ran card βŠ† On
1613, 15sstri 3954 . . . . 5 ran (card β†Ύ ran 𝑅1) βŠ† On
1711, 16eqsstri 3979 . . . 4 ran (card ∘ 𝑅1) βŠ† On
18 df-f 6501 . . . 4 ((card ∘ 𝑅1):dom (card ∘ 𝑅1)⟢On ↔ ((card ∘ 𝑅1) Fn dom (card ∘ 𝑅1) ∧ ran (card ∘ 𝑅1) βŠ† On))
1910, 17, 18mpbir2an 710 . . 3 (card ∘ 𝑅1):dom (card ∘ 𝑅1)⟢On
20 dmco 6207 . . . 4 dom (card ∘ 𝑅1) = (◑𝑅1 β€œ dom card)
2120feq2i 6661 . . 3 ((card ∘ 𝑅1):dom (card ∘ 𝑅1)⟢On ↔ (card ∘ 𝑅1):(◑𝑅1 β€œ dom card)⟢On)
2219, 21mpbi 229 . 2 (card ∘ 𝑅1):(◑𝑅1 β€œ dom card)⟢On
23 elpreima 7009 . . . . . . . . 9 (𝑅1 Fn On β†’ (π‘₯ ∈ (◑𝑅1 β€œ dom card) ↔ (π‘₯ ∈ On ∧ (𝑅1β€˜π‘₯) ∈ dom card)))
244, 23ax-mp 5 . . . . . . . 8 (π‘₯ ∈ (◑𝑅1 β€œ dom card) ↔ (π‘₯ ∈ On ∧ (𝑅1β€˜π‘₯) ∈ dom card))
2524simplbi 499 . . . . . . 7 (π‘₯ ∈ (◑𝑅1 β€œ dom card) β†’ π‘₯ ∈ On)
26 onelon 6343 . . . . . . 7 ((π‘₯ ∈ On ∧ 𝑦 ∈ π‘₯) β†’ 𝑦 ∈ On)
2725, 26sylan 581 . . . . . 6 ((π‘₯ ∈ (◑𝑅1 β€œ dom card) ∧ 𝑦 ∈ π‘₯) β†’ 𝑦 ∈ On)
2824simprbi 498 . . . . . . . 8 (π‘₯ ∈ (◑𝑅1 β€œ dom card) β†’ (𝑅1β€˜π‘₯) ∈ dom card)
2928adantr 482 . . . . . . 7 ((π‘₯ ∈ (◑𝑅1 β€œ dom card) ∧ 𝑦 ∈ π‘₯) β†’ (𝑅1β€˜π‘₯) ∈ dom card)
30 r1ord2 9718 . . . . . . . . 9 (π‘₯ ∈ On β†’ (𝑦 ∈ π‘₯ β†’ (𝑅1β€˜π‘¦) βŠ† (𝑅1β€˜π‘₯)))
3130imp 408 . . . . . . . 8 ((π‘₯ ∈ On ∧ 𝑦 ∈ π‘₯) β†’ (𝑅1β€˜π‘¦) βŠ† (𝑅1β€˜π‘₯))
3225, 31sylan 581 . . . . . . 7 ((π‘₯ ∈ (◑𝑅1 β€œ dom card) ∧ 𝑦 ∈ π‘₯) β†’ (𝑅1β€˜π‘¦) βŠ† (𝑅1β€˜π‘₯))
33 ssnum 9976 . . . . . . 7 (((𝑅1β€˜π‘₯) ∈ dom card ∧ (𝑅1β€˜π‘¦) βŠ† (𝑅1β€˜π‘₯)) β†’ (𝑅1β€˜π‘¦) ∈ dom card)
3429, 32, 33syl2anc 585 . . . . . 6 ((π‘₯ ∈ (◑𝑅1 β€œ dom card) ∧ 𝑦 ∈ π‘₯) β†’ (𝑅1β€˜π‘¦) ∈ dom card)
35 elpreima 7009 . . . . . . 7 (𝑅1 Fn On β†’ (𝑦 ∈ (◑𝑅1 β€œ dom card) ↔ (𝑦 ∈ On ∧ (𝑅1β€˜π‘¦) ∈ dom card)))
364, 35ax-mp 5 . . . . . 6 (𝑦 ∈ (◑𝑅1 β€œ dom card) ↔ (𝑦 ∈ On ∧ (𝑅1β€˜π‘¦) ∈ dom card))
3727, 34, 36sylanbrc 584 . . . . 5 ((π‘₯ ∈ (◑𝑅1 β€œ dom card) ∧ 𝑦 ∈ π‘₯) β†’ 𝑦 ∈ (◑𝑅1 β€œ dom card))
3837rgen2 3195 . . . 4 βˆ€π‘₯ ∈ (◑𝑅1 β€œ dom card)βˆ€π‘¦ ∈ π‘₯ 𝑦 ∈ (◑𝑅1 β€œ dom card)
39 dftr5 5227 . . . 4 (Tr (◑𝑅1 β€œ dom card) ↔ βˆ€π‘₯ ∈ (◑𝑅1 β€œ dom card)βˆ€π‘¦ ∈ π‘₯ 𝑦 ∈ (◑𝑅1 β€œ dom card))
4038, 39mpbir 230 . . 3 Tr (◑𝑅1 β€œ dom card)
41 cnvimass 6034 . . . . 5 (◑𝑅1 β€œ dom card) βŠ† dom 𝑅1
42 dffn2 6671 . . . . . . 7 (𝑅1 Fn On ↔ 𝑅1:On⟢V)
434, 42mpbi 229 . . . . . 6 𝑅1:On⟢V
4443fdmi 6681 . . . . 5 dom 𝑅1 = On
4541, 44sseqtri 3981 . . . 4 (◑𝑅1 β€œ dom card) βŠ† On
46 epweon 7710 . . . 4 E We On
47 wess 5621 . . . 4 ((◑𝑅1 β€œ dom card) βŠ† On β†’ ( E We On β†’ E We (◑𝑅1 β€œ dom card)))
4845, 46, 47mp2 9 . . 3 E We (◑𝑅1 β€œ dom card)
49 df-ord 6321 . . 3 (Ord (◑𝑅1 β€œ dom card) ↔ (Tr (◑𝑅1 β€œ dom card) ∧ E We (◑𝑅1 β€œ dom card)))
5040, 48, 49mpbir2an 710 . 2 Ord (◑𝑅1 β€œ dom card)
51 r1sdom 9711 . . . . . . 7 ((π‘₯ ∈ On ∧ 𝑦 ∈ π‘₯) β†’ (𝑅1β€˜π‘¦) β‰Ί (𝑅1β€˜π‘₯))
5225, 51sylan 581 . . . . . 6 ((π‘₯ ∈ (◑𝑅1 β€œ dom card) ∧ 𝑦 ∈ π‘₯) β†’ (𝑅1β€˜π‘¦) β‰Ί (𝑅1β€˜π‘₯))
53 cardsdom2 9925 . . . . . . 7 (((𝑅1β€˜π‘¦) ∈ dom card ∧ (𝑅1β€˜π‘₯) ∈ dom card) β†’ ((cardβ€˜(𝑅1β€˜π‘¦)) ∈ (cardβ€˜(𝑅1β€˜π‘₯)) ↔ (𝑅1β€˜π‘¦) β‰Ί (𝑅1β€˜π‘₯)))
5434, 29, 53syl2anc 585 . . . . . 6 ((π‘₯ ∈ (◑𝑅1 β€œ dom card) ∧ 𝑦 ∈ π‘₯) β†’ ((cardβ€˜(𝑅1β€˜π‘¦)) ∈ (cardβ€˜(𝑅1β€˜π‘₯)) ↔ (𝑅1β€˜π‘¦) β‰Ί (𝑅1β€˜π‘₯)))
5552, 54mpbird 257 . . . . 5 ((π‘₯ ∈ (◑𝑅1 β€œ dom card) ∧ 𝑦 ∈ π‘₯) β†’ (cardβ€˜(𝑅1β€˜π‘¦)) ∈ (cardβ€˜(𝑅1β€˜π‘₯)))
56 fvco2 6939 . . . . . 6 ((𝑅1 Fn On ∧ 𝑦 ∈ On) β†’ ((card ∘ 𝑅1)β€˜π‘¦) = (cardβ€˜(𝑅1β€˜π‘¦)))
574, 27, 56sylancr 588 . . . . 5 ((π‘₯ ∈ (◑𝑅1 β€œ dom card) ∧ 𝑦 ∈ π‘₯) β†’ ((card ∘ 𝑅1)β€˜π‘¦) = (cardβ€˜(𝑅1β€˜π‘¦)))
5825adantr 482 . . . . . 6 ((π‘₯ ∈ (◑𝑅1 β€œ dom card) ∧ 𝑦 ∈ π‘₯) β†’ π‘₯ ∈ On)
59 fvco2 6939 . . . . . 6 ((𝑅1 Fn On ∧ π‘₯ ∈ On) β†’ ((card ∘ 𝑅1)β€˜π‘₯) = (cardβ€˜(𝑅1β€˜π‘₯)))
604, 58, 59sylancr 588 . . . . 5 ((π‘₯ ∈ (◑𝑅1 β€œ dom card) ∧ 𝑦 ∈ π‘₯) β†’ ((card ∘ 𝑅1)β€˜π‘₯) = (cardβ€˜(𝑅1β€˜π‘₯)))
6155, 57, 603eltr4d 2853 . . . 4 ((π‘₯ ∈ (◑𝑅1 β€œ dom card) ∧ 𝑦 ∈ π‘₯) β†’ ((card ∘ 𝑅1)β€˜π‘¦) ∈ ((card ∘ 𝑅1)β€˜π‘₯))
6261ex 414 . . 3 (π‘₯ ∈ (◑𝑅1 β€œ dom card) β†’ (𝑦 ∈ π‘₯ β†’ ((card ∘ 𝑅1)β€˜π‘¦) ∈ ((card ∘ 𝑅1)β€˜π‘₯)))
6362adantl 483 . 2 ((𝑦 ∈ (◑𝑅1 β€œ dom card) ∧ π‘₯ ∈ (◑𝑅1 β€œ dom card)) β†’ (𝑦 ∈ π‘₯ β†’ ((card ∘ 𝑅1)β€˜π‘¦) ∈ ((card ∘ 𝑅1)β€˜π‘₯)))
6422, 50, 63, 20issmo 8295 1 Smo (card ∘ 𝑅1)
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 397   = wceq 1542   ∈ wcel 2107  {cab 2714  βˆ€wral 3065  βˆƒwrex 3074  Vcvv 3446   βŠ† wss 3911   class class class wbr 5106  Tr wtr 5223   E cep 5537   We wwe 5588  β—‘ccnv 5633  dom cdm 5634  ran crn 5635   β†Ύ cres 5636   β€œ cima 5637   ∘ ccom 5638  Ord word 6317  Oncon0 6318  Fun wfun 6491   Fn wfn 6492  βŸΆwf 6493  β€˜cfv 6497  Smo wsmo 8292   β‰ˆ cen 8881   β‰Ί csdm 8883  π‘…1cr1 9699  cardccrd 9872
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-rep 5243  ax-sep 5257  ax-nul 5264  ax-pow 5321  ax-pr 5385  ax-un 7673
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-ral 3066  df-rex 3075  df-rmo 3354  df-reu 3355  df-rab 3409  df-v 3448  df-sbc 3741  df-csb 3857  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3930  df-nul 4284  df-if 4488  df-pw 4563  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-int 4909  df-iun 4957  df-br 5107  df-opab 5169  df-mpt 5190  df-tr 5224  df-id 5532  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5589  df-se 5590  df-we 5591  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-pred 6254  df-ord 6321  df-on 6322  df-lim 6323  df-suc 6324  df-iota 6449  df-fun 6499  df-fn 6500  df-f 6501  df-f1 6502  df-fo 6503  df-f1o 6504  df-fv 6505  df-isom 6506  df-riota 7314  df-ov 7361  df-om 7804  df-2nd 7923  df-frecs 8213  df-wrecs 8244  df-smo 8293  df-recs 8318  df-rdg 8357  df-er 8649  df-en 8885  df-dom 8886  df-sdom 8887  df-r1 9701  df-card 9876
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator