hartogs

Description: The class of ordinals dominated by a given set is an ordinal. A shorter (when taking into account lemmas hartogslem1 and hartogslem2 ) proof can be given using the axiom of choice, see ondomon . As its label indicates, this result is used to justify the definition of the Hartogs function df-har . (Contributed by Jeff Hankins, 22-Oct-2009) (Revised by Mario Carneiro, 15-May-2015)

		Ref	Expression
	Assertion	hartogs	$⊢ A \in V \to \{x \in On \| x ≼ A\} \in On$

Proof

Step	Hyp	Ref	Expression
1		onelon	$⊢ (z \in On \land y \in z) \to y \in On$
2		vex	$⊢ z \in V$
3		onelss	$⊢ z \in On \to (y \in z \to y \subseteq z)$
4	3	imp	$⊢ (z \in On \land y \in z) \to y \subseteq z$
5		ssdomg	$⊢ z \in V \to (y \subseteq z \to y ≼ z)$
6	2 4 5	mpsyl	$⊢ (z \in On \land y \in z) \to y ≼ z$
7	1 6	jca	$⊢ (z \in On \land y \in z) \to (y \in On \land y ≼ z)$
8		domtr	$⊢ (y ≼ z \land z ≼ A) \to y ≼ A$
9	8	anim2i	$⊢ (y \in On \land (y ≼ z \land z ≼ A)) \to (y \in On \land y ≼ A)$
10	9	anassrs	$⊢ ((y \in On \land y ≼ z) \land z ≼ A) \to (y \in On \land y ≼ A)$
11	7 10	sylan	$⊢ ((z \in On \land y \in z) \land z ≼ A) \to (y \in On \land y ≼ A)$
12	11	exp31	$⊢ z \in On \to (y \in z \to (z ≼ A \to (y \in On \land y ≼ A)))$
13	12	com12	$⊢ y \in z \to (z \in On \to (z ≼ A \to (y \in On \land y ≼ A)))$
14	13	impd	$⊢ y \in z \to ((z \in On \land z ≼ A) \to (y \in On \land y ≼ A))$
15		breq1	$⊢ x = z \to (x ≼ A \leftrightarrow z ≼ A)$
16	15	elrab	$⊢ z \in \{x \in On \| x ≼ A\} \leftrightarrow (z \in On \land z ≼ A)$
17		breq1	$⊢ x = y \to (x ≼ A \leftrightarrow y ≼ A)$
18	17	elrab	$⊢ y \in \{x \in On \| x ≼ A\} \leftrightarrow (y \in On \land y ≼ A)$
19	14 16 18	3imtr4g	$⊢ y \in z \to (z \in \{x \in On \| x ≼ A\} \to y \in \{x \in On \| x ≼ A\})$
20	19	imp	$⊢ (y \in z \land z \in \{x \in On \| x ≼ A\}) \to y \in \{x \in On \| x ≼ A\}$
21	20	gen2	$⊢ \forall y \forall z ((y \in z \land z \in \{x \in On \| x ≼ A\}) \to y \in \{x \in On \| x ≼ A\})$
22		dftr2	$⊢ Tr \{x \in On \| x ≼ A\} \leftrightarrow \forall y \forall z ((y \in z \land z \in \{x \in On \| x ≼ A\}) \to y \in \{x \in On \| x ≼ A\})$
23	21 22	mpbir	$⊢ Tr \{x \in On \| x ≼ A\}$
24		ssrab2	$⊢ \{x \in On \| x ≼ A\} \subseteq On$
25		ordon	$⊢ Ord On$
26		trssord	$⊢ (Tr \{x \in On \| x ≼ A\} \land \{x \in On \| x ≼ A\} \subseteq On \land Ord On) \to Ord \{x \in On \| x ≼ A\}$
27	23 24 25 26	mp3an	$⊢ Ord \{x \in On \| x ≼ A\}$
28		eqid	$⊢ \{⟨r, y⟩ \| (((dom r \subseteq A \land {I ↾}_{dom r} \subseteq r \land r \subseteq dom r \times dom r) \land (r ∖ I) We dom r) \land y = dom OrdIso (r ∖ I, dom r))\} = \{⟨r, y⟩ \| (((dom r \subseteq A \land {I ↾}_{dom r} \subseteq r \land r \subseteq dom r \times dom r) \land (r ∖ I) We dom r) \land y = dom OrdIso (r ∖ I, dom r))\}$
29		eqid	$⊢ \{⟨s, t⟩ \| \exists w \in y \exists z \in y ((s = g (w) \land t = g (z)) \land w E z)\} = \{⟨s, t⟩ \| \exists w \in y \exists z \in y ((s = g (w) \land t = g (z)) \land w E z)\}$
30	28 29	hartogslem2	$⊢ A \in V \to \{x \in On \| x ≼ A\} \in V$
31		elong	$⊢ \{x \in On \| x ≼ A\} \in V \to (\{x \in On \| x ≼ A\} \in On \leftrightarrow Ord \{x \in On \| x ≼ A\})$
32	30 31	syl	$⊢ A \in V \to (\{x \in On \| x ≼ A\} \in On \leftrightarrow Ord \{x \in On \| x ≼ A\})$
33	27 32	mpbiri	$⊢ A \in V \to \{x \in On \| x ≼ A\} \in On$

Metamath Proof Explorer

Theorem hartogs

Proof