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 )