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

Theorem smobeth 8466
 Description: The beth function is strictly monotone. This function is not strictly the beth function, but rather bethA is the same as , 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

Proof of Theorem smobeth
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 cardf2 7835 . . . . . . 7
2 ffun 5596 . . . . . . 7
31, 2ax-mp 5 . . . . . 6
4 r1fnon 7696 . . . . . . 7
5 fnfun 5545 . . . . . . 7
64, 5ax-mp 5 . . . . . 6
7 funco 5494 . . . . . 6
83, 6, 7mp2an 655 . . . . 5
9 funfn 5485 . . . . 5
108, 9mpbi 201 . . . 4
11 rnco 5379 . . . . 5
12 resss 5173 . . . . . . 7
13 rnss 5101 . . . . . . 7
1412, 13ax-mp 5 . . . . . 6
15 frn 5600 . . . . . . 7
161, 15ax-mp 5 . . . . . 6
1714, 16sstri 3359 . . . . 5
1811, 17eqsstri 3380 . . . 4
19 df-f 5461 . . . 4
2010, 18, 19mpbir2an 888 . . 3
21 dmco 5381 . . . 4
2221feq2i 5589 . . 3
2320, 22mpbi 201 . 2
24 elpreima 5853 . . . . . . . . 9
254, 24ax-mp 5 . . . . . . . 8
2625simplbi 448 . . . . . . 7
27 onelon 4609 . . . . . . 7
2826, 27sylan 459 . . . . . 6
2925simprbi 452 . . . . . . . 8
3029adantr 453 . . . . . . 7
31 r1ord2 7710 . . . . . . . . 9
3231imp 420 . . . . . . . 8
3326, 32sylan 459 . . . . . . 7
34 ssnum 7925 . . . . . . 7
3530, 33, 34syl2anc 644 . . . . . 6
36 elpreima 5853 . . . . . . 7
374, 36ax-mp 5 . . . . . 6
3828, 35, 37sylanbrc 647 . . . . 5
3938rgen2 2804 . . . 4
40 dftr5 4308 . . . 4
4139, 40mpbir 202 . . 3
42 cnvimass 5227 . . . . 5
43 dffn2 5595 . . . . . . 7
444, 43mpbi 201 . . . . . 6
4544fdmi 5599 . . . . 5
4642, 45sseqtri 3382 . . . 4
47 epweon 4767 . . . 4
48 wess 4572 . . . 4
4946, 47, 48mp2 9 . . 3
50 df-ord 4587 . . 3
5141, 49, 50mpbir2an 888 . 2
52 r1sdom 7703 . . . . . . 7
5326, 52sylan 459 . . . . . 6
54 cardsdom2 7880 . . . . . . 7
5535, 30, 54syl2anc 644 . . . . . 6
5653, 55mpbird 225 . . . . 5
57 fvco2 5801 . . . . . 6
584, 28, 57sylancr 646 . . . . 5
5926adantr 453 . . . . . 6
60 fvco2 5801 . . . . . 6
614, 59, 60sylancr 646 . . . . 5
6256, 58, 613eltr4d 2519 . . . 4
6362ex 425 . . 3