card2on

Description: The alternate definition of the cardinal of a set given in cardval2 always gives a set, and indeed an ordinal. (Contributed by Mario Carneiro, 14-Jan-2013)

		Ref	Expression
	Assertion	card2on	$⊢ \{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		domsdomtr	$⊢ (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		hartogs	$⊢ A \in V \to \{x \in On \| x ≼ A\} \in On$
29		sdomdom	$⊢ x ≺ A \to x ≼ A$
30	29	a1i	$⊢ x \in On \to (x ≺ A \to x ≼ A)$
31	30	ss2rabi	$⊢ \{x \in On \| x ≺ A\} \subseteq \{x \in On \| x ≼ A\}$
32		ssexg	$⊢ (\{x \in On \| x ≺ A\} \subseteq \{x \in On \| x ≼ A\} \land \{x \in On \| x ≼ A\} \in On) \to \{x \in On \| x ≺ A\} \in V$
33	31 32	mpan	$⊢ \{x \in On \| x ≼ A\} \in On \to \{x \in On \| x ≺ A\} \in V$
34		elong	$⊢ \{x \in On \| x ≺ A\} \in V \to (\{x \in On \| x ≺ A\} \in On \leftrightarrow Ord \{x \in On \| x ≺ A\})$
35	28 33 34	3syl	$⊢ A \in V \to (\{x \in On \| x ≺ A\} \in On \leftrightarrow Ord \{x \in On \| x ≺ A\})$
36	27 35	mpbiri	$⊢ A \in V \to \{x \in On \| x ≺ A\} \in On$
37		0elon	$⊢ \emptyset \in On$
38		eleq1	$⊢ \{x \in On \| x ≺ A\} = \emptyset \to (\{x \in On \| x ≺ A\} \in On \leftrightarrow \emptyset \in On)$
39	37 38	mpbiri	$⊢ \{x \in On \| x ≺ A\} = \emptyset \to \{x \in On \| x ≺ A\} \in On$
40		df-ne	$⊢ \{x \in On \| x ≺ A\} \neq \emptyset \leftrightarrow \neg \{x \in On \| x ≺ A\} = \emptyset$
41		rabn0	$⊢ \{x \in On \| x ≺ A\} \neq \emptyset \leftrightarrow \exists x \in On x ≺ A$
42	40 41	bitr3i	$⊢ \neg \{x \in On \| x ≺ A\} = \emptyset \leftrightarrow \exists x \in On x ≺ A$
43		relsdom	$⊢ Rel ≺$
44	43	brrelex2i	$⊢ x ≺ A \to A \in V$
45	44	rexlimivw	$⊢ \exists x \in On x ≺ A \to A \in V$
46	42 45	sylbi	$⊢ \neg \{x \in On \| x ≺ A\} = \emptyset \to A \in V$
47	39 46	nsyl4	$⊢ \neg A \in V \to \{x \in On \| x ≺ A\} \in On$
48	36 47	pm2.61i	$⊢ \{x \in On \| x ≺ A\} \in On$

Metamath Proof Explorer

Theorem card2on

Proof