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

Theorem smobeth 9359
Description: The beth function is strictly monotone. This function is not strictly the beth function, but rather bethA is the same as (card‘(𝑅1‘(ω +𝑜 𝐴))), 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 8720 . . . . . . 7 card:{𝑥 ∣ ∃𝑦 ∈ On 𝑦𝑥}⟶On
2 ffun 6010 . . . . . . 7 (card:{𝑥 ∣ ∃𝑦 ∈ On 𝑦𝑥}⟶On → Fun card)
31, 2ax-mp 5 . . . . . 6 Fun card
4 r1fnon 8581 . . . . . . 7 𝑅1 Fn On
5 fnfun 5951 . . . . . . 7 (𝑅1 Fn On → Fun 𝑅1)
64, 5ax-mp 5 . . . . . 6 Fun 𝑅1
7 funco 5891 . . . . . 6 ((Fun card ∧ Fun 𝑅1) → Fun (card ∘ 𝑅1))
83, 6, 7mp2an 707 . . . . 5 Fun (card ∘ 𝑅1)
9 funfn 5882 . . . . 5 (Fun (card ∘ 𝑅1) ↔ (card ∘ 𝑅1) Fn dom (card ∘ 𝑅1))
108, 9mpbi 220 . . . 4 (card ∘ 𝑅1) Fn dom (card ∘ 𝑅1)
11 rnco 5605 . . . . 5 ran (card ∘ 𝑅1) = ran (card ↾ ran 𝑅1)
12 resss 5386 . . . . . . 7 (card ↾ ran 𝑅1) ⊆ card
13 rnss 5319 . . . . . . 7 ((card ↾ ran 𝑅1) ⊆ card → ran (card ↾ ran 𝑅1) ⊆ ran card)
1412, 13ax-mp 5 . . . . . 6 ran (card ↾ ran 𝑅1) ⊆ ran card
15 frn 6015 . . . . . . 7 (card:{𝑥 ∣ ∃𝑦 ∈ On 𝑦𝑥}⟶On → ran card ⊆ On)
161, 15ax-mp 5 . . . . . 6 ran card ⊆ On
1714, 16sstri 3596 . . . . 5 ran (card ↾ ran 𝑅1) ⊆ On
1811, 17eqsstri 3619 . . . 4 ran (card ∘ 𝑅1) ⊆ On
19 df-f 5856 . . . 4 ((card ∘ 𝑅1):dom (card ∘ 𝑅1)⟶On ↔ ((card ∘ 𝑅1) Fn dom (card ∘ 𝑅1) ∧ ran (card ∘ 𝑅1) ⊆ On))
2010, 18, 19mpbir2an 954 . . 3 (card ∘ 𝑅1):dom (card ∘ 𝑅1)⟶On
21 dmco 5607 . . . 4 dom (card ∘ 𝑅1) = (𝑅1 “ dom card)
2221feq2i 5999 . . 3 ((card ∘ 𝑅1):dom (card ∘ 𝑅1)⟶On ↔ (card ∘ 𝑅1):(𝑅1 “ dom card)⟶On)
2320, 22mpbi 220 . 2 (card ∘ 𝑅1):(𝑅1 “ dom card)⟶On
24 elpreima 6298 . . . . . . . . 9 (𝑅1 Fn On → (𝑥 ∈ (𝑅1 “ dom card) ↔ (𝑥 ∈ On ∧ (𝑅1𝑥) ∈ dom card)))
254, 24ax-mp 5 . . . . . . . 8 (𝑥 ∈ (𝑅1 “ dom card) ↔ (𝑥 ∈ On ∧ (𝑅1𝑥) ∈ dom card))
2625simplbi 476 . . . . . . 7 (𝑥 ∈ (𝑅1 “ dom card) → 𝑥 ∈ On)
27 onelon 5712 . . . . . . 7 ((𝑥 ∈ On ∧ 𝑦𝑥) → 𝑦 ∈ On)
2826, 27sylan 488 . . . . . 6 ((𝑥 ∈ (𝑅1 “ dom card) ∧ 𝑦𝑥) → 𝑦 ∈ On)
2925simprbi 480 . . . . . . . 8 (𝑥 ∈ (𝑅1 “ dom card) → (𝑅1𝑥) ∈ dom card)
3029adantr 481 . . . . . . 7 ((𝑥 ∈ (𝑅1 “ dom card) ∧ 𝑦𝑥) → (𝑅1𝑥) ∈ dom card)
31 r1ord2 8595 . . . . . . . . 9 (𝑥 ∈ On → (𝑦𝑥 → (𝑅1𝑦) ⊆ (𝑅1𝑥)))
3231imp 445 . . . . . . . 8 ((𝑥 ∈ On ∧ 𝑦𝑥) → (𝑅1𝑦) ⊆ (𝑅1𝑥))
3326, 32sylan 488 . . . . . . 7 ((𝑥 ∈ (𝑅1 “ dom card) ∧ 𝑦𝑥) → (𝑅1𝑦) ⊆ (𝑅1𝑥))
34 ssnum 8813 . . . . . . 7 (((𝑅1𝑥) ∈ dom card ∧ (𝑅1𝑦) ⊆ (𝑅1𝑥)) → (𝑅1𝑦) ∈ dom card)
3530, 33, 34syl2anc 692 . . . . . 6 ((𝑥 ∈ (𝑅1 “ dom card) ∧ 𝑦𝑥) → (𝑅1𝑦) ∈ dom card)
36 elpreima 6298 . . . . . . 7 (𝑅1 Fn On → (𝑦 ∈ (𝑅1 “ dom card) ↔ (𝑦 ∈ On ∧ (𝑅1𝑦) ∈ dom card)))
374, 36ax-mp 5 . . . . . 6 (𝑦 ∈ (𝑅1 “ dom card) ↔ (𝑦 ∈ On ∧ (𝑅1𝑦) ∈ dom card))
3828, 35, 37sylanbrc 697 . . . . 5 ((𝑥 ∈ (𝑅1 “ dom card) ∧ 𝑦𝑥) → 𝑦 ∈ (𝑅1 “ dom card))
3938rgen2 2970 . . . 4 𝑥 ∈ (𝑅1 “ dom card)∀𝑦𝑥 𝑦 ∈ (𝑅1 “ dom card)
40 dftr5 4720 . . . 4 (Tr (𝑅1 “ dom card) ↔ ∀𝑥 ∈ (𝑅1 “ dom card)∀𝑦𝑥 𝑦 ∈ (𝑅1 “ dom card))
4139, 40mpbir 221 . . 3 Tr (𝑅1 “ dom card)
42 cnvimass 5449 . . . . 5 (𝑅1 “ dom card) ⊆ dom 𝑅1
43 dffn2 6009 . . . . . . 7 (𝑅1 Fn On ↔ 𝑅1:On⟶V)
444, 43mpbi 220 . . . . . 6 𝑅1:On⟶V
4544fdmi 6014 . . . . 5 dom 𝑅1 = On
4642, 45sseqtri 3621 . . . 4 (𝑅1 “ dom card) ⊆ On
47 epweon 6937 . . . 4 E We On
48 wess 5066 . . . 4 ((𝑅1 “ dom card) ⊆ On → ( E We On → E We (𝑅1 “ dom card)))
4946, 47, 48mp2 9 . . 3 E We (𝑅1 “ dom card)
50 df-ord 5690 . . 3 (Ord (𝑅1 “ dom card) ↔ (Tr (𝑅1 “ dom card) ∧ E We (𝑅1 “ dom card)))
5141, 49, 50mpbir2an 954 . 2 Ord (𝑅1 “ dom card)
52 r1sdom 8588 . . . . . . 7 ((𝑥 ∈ On ∧ 𝑦𝑥) → (𝑅1𝑦) ≺ (𝑅1𝑥))
5326, 52sylan 488 . . . . . 6 ((𝑥 ∈ (𝑅1 “ dom card) ∧ 𝑦𝑥) → (𝑅1𝑦) ≺ (𝑅1𝑥))
54 cardsdom2 8765 . . . . . . 7 (((𝑅1𝑦) ∈ dom card ∧ (𝑅1𝑥) ∈ dom card) → ((card‘(𝑅1𝑦)) ∈ (card‘(𝑅1𝑥)) ↔ (𝑅1𝑦) ≺ (𝑅1𝑥)))
5535, 30, 54syl2anc 692 . . . . . 6 ((𝑥 ∈ (𝑅1 “ dom card) ∧ 𝑦𝑥) → ((card‘(𝑅1𝑦)) ∈ (card‘(𝑅1𝑥)) ↔ (𝑅1𝑦) ≺ (𝑅1𝑥)))
5653, 55mpbird 247 . . . . 5 ((𝑥 ∈ (𝑅1 “ dom card) ∧ 𝑦𝑥) → (card‘(𝑅1𝑦)) ∈ (card‘(𝑅1𝑥)))
57 fvco2 6235 . . . . . 6 ((𝑅1 Fn On ∧ 𝑦 ∈ On) → ((card ∘ 𝑅1)‘𝑦) = (card‘(𝑅1𝑦)))
584, 28, 57sylancr 694 . . . . 5 ((𝑥 ∈ (𝑅1 “ dom card) ∧ 𝑦𝑥) → ((card ∘ 𝑅1)‘𝑦) = (card‘(𝑅1𝑦)))
5926adantr 481 . . . . . 6 ((𝑥 ∈ (𝑅1 “ dom card) ∧ 𝑦𝑥) → 𝑥 ∈ On)
60 fvco2 6235 . . . . . 6 ((𝑅1 Fn On ∧ 𝑥 ∈ On) → ((card ∘ 𝑅1)‘𝑥) = (card‘(𝑅1𝑥)))
614, 59, 60sylancr 694 . . . . 5 ((𝑥 ∈ (𝑅1 “ dom card) ∧ 𝑦𝑥) → ((card ∘ 𝑅1)‘𝑥) = (card‘(𝑅1𝑥)))
6256, 58, 613eltr4d 2713 . . . 4 ((𝑥 ∈ (𝑅1 “ dom card) ∧ 𝑦𝑥) → ((card ∘ 𝑅1)‘𝑦) ∈ ((card ∘ 𝑅1)‘𝑥))
6362ex 450 . . 3 (𝑥 ∈ (𝑅1 “ dom card) → (𝑦𝑥 → ((card ∘ 𝑅1)‘𝑦) ∈ ((card ∘ 𝑅1)‘𝑥)))
6463adantl 482 . 2 ((𝑦 ∈ (𝑅1 “ dom card) ∧ 𝑥 ∈ (𝑅1 “ dom card)) → (𝑦𝑥 → ((card ∘ 𝑅1)‘𝑦) ∈ ((card ∘ 𝑅1)‘𝑥)))
6523, 51, 64, 21issmo 7397 1 Smo (card ∘ 𝑅1)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384   = wceq 1480  wcel 1987  {cab 2607  wral 2907  wrex 2908  Vcvv 3189  wss 3559   class class class wbr 4618  Tr wtr 4717   E cep 4988   We wwe 5037  ccnv 5078  dom cdm 5079  ran crn 5080  cres 5081  cima 5082  ccom 5083  Ord word 5686  Oncon0 5687  Fun wfun 5846   Fn wfn 5847  wf 5848  cfv 5852  Smo wsmo 7394  cen 7903  csdm 7905  𝑅1cr1 8576  cardccrd 8712
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4736  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6909
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2912  df-rex 2913  df-reu 2914  df-rmo 2915  df-rab 2916  df-v 3191  df-sbc 3422  df-csb 3519  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-pss 3575  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-tp 4158  df-op 4160  df-uni 4408  df-int 4446  df-iun 4492  df-br 4619  df-opab 4679  df-mpt 4680  df-tr 4718  df-eprel 4990  df-id 4994  df-po 5000  df-so 5001  df-fr 5038  df-se 5039  df-we 5040  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-pred 5644  df-ord 5690  df-on 5691  df-lim 5692  df-suc 5693  df-iota 5815  df-fun 5854  df-fn 5855  df-f 5856  df-f1 5857  df-fo 5858  df-f1o 5859  df-fv 5860  df-isom 5861  df-riota 6571  df-om 7020  df-wrecs 7359  df-smo 7395  df-recs 7420  df-rdg 7458  df-er 7694  df-en 7907  df-dom 7908  df-sdom 7909  df-r1 8578  df-card 8716
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator