This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem smobeth

Description: The beth function is strictly monotone. This function is not strictly the beth function, but rather beth_A is the same as ( card( R1( _om +o A ) ) ) , 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)

Ref Expression
Assertion smobeth Smo ( card ∘ 𝑅1 )

Proof

Step Hyp Ref Expression
1 cardf2 ⊢ card : { 𝑥 ∣ ∃ 𝑦 ∈ On 𝑦 ≈ 𝑥 } ⟶ On
2 ffun ⊢ ( card : { 𝑥 ∣ ∃ 𝑦 ∈ On 𝑦 ≈ 𝑥 } ⟶ On → Fun card )
3 1 2 ax-mp ⊢ Fun card
4 r1fnon ⊢ 𝑅1 Fn On
5 fnfun ⊢ ( 𝑅1 Fn On → Fun 𝑅1 )
6 4 5 ax-mp ⊢ Fun 𝑅1
7 funco ⊢ ( ( Fun card ∧ Fun 𝑅1 ) → Fun ( card ∘ 𝑅1 ) )
8 3 6 7 mp2an ⊢ Fun ( card ∘ 𝑅1 )
9 funfn ⊢ ( Fun ( card ∘ 𝑅1 ) ↔ ( card ∘ 𝑅1 ) Fn dom ( card ∘ 𝑅1 ) )
10 8 9 mpbi ⊢ ( card ∘ 𝑅1 ) Fn dom ( card ∘ 𝑅1 )
11 rnco ⊢ ran ( card ∘ 𝑅1 ) = ran ( card ↾ ran 𝑅1 )
12 resss ⊢ ( card ↾ ran 𝑅1 ) ⊆ card
13 12 rnssi ⊢ ran ( card ↾ ran 𝑅1 ) ⊆ ran card
14 frn ⊢ ( card : { 𝑥 ∣ ∃ 𝑦 ∈ On 𝑦 ≈ 𝑥 } ⟶ On → ran card ⊆ On )
15 1 14 ax-mp ⊢ ran card ⊆ On
16 13 15 sstri ⊢ ran ( card ↾ ran 𝑅1 ) ⊆ On
17 11 16 eqsstri ⊢ ran ( card ∘ 𝑅1 ) ⊆ On
18 df-f ⊢ ( ( card ∘ 𝑅1 ) : dom ( card ∘ 𝑅1 ) ⟶ On ↔ ( ( card ∘ 𝑅1 ) Fn dom ( card ∘ 𝑅1 ) ∧ ran ( card ∘ 𝑅1 ) ⊆ On ) )
19 10 17 18 mpbir2an ⊢ ( card ∘ 𝑅1 ) : dom ( card ∘ 𝑅1 ) ⟶ On
20 dmco ⊢ dom ( card ∘ 𝑅1 ) = ( ◡ 𝑅1 “ dom card )
21 20 feq2i ⊢ ( ( card ∘ 𝑅1 ) : dom ( card ∘ 𝑅1 ) ⟶ On ↔ ( card ∘ 𝑅1 ) : ( ◡ 𝑅1 “ dom card ) ⟶ On )
22 19 21 mpbi ⊢ ( card ∘ 𝑅1 ) : ( ◡ 𝑅1 “ dom card ) ⟶ On
23 elpreima ⊢ ( 𝑅1 Fn On → ( 𝑥 ∈ ( ◡ 𝑅1 “ dom card ) ↔ ( 𝑥 ∈ On ∧ ( 𝑅1 ‘ 𝑥 ) ∈ dom card ) ) )
24 4 23 ax-mp ⊢ ( 𝑥 ∈ ( ◡ 𝑅1 “ dom card ) ↔ ( 𝑥 ∈ On ∧ ( 𝑅1 ‘ 𝑥 ) ∈ dom card ) )
25 24 simplbi ⊢ ( 𝑥 ∈ ( ◡ 𝑅1 “ dom card ) → 𝑥 ∈ On )
26 onelon ⊢ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ 𝑥 ) → 𝑦 ∈ On )
27 25 26 sylan ⊢ ( ( 𝑥 ∈ ( ◡ 𝑅1 “ dom card ) ∧ 𝑦 ∈ 𝑥 ) → 𝑦 ∈ On )
28 24 simprbi ⊢ ( 𝑥 ∈ ( ◡ 𝑅1 “ dom card ) → ( 𝑅1 ‘ 𝑥 ) ∈ dom card )
29 28 adantr ⊢ ( ( 𝑥 ∈ ( ◡ 𝑅1 “ dom card ) ∧ 𝑦 ∈ 𝑥 ) → ( 𝑅1 ‘ 𝑥 ) ∈ dom card )
30 r1ord2 ⊢ ( 𝑥 ∈ On → ( 𝑦 ∈ 𝑥 → ( 𝑅1 ‘ 𝑦 ) ⊆ ( 𝑅1 ‘ 𝑥 ) ) )
31 30 imp ⊢ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ 𝑥 ) → ( 𝑅1 ‘ 𝑦 ) ⊆ ( 𝑅1 ‘ 𝑥 ) )
32 25 31 sylan ⊢ ( ( 𝑥 ∈ ( ◡ 𝑅1 “ dom card ) ∧ 𝑦 ∈ 𝑥 ) → ( 𝑅1 ‘ 𝑦 ) ⊆ ( 𝑅1 ‘ 𝑥 ) )
33 ssnum ⊢ ( ( ( 𝑅1 ‘ 𝑥 ) ∈ dom card ∧ ( 𝑅1 ‘ 𝑦 ) ⊆ ( 𝑅1 ‘ 𝑥 ) ) → ( 𝑅1 ‘ 𝑦 ) ∈ dom card )
34 29 32 33 syl2anc ⊢ ( ( 𝑥 ∈ ( ◡ 𝑅1 “ dom card ) ∧ 𝑦 ∈ 𝑥 ) → ( 𝑅1 ‘ 𝑦 ) ∈ dom card )
35 elpreima ⊢ ( 𝑅1 Fn On → ( 𝑦 ∈ ( ◡ 𝑅1 “ dom card ) ↔ ( 𝑦 ∈ On ∧ ( 𝑅1 ‘ 𝑦 ) ∈ dom card ) ) )
36 4 35 ax-mp ⊢ ( 𝑦 ∈ ( ◡ 𝑅1 “ dom card ) ↔ ( 𝑦 ∈ On ∧ ( 𝑅1 ‘ 𝑦 ) ∈ dom card ) )
37 27 34 36 sylanbrc ⊢ ( ( 𝑥 ∈ ( ◡ 𝑅1 “ dom card ) ∧ 𝑦 ∈ 𝑥 ) → 𝑦 ∈ ( ◡ 𝑅1 “ dom card ) )
38 37 rgen2 ⊢ ∀ 𝑥 ∈ ( ◡ 𝑅1 “ dom card ) ∀ 𝑦 ∈ 𝑥 𝑦 ∈ ( ◡ 𝑅1 “ dom card )
39 dftr5 ⊢ ( Tr ( ◡ 𝑅1 “ dom card ) ↔ ∀ 𝑥 ∈ ( ◡ 𝑅1 “ dom card ) ∀ 𝑦 ∈ 𝑥 𝑦 ∈ ( ◡ 𝑅1 “ dom card ) )
40 38 39 mpbir ⊢ Tr ( ◡ 𝑅1 “ dom card )
41 cnvimass ⊢ ( ◡ 𝑅1 “ dom card ) ⊆ dom 𝑅1
42 dffn2 ⊢ ( 𝑅1 Fn On ↔ 𝑅1 : On ⟶ V )
43 4 42 mpbi ⊢ 𝑅1 : On ⟶ V
44 43 fdmi ⊢ dom 𝑅1 = On
45 41 44 sseqtri ⊢ ( ◡ 𝑅1 “ dom card ) ⊆ On
46 epweon ⊢ E We On
47 wess ⊢ ( ( ◡ 𝑅1 “ dom card ) ⊆ On → ( E We On → E We ( ◡ 𝑅1 “ dom card ) ) )
48 45 46 47 mp2 ⊢ E We ( ◡ 𝑅1 “ dom card )
49 df-ord ⊢ ( Ord ( ◡ 𝑅1 “ dom card ) ↔ ( Tr ( ◡ 𝑅1 “ dom card ) ∧ E We ( ◡ 𝑅1 “ dom card ) ) )
50 40 48 49 mpbir2an ⊢ Ord ( ◡ 𝑅1 “ dom card )
51 r1sdom ⊢ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ 𝑥 ) → ( 𝑅1 ‘ 𝑦 ) ≺ ( 𝑅1 ‘ 𝑥 ) )
52 25 51 sylan ⊢ ( ( 𝑥 ∈ ( ◡ 𝑅1 “ dom card ) ∧ 𝑦 ∈ 𝑥 ) → ( 𝑅1 ‘ 𝑦 ) ≺ ( 𝑅1 ‘ 𝑥 ) )
53 cardsdom2 ⊢ ( ( ( 𝑅1 ‘ 𝑦 ) ∈ dom card ∧ ( 𝑅1 ‘ 𝑥 ) ∈ dom card ) → ( ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ∈ ( card ‘ ( 𝑅1 ‘ 𝑥 ) ) ↔ ( 𝑅1 ‘ 𝑦 ) ≺ ( 𝑅1 ‘ 𝑥 ) ) )
54 34 29 53 syl2anc ⊢ ( ( 𝑥 ∈ ( ◡ 𝑅1 “ dom card ) ∧ 𝑦 ∈ 𝑥 ) → ( ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ∈ ( card ‘ ( 𝑅1 ‘ 𝑥 ) ) ↔ ( 𝑅1 ‘ 𝑦 ) ≺ ( 𝑅1 ‘ 𝑥 ) ) )
55 52 54 mpbird ⊢ ( ( 𝑥 ∈ ( ◡ 𝑅1 “ dom card ) ∧ 𝑦 ∈ 𝑥 ) → ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ∈ ( card ‘ ( 𝑅1 ‘ 𝑥 ) ) )
56 fvco2 ⊢ ( ( 𝑅1 Fn On ∧ 𝑦 ∈ On ) → ( ( card ∘ 𝑅1 ) ‘ 𝑦 ) = ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) )
57 4 27 56 sylancr ⊢ ( ( 𝑥 ∈ ( ◡ 𝑅1 “ dom card ) ∧ 𝑦 ∈ 𝑥 ) → ( ( card ∘ 𝑅1 ) ‘ 𝑦 ) = ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) )
58 25 adantr ⊢ ( ( 𝑥 ∈ ( ◡ 𝑅1 “ dom card ) ∧ 𝑦 ∈ 𝑥 ) → 𝑥 ∈ On )
59 fvco2 ⊢ ( ( 𝑅1 Fn On ∧ 𝑥 ∈ On ) → ( ( card ∘ 𝑅1 ) ‘ 𝑥 ) = ( card ‘ ( 𝑅1 ‘ 𝑥 ) ) )
60 4 58 59 sylancr ⊢ ( ( 𝑥 ∈ ( ◡ 𝑅1 “ dom card ) ∧ 𝑦 ∈ 𝑥 ) → ( ( card ∘ 𝑅1 ) ‘ 𝑥 ) = ( card ‘ ( 𝑅1 ‘ 𝑥 ) ) )
61 55 57 60 3eltr4d ⊢ ( ( 𝑥 ∈ ( ◡ 𝑅1 “ dom card ) ∧ 𝑦 ∈ 𝑥 ) → ( ( card ∘ 𝑅1 ) ‘ 𝑦 ) ∈ ( ( card ∘ 𝑅1 ) ‘ 𝑥 ) )
62 61 ex ⊢ ( 𝑥 ∈ ( ◡ 𝑅1 “ dom card ) → ( 𝑦 ∈ 𝑥 → ( ( card ∘ 𝑅1 ) ‘ 𝑦 ) ∈ ( ( card ∘ 𝑅1 ) ‘ 𝑥 ) ) )
63 62 adantl ⊢ ( ( 𝑦 ∈ ( ◡ 𝑅1 “ dom card ) ∧ 𝑥 ∈ ( ◡ 𝑅1 “ dom card ) ) → ( 𝑦 ∈ 𝑥 → ( ( card ∘ 𝑅1 ) ‘ 𝑦 ) ∈ ( ( card ∘ 𝑅1 ) ‘ 𝑥 ) ) )
64 22 50 63 20 issmo ⊢ Smo ( card ∘ 𝑅1 )