Theorem smobeth 9997

Description: The beth function is strictly monotone. This function is not strictly the beth function, but rather beth_A is the same as (card‘(𝑅₁‘(ω +_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.

Step	Hyp	Ref	Expression
1		cardf2 9356	. . . . . . 7 ⊢ card:{𝑥 ∣ ∃𝑦 ∈ On 𝑦 ≈ 𝑥}⟶On
2		ffun 6490	. . . . . . 7 ⊢ (card:{𝑥 ∣ ∃𝑦 ∈ On 𝑦 ≈ 𝑥}⟶On → Fun card)
3	1, 2	ax-mp 5	. . . . . 6 ⊢ Fun card
4		r1fnon 9180	. . . . . . 7 ⊢ 𝑅1 Fn On
5		fnfun 6423	. . . . . . 7 ⊢ (𝑅1 Fn On → Fun 𝑅1)
6	4, 5	ax-mp 5	. . . . . 6 ⊢ Fun 𝑅1
7		funco 6364	. . . . . 6 ⊢ ((Fun card ∧ Fun 𝑅1) → Fun (card ∘ 𝑅1))
8	3, 6, 7	mp2an 691	. . . . 5 ⊢ Fun (card ∘ 𝑅1)
9		funfn 6354	. . . . 5 ⊢ (Fun (card ∘ 𝑅1) ↔ (card ∘ 𝑅1) Fn dom (card ∘ 𝑅1))
10	8, 9	mpbi 233	. . . 4 ⊢ (card ∘ 𝑅1) Fn dom (card ∘ 𝑅1)
11		rnco 6072	. . . . 5 ⊢ ran (card ∘ 𝑅1) = ran (card ↾ ran 𝑅1)
12		resss 5843	. . . . . . 7 ⊢ (card ↾ ran 𝑅1) ⊆ card
13	12	rnssi 5774	. . . . . 6 ⊢ ran (card ↾ ran 𝑅1) ⊆ ran card
14		frn 6493	. . . . . . 7 ⊢ (card:{𝑥 ∣ ∃𝑦 ∈ On 𝑦 ≈ 𝑥}⟶On → ran card ⊆ On)
15	1, 14	ax-mp 5	. . . . . 6 ⊢ ran card ⊆ On
16	13, 15	sstri 3924	. . . . 5 ⊢ ran (card ↾ ran 𝑅1) ⊆ On
17	11, 16	eqsstri 3949	. . . 4 ⊢ ran (card ∘ 𝑅1) ⊆ On
18		df-f 6328	. . . 4 ⊢ ((card ∘ 𝑅1):dom (card ∘ 𝑅1)⟶On ↔ ((card ∘ 𝑅1) Fn dom (card ∘ 𝑅1) ∧ ran (card ∘ 𝑅1) ⊆ On))
19	10, 17, 18	mpbir2an 710	. . 3 ⊢ (card ∘ 𝑅1):dom (card ∘ 𝑅1)⟶On
20		dmco 6074	. . . 4 ⊢ dom (card ∘ 𝑅1) = (◡𝑅1 “ dom card)
21	20	feq2i 6479	. . 3 ⊢ ((card ∘ 𝑅1):dom (card ∘ 𝑅1)⟶On ↔ (card ∘ 𝑅1):(◡𝑅1 “ dom card)⟶On)
22	19, 21	mpbi 233	. 2 ⊢ (card ∘ 𝑅1):(◡𝑅1 “ dom card)⟶On
23		elpreima 6805	. . . . . . . . 9 ⊢ (𝑅1 Fn On → (𝑥 ∈ (◡𝑅1 “ dom card) ↔ (𝑥 ∈ On ∧ (𝑅1‘𝑥) ∈ dom card)))
24	4, 23	ax-mp 5	. . . . . . . 8 ⊢ (𝑥 ∈ (◡𝑅1 “ dom card) ↔ (𝑥 ∈ On ∧ (𝑅1‘𝑥) ∈ dom card))
25	24	simplbi 501	. . . . . . 7 ⊢ (𝑥 ∈ (◡𝑅1 “ dom card) → 𝑥 ∈ On)
26		onelon 6184	. . . . . . 7 ⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ On)
27	25, 26	sylan 583	. . . . . 6 ⊢ ((𝑥 ∈ (◡𝑅1 “ dom card) ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ On)
28	24	simprbi 500	. . . . . . . 8 ⊢ (𝑥 ∈ (◡𝑅1 “ dom card) → (𝑅1‘𝑥) ∈ dom card)
29	28	adantr 484	. . . . . . 7 ⊢ ((𝑥 ∈ (◡𝑅1 “ dom card) ∧ 𝑦 ∈ 𝑥) → (𝑅1‘𝑥) ∈ dom card)
30		r1ord2 9194	. . . . . . . . 9 ⊢ (𝑥 ∈ On → (𝑦 ∈ 𝑥 → (𝑅1‘𝑦) ⊆ (𝑅1‘𝑥)))
31	30	imp 410	. . . . . . . 8 ⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ 𝑥) → (𝑅1‘𝑦) ⊆ (𝑅1‘𝑥))
32	25, 31	sylan 583	. . . . . . 7 ⊢ ((𝑥 ∈ (◡𝑅1 “ dom card) ∧ 𝑦 ∈ 𝑥) → (𝑅1‘𝑦) ⊆ (𝑅1‘𝑥))
33		ssnum 9450	. . . . . . 7 ⊢ (((𝑅1‘𝑥) ∈ dom card ∧ (𝑅1‘𝑦) ⊆ (𝑅1‘𝑥)) → (𝑅1‘𝑦) ∈ dom card)
34	29, 32, 33	syl2anc 587	. . . . . 6 ⊢ ((𝑥 ∈ (◡𝑅1 “ dom card) ∧ 𝑦 ∈ 𝑥) → (𝑅1‘𝑦) ∈ dom card)
35		elpreima 6805	. . . . . . 7 ⊢ (𝑅1 Fn On → (𝑦 ∈ (◡𝑅1 “ dom card) ↔ (𝑦 ∈ On ∧ (𝑅1‘𝑦) ∈ dom card)))
36	4, 35	ax-mp 5	. . . . . 6 ⊢ (𝑦 ∈ (◡𝑅1 “ dom card) ↔ (𝑦 ∈ On ∧ (𝑅1‘𝑦) ∈ dom card))
37	27, 34, 36	sylanbrc 586	. . . . 5 ⊢ ((𝑥 ∈ (◡𝑅1 “ dom card) ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ (◡𝑅1 “ dom card))
38	37	rgen2 3168	. . . 4 ⊢ ∀𝑥 ∈ (◡𝑅1 “ dom card)∀𝑦 ∈ 𝑥 𝑦 ∈ (◡𝑅1 “ dom card)
39		dftr5 5139	. . . 4 ⊢ (Tr (◡𝑅1 “ dom card) ↔ ∀𝑥 ∈ (◡𝑅1 “ dom card)∀𝑦 ∈ 𝑥 𝑦 ∈ (◡𝑅1 “ dom card))
40	38, 39	mpbir 234	. . 3 ⊢ Tr (◡𝑅1 “ dom card)
41		cnvimass 5916	. . . . 5 ⊢ (◡𝑅1 “ dom card) ⊆ dom 𝑅1
42		dffn2 6489	. . . . . . 7 ⊢ (𝑅1 Fn On ↔ 𝑅1:On⟶V)
43	4, 42	mpbi 233	. . . . . 6 ⊢ 𝑅1:On⟶V
44	43	fdmi 6498	. . . . 5 ⊢ dom 𝑅1 = On
45	41, 44	sseqtri 3951	. . . 4 ⊢ (◡𝑅1 “ dom card) ⊆ On
46		epweon 7477	. . . 4 ⊢ E We On
47		wess 5506	. . . 4 ⊢ ((◡𝑅1 “ dom card) ⊆ On → ( E We On → E We (◡𝑅1 “ dom card)))
48	45, 46, 47	mp2 9	. . 3 ⊢ E We (◡𝑅1 “ dom card)
49		df-ord 6162	. . 3 ⊢ (Ord (◡𝑅1 “ dom card) ↔ (Tr (◡𝑅1 “ dom card) ∧ E We (◡𝑅1 “ dom card)))
50	40, 48, 49	mpbir2an 710	. 2 ⊢ Ord (◡𝑅1 “ dom card)
51		r1sdom 9187	. . . . . . 7 ⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ 𝑥) → (𝑅1‘𝑦) ≺ (𝑅1‘𝑥))
52	25, 51	sylan 583	. . . . . 6 ⊢ ((𝑥 ∈ (◡𝑅1 “ dom card) ∧ 𝑦 ∈ 𝑥) → (𝑅1‘𝑦) ≺ (𝑅1‘𝑥))
53		cardsdom2 9401	. . . . . . 7 ⊢ (((𝑅1‘𝑦) ∈ dom card ∧ (𝑅1‘𝑥) ∈ dom card) → ((card‘(𝑅1‘𝑦)) ∈ (card‘(𝑅1‘𝑥)) ↔ (𝑅1‘𝑦) ≺ (𝑅1‘𝑥)))
54	34, 29, 53	syl2anc 587	. . . . . 6 ⊢ ((𝑥 ∈ (◡𝑅1 “ dom card) ∧ 𝑦 ∈ 𝑥) → ((card‘(𝑅1‘𝑦)) ∈ (card‘(𝑅1‘𝑥)) ↔ (𝑅1‘𝑦) ≺ (𝑅1‘𝑥)))
55	52, 54	mpbird 260	. . . . 5 ⊢ ((𝑥 ∈ (◡𝑅1 “ dom card) ∧ 𝑦 ∈ 𝑥) → (card‘(𝑅1‘𝑦)) ∈ (card‘(𝑅1‘𝑥)))
56		fvco2 6735	. . . . . 6 ⊢ ((𝑅1 Fn On ∧ 𝑦 ∈ On) → ((card ∘ 𝑅1)‘𝑦) = (card‘(𝑅1‘𝑦)))
57	4, 27, 56	sylancr 590	. . . . 5 ⊢ ((𝑥 ∈ (◡𝑅1 “ dom card) ∧ 𝑦 ∈ 𝑥) → ((card ∘ 𝑅1)‘𝑦) = (card‘(𝑅1‘𝑦)))
58	25	adantr 484	. . . . . 6 ⊢ ((𝑥 ∈ (◡𝑅1 “ dom card) ∧ 𝑦 ∈ 𝑥) → 𝑥 ∈ On)
59		fvco2 6735	. . . . . 6 ⊢ ((𝑅1 Fn On ∧ 𝑥 ∈ On) → ((card ∘ 𝑅1)‘𝑥) = (card‘(𝑅1‘𝑥)))
60	4, 58, 59	sylancr 590	. . . . 5 ⊢ ((𝑥 ∈ (◡𝑅1 “ dom card) ∧ 𝑦 ∈ 𝑥) → ((card ∘ 𝑅1)‘𝑥) = (card‘(𝑅1‘𝑥)))
61	55, 57, 60	3eltr4d 2905	. . . 4 ⊢ ((𝑥 ∈ (◡𝑅1 “ dom card) ∧ 𝑦 ∈ 𝑥) → ((card ∘ 𝑅1)‘𝑦) ∈ ((card ∘ 𝑅1)‘𝑥))
62	61	ex 416	. . 3 ⊢ (𝑥 ∈ (◡𝑅1 “ dom card) → (𝑦 ∈ 𝑥 → ((card ∘ 𝑅1)‘𝑦) ∈ ((card ∘ 𝑅1)‘𝑥)))
63	62	adantl 485	. 2 ⊢ ((𝑦 ∈ (◡𝑅1 “ dom card) ∧ 𝑥 ∈ (◡𝑅1 “ dom card)) → (𝑦 ∈ 𝑥 → ((card ∘ 𝑅1)‘𝑦) ∈ ((card ∘ 𝑅1)‘𝑥)))
64	22, 50, 63, 20	issmo 7968	1 ⊢ Smo (card ∘ 𝑅1)

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538   ∈ wcel 2111  {cab 2776  ∀wral 3106  ∃wrex 3107  Vcvv 3441   ⊆ wss 3881   class class class wbr 5030  Tr wtr 5136   E cep 5429   We wwe 5477  ^◡ccnv 5518  dom cdm 5519  ran crn 5520   ↾ cres 5521   “ cima 5522   ∘ ccom 5523  Ord word 6158  Oncon0 6159  Fun wfun 6318   Fn wfn 6319  ⟶wf 6320  ‘cfv 6324  Smo wsmo 7965   ≈ cen 8489   ≺ csdm 8491  𝑅₁cr1 9175  cardccrd 9348

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-rep 5154  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7441

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 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-ral 3111  df-rex 3112  df-reu 3113  df-rmo 3114  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-pss 3900  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4801  df-int 4839  df-iun 4883  df-br 5031  df-opab 5093  df-mpt 5111  df-tr 5137  df-id 5425  df-eprel 5430  df-po 5438  df-so 5439  df-fr 5478  df-se 5479  df-we 5480  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-pred 6116  df-ord 6162  df-on 6163  df-lim 6164  df-suc 6165  df-iota 6283  df-fun 6326  df-fn 6327  df-f 6328  df-f1 6329  df-fo 6330  df-f1o 6331  df-fv 6332  df-isom 6333  df-riota 7093  df-om 7561  df-wrecs 7930  df-smo 7966  df-recs 7991  df-rdg 8029  df-er 8272  df-en 8493  df-dom 8494  df-sdom 8495  df-r1 9177  df-card 9352

This theorem is referenced by: (None)