harsucnn

Description: The next cardinal after a finite ordinal is the successor ordinal. (Contributed by RP, 5-Nov-2023)

		Ref	Expression
	Assertion	harsucnn	$⊢ A \in ω \to har (A) = suc A$

Step	Hyp	Ref	Expression
1		nnon	$⊢ A \in ω \to A \in On$
2		onenon	$⊢ A \in On \to A \in dom card$
3		harval2	$⊢ A \in dom card \to har (A) = ⋂ \{x \in On \| A ≺ x\}$
4	1 2 3	3syl	$⊢ A \in ω \to har (A) = ⋂ \{x \in On \| A ≺ x\}$
5		sucdom	$⊢ A \in ω \to (A ≺ x \leftrightarrow suc A ≼ x)$
6	5	adantr	$⊢ (A \in ω \land x \in On) \to (A ≺ x \leftrightarrow suc A ≼ x)$
7		peano2	$⊢ A \in ω \to suc A \in ω$
8		nndomog	$⊢ (suc A \in ω \land x \in On) \to (suc A ≼ x \leftrightarrow suc A \subseteq x)$
9	7 8	sylan	$⊢ (A \in ω \land x \in On) \to (suc A ≼ x \leftrightarrow suc A \subseteq x)$
10	6 9	bitrd	$⊢ (A \in ω \land x \in On) \to (A ≺ x \leftrightarrow suc A \subseteq x)$
11	10	rabbidva	$⊢ A \in ω \to \{x \in On \| A ≺ x\} = \{x \in On \| suc A \subseteq x\}$
12	11	inteqd	$⊢ A \in ω \to ⋂ \{x \in On \| A ≺ x\} = ⋂ \{x \in On \| suc A \subseteq x\}$
13		nnon	$⊢ suc A \in ω \to suc A \in On$
14		intmin	$⊢ suc A \in On \to ⋂ \{x \in On \| suc A \subseteq x\} = suc A$
15	7 13 14	3syl	$⊢ A \in ω \to ⋂ \{x \in On \| suc A \subseteq x\} = suc A$
16	4 12 15	3eqtrd	$⊢ A \in ω \to har (A) = suc A$

Metamath Proof Explorer