alephiso3

Description: aleph is a strictly order-preserving mapping of On onto the class of all infinite cardinal numbers. (Contributed by RP, 18-Nov-2023)

		Ref	Expression
	Assertion	alephiso3	$⊢ ℵ {Isom}_{E, ≺} (On, ran card ∖ ω)$

Step	Hyp	Ref	Expression
1		alephiso2	$⊢ ℵ {Isom}_{E, ≺} (On, \{x \in ran card \| ω \subseteq x\})$
2		omelon	$⊢ ω \in On$
3		elrncard	$⊢ x \in ran card \leftrightarrow (x \in On \land \forall y \in x \neg y \approx x)$
4	3	simplbi	$⊢ x \in ran card \to x \in On$
5		ontri1	$⊢ (ω \in On \land x \in On) \to (ω \subseteq x \leftrightarrow \neg x \in ω)$
6	2 4 5	sylancr	$⊢ x \in ran card \to (ω \subseteq x \leftrightarrow \neg x \in ω)$
7	6	rabbiia	$⊢ \{x \in ran card \| ω \subseteq x\} = \{x \in ran card \| \neg x \in ω\}$
8		dfdif2	$⊢ ran card ∖ ω = \{x \in ran card \| \neg x \in ω\}$
9	7 8	eqtr4i	$⊢ \{x \in ran card \| ω \subseteq x\} = ran card ∖ ω$
10		isoeq5	$⊢ \{x \in ran card \| ω \subseteq x\} = ran card ∖ ω \to (ℵ {Isom}_{E, ≺} (On, \{x \in ran card \| ω \subseteq x\}) \leftrightarrow ℵ {Isom}_{E, ≺} (On, ran card ∖ ω))$
11	9 10	ax-mp	$⊢ ℵ {Isom}_{E, ≺} (On, \{x \in ran card \| ω \subseteq x\}) \leftrightarrow ℵ {Isom}_{E, ≺} (On, ran card ∖ ω)$
12	1 11	mpbi	$⊢ ℵ {Isom}_{E, ≺} (On, ran card ∖ ω)$

Metamath Proof Explorer