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) Avoid ax-pow . (Revised by BTernaryTau, 2-Dec-2024)

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

Proof

Step	Hyp	Ref	Expression
1		endom	$⊢ A \approx B \to A ≼ B$
2		nnfi	$⊢ B \in ω \to B \in Fin$
3		domfi	$⊢ (B \in Fin \land A ≼ B) \to A \in Fin$
4		simpr	$⊢ (B \in Fin \land A ≼ B) \to A ≼ B$
5	3 4	jca	$⊢ (B \in Fin \land A ≼ B) \to (A \in Fin \land A ≼ B)$
6		domnsymfi	$⊢ (A \in Fin \land A ≼ B) \to \neg B ≺ A$
7	6	ex	$⊢ A \in Fin \to (A ≼ B \to \neg B ≺ A)$
8		php3	$⊢ (A \in Fin \land B \subset A) \to B ≺ A$
9	8	ex	$⊢ A \in Fin \to (B \subset A \to B ≺ A)$
10	7 9	nsyld	$⊢ A \in Fin \to (A ≼ B \to \neg B \subset A)$
11	10	adantl	$⊢ (B \in ω \land A \in Fin) \to (A ≼ B \to \neg B \subset A)$
12	11	expimpd	$⊢ B \in ω \to ((A \in Fin \land A ≼ B) \to \neg B \subset A)$
13	5 12	syl5	$⊢ B \in ω \to ((B \in Fin \land A ≼ B) \to \neg B \subset A)$
14	2 13	mpand	$⊢ B \in ω \to (A ≼ B \to \neg B \subset A)$
15	14	adantl	$⊢ (A \in On \land B \in ω) \to (A ≼ B \to \neg B \subset A)$
16		eloni	$⊢ A \in On \to Ord A$
17		nnord	$⊢ B \in ω \to Ord B$
18		ordtri1	$⊢ (Ord A \land Ord B) \to (A \subseteq B \leftrightarrow \neg B \in A)$
19		ordelpss	$⊢ (Ord B \land Ord A) \to (B \in A \leftrightarrow B \subset A)$
20	19	ancoms	$⊢ (Ord A \land Ord B) \to (B \in A \leftrightarrow B \subset A)$
21	20	notbid	$⊢ (Ord A \land Ord B) \to (\neg B \in A \leftrightarrow \neg B \subset A)$
22	18 21	bitrd	$⊢ (Ord A \land Ord B) \to (A \subseteq B \leftrightarrow \neg B \subset A)$
23	16 17 22	syl2an	$⊢ (A \in On \land B \in ω) \to (A \subseteq B \leftrightarrow \neg B \subset A)$
24	15 23	sylibrd	$⊢ (A \in On \land B \in ω) \to (A ≼ B \to A \subseteq B)$
25	1 24	syl5	$⊢ (A \in On \land B \in ω) \to (A \approx B \to A \subseteq B)$
26	25	3impia	$⊢ (A \in On \land B \in ω \land A \approx B) \to A \subseteq B$
27		ensymfib	$⊢ B \in Fin \to (B \approx A \leftrightarrow A \approx B)$
28	2 27	syl	$⊢ B \in ω \to (B \approx A \leftrightarrow A \approx B)$
29		endom	$⊢ B \approx A \to B ≼ A$
30	28 29	biimtrrdi	$⊢ B \in ω \to (A \approx B \to B ≼ A)$
31	30	imp	$⊢ (B \in ω \land A \approx B) \to B ≼ A$
32	31	3adant1	$⊢ (A \in On \land B \in ω \land A \approx B) \to B ≼ A$
33		nndomog	$⊢ (B \in ω \land A \in On) \to (B ≼ A \leftrightarrow B \subseteq A)$
34	33	ancoms	$⊢ (A \in On \land B \in ω) \to (B ≼ A \leftrightarrow B \subseteq A)$
35	34	biimp3a	$⊢ (A \in On \land B \in ω \land B ≼ A) \to B \subseteq A$
36	32 35	syld3an3	$⊢ (A \in On \land B \in ω \land A \approx B) \to B \subseteq A$
37	26 36	eqssd	$⊢ (A \in On \land B \in ω \land A \approx B) \to A = B$
38	37	3expia	$⊢ (A \in On \land B \in ω) \to (A \approx B \to A = B)$
39		enrefnn	$⊢ B \in ω \to B \approx B$
40		breq1	$⊢ A = B \to (A \approx B \leftrightarrow B \approx B)$
41	39 40	syl5ibrcom	$⊢ B \in ω \to (A = B \to A \approx B)$
42	41	adantl	$⊢ (A \in On \land B \in ω) \to (A = B \to A \approx B)$
43	38 42	impbid	$⊢ (A \in On \land B \in ω) \to (A \approx B \leftrightarrow A = B)$

Metamath Proof Explorer

Theorem onomeneq

Proof