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

Theorem smobeth 10006
 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 9369 . . . . . . 7 card:{𝑥 ∣ ∃𝑦 ∈ On 𝑦𝑥}⟶On
2 ffun 6506 . . . . . . 7 (card:{𝑥 ∣ ∃𝑦 ∈ On 𝑦𝑥}⟶On → Fun card)
31, 2ax-mp 5 . . . . . 6 Fun card
4 r1fnon 9193 . . . . . . 7 𝑅1 Fn On
5 fnfun 6441 . . . . . . 7 (𝑅1 Fn On → Fun 𝑅1)
64, 5ax-mp 5 . . . . . 6 Fun 𝑅1
7 funco 6383 . . . . . 6 ((Fun card ∧ Fun 𝑅1) → Fun (card ∘ 𝑅1))
83, 6, 7mp2an 691 . . . . 5 Fun (card ∘ 𝑅1)
9 funfn 6373 . . . . 5 (Fun (card ∘ 𝑅1) ↔ (card ∘ 𝑅1) Fn dom (card ∘ 𝑅1))
108, 9mpbi 233 . . . 4 (card ∘ 𝑅1) Fn dom (card ∘ 𝑅1)
11 rnco 6092 . . . . 5 ran (card ∘ 𝑅1) = ran (card ↾ ran 𝑅1)
12 resss 5865 . . . . . . 7 (card ↾ ran 𝑅1) ⊆ card
1312rnssi 5797 . . . . . 6 ran (card ↾ ran 𝑅1) ⊆ ran card
14 frn 6509 . . . . . . 7 (card:{𝑥 ∣ ∃𝑦 ∈ On 𝑦𝑥}⟶On → ran card ⊆ On)
151, 14ax-mp 5 . . . . . 6 ran card ⊆ On
1613, 15sstri 3962 . . . . 5 ran (card ↾ ran 𝑅1) ⊆ On
1711, 16eqsstri 3987 . . . 4 ran (card ∘ 𝑅1) ⊆ On
18 df-f 6347 . . . 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 6094 . . . 4 dom (card ∘ 𝑅1) = (𝑅1 “ dom card)
2120feq2i 6495 . . 3 ((card ∘ 𝑅1):dom (card ∘ 𝑅1)⟶On ↔ (card ∘ 𝑅1):(𝑅1 “ dom card)⟶On)
2219, 21mpbi 233 . 2 (card ∘ 𝑅1):(𝑅1 “ dom card)⟶On
23 elpreima 6819 . . . . . . . . 9 (𝑅1 Fn On → (𝑥 ∈ (𝑅1 “ dom card) ↔ (𝑥 ∈ On ∧ (𝑅1𝑥) ∈ dom card)))
244, 23ax-mp 5 . . . . . . . 8 (𝑥 ∈ (𝑅1 “ dom card) ↔ (𝑥 ∈ On ∧ (𝑅1𝑥) ∈ dom card))
2524simplbi 501 . . . . . . 7 (𝑥 ∈ (𝑅1 “ dom card) → 𝑥 ∈ On)
26 onelon 6203 . . . . . . 7 ((𝑥 ∈ On ∧ 𝑦𝑥) → 𝑦 ∈ On)
2725, 26sylan 583 . . . . . 6 ((𝑥 ∈ (𝑅1 “ dom card) ∧ 𝑦𝑥) → 𝑦 ∈ On)
2824simprbi 500 . . . . . . . 8 (𝑥 ∈ (𝑅1 “ dom card) → (𝑅1𝑥) ∈ dom card)
2928adantr 484 . . . . . . 7 ((𝑥 ∈ (𝑅1 “ dom card) ∧ 𝑦𝑥) → (𝑅1𝑥) ∈ dom card)
30 r1ord2 9207 . . . . . . . . 9 (𝑥 ∈ On → (𝑦𝑥 → (𝑅1𝑦) ⊆ (𝑅1𝑥)))
3130imp 410 . . . . . . . 8 ((𝑥 ∈ On ∧ 𝑦𝑥) → (𝑅1𝑦) ⊆ (𝑅1𝑥))
3225, 31sylan 583 . . . . . . 7 ((𝑥 ∈ (𝑅1 “ dom card) ∧ 𝑦𝑥) → (𝑅1𝑦) ⊆ (𝑅1𝑥))
33 ssnum 9463 . . . . . . 7 (((𝑅1𝑥) ∈ dom card ∧ (𝑅1𝑦) ⊆ (𝑅1𝑥)) → (𝑅1𝑦) ∈ dom card)
3429, 32, 33syl2anc 587 . . . . . 6 ((𝑥 ∈ (𝑅1 “ dom card) ∧ 𝑦𝑥) → (𝑅1𝑦) ∈ dom card)
35 elpreima 6819 . . . . . . 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 586 . . . . 5 ((𝑥 ∈ (𝑅1 “ dom card) ∧ 𝑦𝑥) → 𝑦 ∈ (𝑅1 “ dom card))
3837rgen2 3198 . . . 4 𝑥 ∈ (𝑅1 “ dom card)∀𝑦𝑥 𝑦 ∈ (𝑅1 “ dom card)
39 dftr5 5161 . . . 4 (Tr (𝑅1 “ dom card) ↔ ∀𝑥 ∈ (𝑅1 “ dom card)∀𝑦𝑥 𝑦 ∈ (𝑅1 “ dom card))
4038, 39mpbir 234 . . 3 Tr (𝑅1 “ dom card)
41 cnvimass 5936 . . . . 5 (𝑅1 “ dom card) ⊆ dom 𝑅1
42 dffn2 6505 . . . . . . 7 (𝑅1 Fn On ↔ 𝑅1:On⟶V)
434, 42mpbi 233 . . . . . 6 𝑅1:On⟶V
4443fdmi 6514 . . . . 5 dom 𝑅1 = On
4541, 44sseqtri 3989 . . . 4 (𝑅1 “ dom card) ⊆ On
46 epweon 7491 . . . 4 E We On
47 wess 5529 . . . 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 6181 . . 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 9200 . . . . . . 7 ((𝑥 ∈ On ∧ 𝑦𝑥) → (𝑅1𝑦) ≺ (𝑅1𝑥))
5225, 51sylan 583 . . . . . 6 ((𝑥 ∈ (𝑅1 “ dom card) ∧ 𝑦𝑥) → (𝑅1𝑦) ≺ (𝑅1𝑥))
53 cardsdom2 9414 . . . . . . 7 (((𝑅1𝑦) ∈ dom card ∧ (𝑅1𝑥) ∈ dom card) → ((card‘(𝑅1𝑦)) ∈ (card‘(𝑅1𝑥)) ↔ (𝑅1𝑦) ≺ (𝑅1𝑥)))
5434, 29, 53syl2anc 587 . . . . . 6 ((𝑥 ∈ (𝑅1 “ dom card) ∧ 𝑦𝑥) → ((card‘(𝑅1𝑦)) ∈ (card‘(𝑅1𝑥)) ↔ (𝑅1𝑦) ≺ (𝑅1𝑥)))
5552, 54mpbird 260 . . . . 5 ((𝑥 ∈ (𝑅1 “ dom card) ∧ 𝑦𝑥) → (card‘(𝑅1𝑦)) ∈ (card‘(𝑅1𝑥)))
56 fvco2 6749 . . . . . 6 ((𝑅1 Fn On ∧ 𝑦 ∈ On) → ((card ∘ 𝑅1)‘𝑦) = (card‘(𝑅1𝑦)))
574, 27, 56sylancr 590 . . . . 5 ((𝑥 ∈ (𝑅1 “ dom card) ∧ 𝑦𝑥) → ((card ∘ 𝑅1)‘𝑦) = (card‘(𝑅1𝑦)))
5825adantr 484 . . . . . 6 ((𝑥 ∈ (𝑅1 “ dom card) ∧ 𝑦𝑥) → 𝑥 ∈ On)
59 fvco2 6749 . . . . . 6 ((𝑅1 Fn On ∧ 𝑥 ∈ On) → ((card ∘ 𝑅1)‘𝑥) = (card‘(𝑅1𝑥)))
604, 58, 59sylancr 590 . . . . 5 ((𝑥 ∈ (𝑅1 “ dom card) ∧ 𝑦𝑥) → ((card ∘ 𝑅1)‘𝑥) = (card‘(𝑅1𝑥)))
6155, 57, 603eltr4d 2931 . . . 4 ((𝑥 ∈ (𝑅1 “ dom card) ∧ 𝑦𝑥) → ((card ∘ 𝑅1)‘𝑦) ∈ ((card ∘ 𝑅1)‘𝑥))
6261ex 416 . . 3 (𝑥 ∈ (𝑅1 “ dom card) → (𝑦𝑥 → ((card ∘ 𝑅1)‘𝑦) ∈ ((card ∘ 𝑅1)‘𝑥)))
6362adantl 485 . 2 ((𝑦 ∈ (𝑅1 “ dom card) ∧ 𝑥 ∈ (𝑅1 “ dom card)) → (𝑦𝑥 → ((card ∘ 𝑅1)‘𝑦) ∈ ((card ∘ 𝑅1)‘𝑥)))
6422, 50, 63, 20issmo 7981 1 Smo (card ∘ 𝑅1)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538   ∈ wcel 2115  {cab 2802  ∀wral 3133  ∃wrex 3134  Vcvv 3480   ⊆ wss 3919   class class class wbr 5052  Tr wtr 5158   E cep 5451   We wwe 5500  ◡ccnv 5541  dom cdm 5542  ran crn 5543   ↾ cres 5544   “ cima 5545   ∘ ccom 5546  Ord word 6177  Oncon0 6178  Fun wfun 6337   Fn wfn 6338  ⟶wf 6339  ‘cfv 6343  Smo wsmo 7978   ≈ cen 8502   ≺ csdm 8504  𝑅1cr1 9188  cardccrd 9361 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 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-rep 5176  ax-sep 5189  ax-nul 5196  ax-pow 5253  ax-pr 5317  ax-un 7455 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ne 3015  df-ral 3138  df-rex 3139  df-reu 3140  df-rmo 3141  df-rab 3142  df-v 3482  df-sbc 3759  df-csb 3867  df-dif 3922  df-un 3924  df-in 3926  df-ss 3936  df-pss 3938  df-nul 4277  df-if 4451  df-pw 4524  df-sn 4551  df-pr 4553  df-tp 4555  df-op 4557  df-uni 4825  df-int 4863  df-iun 4907  df-br 5053  df-opab 5115  df-mpt 5133  df-tr 5159  df-id 5447  df-eprel 5452  df-po 5461  df-so 5462  df-fr 5501  df-se 5502  df-we 5503  df-xp 5548  df-rel 5549  df-cnv 5550  df-co 5551  df-dm 5552  df-rn 5553  df-res 5554  df-ima 5555  df-pred 6135  df-ord 6181  df-on 6182  df-lim 6183  df-suc 6184  df-iota 6302  df-fun 6345  df-fn 6346  df-f 6347  df-f1 6348  df-fo 6349  df-f1o 6350  df-fv 6351  df-isom 6352  df-riota 7107  df-om 7575  df-wrecs 7943  df-smo 7979  df-recs 8004  df-rdg 8042  df-er 8285  df-en 8506  df-dom 8507  df-sdom 8508  df-r1 9190  df-card 9365 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator