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 \circ R_{1})$

Proof

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

Metamath Proof Explorer

Theorem smobeth

Proof