onomeneq

Description: An ordinal number equinumerous to a natural number is equal to it. Proposition 10.22 of TakeutiZaring p. 90 and its converse. (Contributed by NM, 26-Jul-2004)

		Ref	Expression
	Assertion	onomeneq	$⊢ (A \in On \land B \in ω) \to (A \approx B \leftrightarrow A = B)$

Proof

Step	Hyp	Ref	Expression
1		php5	$⊢ B \in ω \to \neg B \approx suc B$
2	1	ad2antlr	$⊢ ((A \in On \land B \in ω) \land A \approx B) \to \neg B \approx suc B$
3		enen1	$⊢ A \approx B \to (A \approx suc B \leftrightarrow B \approx suc B)$
4	3	adantl	$⊢ ((A \in On \land B \in ω) \land A \approx B) \to (A \approx suc B \leftrightarrow B \approx suc B)$
5	2 4	mtbird	$⊢ ((A \in On \land B \in ω) \land A \approx B) \to \neg A \approx suc B$
6		peano2	$⊢ B \in ω \to suc B \in ω$
7		sssucid	$⊢ B \subseteq suc B$
8		ssdomg	$⊢ suc B \in ω \to (B \subseteq suc B \to B ≼ suc B)$
9	6 7 8	mpisyl	$⊢ B \in ω \to B ≼ suc B$
10		endomtr	$⊢ (A \approx B \land B ≼ suc B) \to A ≼ suc B$
11	9 10	sylan2	$⊢ (A \approx B \land B \in ω) \to A ≼ suc B$
12	11	ancoms	$⊢ (B \in ω \land A \approx B) \to A ≼ suc B$
13	12	a1d	$⊢ (B \in ω \land A \approx B) \to (ω \subseteq A \to A ≼ suc B)$
14	13	adantll	$⊢ ((A \in On \land B \in ω) \land A \approx B) \to (ω \subseteq A \to A ≼ suc B)$
15		ssel	$⊢ ω \subseteq A \to (B \in ω \to B \in A)$
16	15	com12	$⊢ B \in ω \to (ω \subseteq A \to B \in A)$
17	16	adantr	$⊢ (B \in ω \land A \in On) \to (ω \subseteq A \to B \in A)$
18		eloni	$⊢ A \in On \to Ord A$
19		ordelsuc	$⊢ (B \in ω \land Ord A) \to (B \in A \leftrightarrow suc B \subseteq A)$
20	18 19	sylan2	$⊢ (B \in ω \land A \in On) \to (B \in A \leftrightarrow suc B \subseteq A)$
21	17 20	sylibd	$⊢ (B \in ω \land A \in On) \to (ω \subseteq A \to suc B \subseteq A)$
22		ssdomg	$⊢ A \in On \to (suc B \subseteq A \to suc B ≼ A)$
23	22	adantl	$⊢ (B \in ω \land A \in On) \to (suc B \subseteq A \to suc B ≼ A)$
24	21 23	syld	$⊢ (B \in ω \land A \in On) \to (ω \subseteq A \to suc B ≼ A)$
25	24	ancoms	$⊢ (A \in On \land B \in ω) \to (ω \subseteq A \to suc B ≼ A)$
26	25	adantr	$⊢ ((A \in On \land B \in ω) \land A \approx B) \to (ω \subseteq A \to suc B ≼ A)$
27	14 26	jcad	$⊢ ((A \in On \land B \in ω) \land A \approx B) \to (ω \subseteq A \to (A ≼ suc B \land suc B ≼ A))$
28		sbth	$⊢ (A ≼ suc B \land suc B ≼ A) \to A \approx suc B$
29	27 28	syl6	$⊢ ((A \in On \land B \in ω) \land A \approx B) \to (ω \subseteq A \to A \approx suc B)$
30	5 29	mtod	$⊢ ((A \in On \land B \in ω) \land A \approx B) \to \neg ω \subseteq A$
31		ordom	$⊢ Ord ω$
32		ordtri1	$⊢ (Ord ω \land Ord A) \to (ω \subseteq A \leftrightarrow \neg A \in ω)$
33	31 18 32	sylancr	$⊢ A \in On \to (ω \subseteq A \leftrightarrow \neg A \in ω)$
34	33	con2bid	$⊢ A \in On \to (A \in ω \leftrightarrow \neg ω \subseteq A)$
35	34	ad2antrr	$⊢ ((A \in On \land B \in ω) \land A \approx B) \to (A \in ω \leftrightarrow \neg ω \subseteq A)$
36	30 35	mpbird	$⊢ ((A \in On \land B \in ω) \land A \approx B) \to A \in ω$
37		simplr	$⊢ ((A \in On \land B \in ω) \land A \approx B) \to B \in ω$
38	36 37	jca	$⊢ ((A \in On \land B \in ω) \land A \approx B) \to (A \in ω \land B \in ω)$
39		nneneq	$⊢ (A \in ω \land B \in ω) \to (A \approx B \leftrightarrow A = B)$
40	39	biimpa	$⊢ ((A \in ω \land B \in ω) \land A \approx B) \to A = B$
41	38 40	sylancom	$⊢ ((A \in On \land B \in ω) \land A \approx B) \to A = B$
42	41	ex	$⊢ (A \in On \land B \in ω) \to (A \approx B \to A = B)$
43		eqeng	$⊢ A \in On \to (A = B \to A \approx B)$
44	43	adantr	$⊢ (A \in On \land B \in ω) \to (A = B \to A \approx B)$
45	42 44	impbid	$⊢ (A \in On \land B \in ω) \to (A \approx B \leftrightarrow A = B)$

Metamath Proof Explorer

Theorem onomeneq

Proof