cardmin2

Description: The smallest ordinal that strictly dominates a set is a cardinal, if it exists. (Contributed by Mario Carneiro, 2-Feb-2013)

		Ref	Expression
	Assertion	cardmin2	$⊢ \exists x \in On A ≺ x \leftrightarrow card (⋂ \{x \in On \| A ≺ x\}) = ⋂ \{x \in On \| A ≺ x\}$

Proof

Step	Hyp	Ref	Expression
1		onintrab2	$⊢ \exists x \in On A ≺ x \leftrightarrow ⋂ \{x \in On \| A ≺ x\} \in On$
2	1	biimpi	$⊢ \exists x \in On A ≺ x \to ⋂ \{x \in On \| A ≺ x\} \in On$
3	1	birani	$⊢ (\exists x \in On A ≺ x \land y \in ⋂ \{x \in On \| A ≺ x\}) \to ⋂ \{x \in On \| A ≺ x\} \in On$
4		eloni	$⊢ ⋂ \{x \in On \| A ≺ x\} \in On \to Ord ⋂ \{x \in On \| A ≺ x\}$
5		ordelss	$⊢ (Ord ⋂ \{x \in On \| A ≺ x\} \land y \in ⋂ \{x \in On \| A ≺ x\}) \to y \subseteq ⋂ \{x \in On \| A ≺ x\}$
6	4 5	sylan	$⊢ (⋂ \{x \in On \| A ≺ x\} \in On \land y \in ⋂ \{x \in On \| A ≺ x\}) \to y \subseteq ⋂ \{x \in On \| A ≺ x\}$
7	1 6	sylanb	$⊢ (\exists x \in On A ≺ x \land y \in ⋂ \{x \in On \| A ≺ x\}) \to y \subseteq ⋂ \{x \in On \| A ≺ x\}$
8		ssdomg	$⊢ ⋂ \{x \in On \| A ≺ x\} \in On \to (y \subseteq ⋂ \{x \in On \| A ≺ x\} \to y ≼ ⋂ \{x \in On \| A ≺ x\})$
9	3 7 8	sylc	$⊢ (\exists x \in On A ≺ x \land y \in ⋂ \{x \in On \| A ≺ x\}) \to y ≼ ⋂ \{x \in On \| A ≺ x\}$
10		onelon	$⊢ (⋂ \{x \in On \| A ≺ x\} \in On \land y \in ⋂ \{x \in On \| A ≺ x\}) \to y \in On$
11	1 10	sylanb	$⊢ (\exists x \in On A ≺ x \land y \in ⋂ \{x \in On \| A ≺ x\}) \to y \in On$
12		nfcv	$⊢ \underline{Ⅎ} x A$
13		nfcv	$⊢ \underline{Ⅎ} x ≺$
14		nfrab1	$⊢ \underline{Ⅎ} x \{x \in On \| A ≺ x\}$
15	14	nfint	$⊢ \underline{Ⅎ} x ⋂ \{x \in On \| A ≺ x\}$
16	12 13 15	nfbr	$⊢ Ⅎ x A ≺ ⋂ \{x \in On \| A ≺ x\}$
17		breq2	$⊢ x = ⋂ \{x \in On \| A ≺ x\} \to (A ≺ x \leftrightarrow A ≺ ⋂ \{x \in On \| A ≺ x\})$
18	16 17	onminsb	$⊢ \exists x \in On A ≺ x \to A ≺ ⋂ \{x \in On \| A ≺ x\}$
19		sdomentr	$⊢ (A ≺ ⋂ \{x \in On \| A ≺ x\} \land ⋂ \{x \in On \| A ≺ x\} \approx y) \to A ≺ y$
20	18 19	sylan	$⊢ (\exists x \in On A ≺ x \land ⋂ \{x \in On \| A ≺ x\} \approx y) \to A ≺ y$
21		breq2	$⊢ x = y \to (A ≺ x \leftrightarrow A ≺ y)$
22	21	elrab	$⊢ y \in \{x \in On \| A ≺ x\} \leftrightarrow (y \in On \land A ≺ y)$
23		ssrab2	$⊢ \{x \in On \| A ≺ x\} \subseteq On$
24		onnmin	$⊢ (\{x \in On \| A ≺ x\} \subseteq On \land y \in \{x \in On \| A ≺ x\}) \to \neg y \in ⋂ \{x \in On \| A ≺ x\}$
25	23 24	mpan	$⊢ y \in \{x \in On \| A ≺ x\} \to \neg y \in ⋂ \{x \in On \| A ≺ x\}$
26	22 25	sylbir	$⊢ (y \in On \land A ≺ y) \to \neg y \in ⋂ \{x \in On \| A ≺ x\}$
27	26	expcom	$⊢ A ≺ y \to (y \in On \to \neg y \in ⋂ \{x \in On \| A ≺ x\})$
28	20 27	syl	$⊢ (\exists x \in On A ≺ x \land ⋂ \{x \in On \| A ≺ x\} \approx y) \to (y \in On \to \neg y \in ⋂ \{x \in On \| A ≺ x\})$
29	28	impancom	$⊢ (\exists x \in On A ≺ x \land y \in On) \to (⋂ \{x \in On \| A ≺ x\} \approx y \to \neg y \in ⋂ \{x \in On \| A ≺ x\})$
30	29	con2d	$⊢ (\exists x \in On A ≺ x \land y \in On) \to (y \in ⋂ \{x \in On \| A ≺ x\} \to \neg ⋂ \{x \in On \| A ≺ x\} \approx y)$
31	30	impancom	$⊢ (\exists x \in On A ≺ x \land y \in ⋂ \{x \in On \| A ≺ x\}) \to (y \in On \to \neg ⋂ \{x \in On \| A ≺ x\} \approx y)$
32	11 31	mpd	$⊢ (\exists x \in On A ≺ x \land y \in ⋂ \{x \in On \| A ≺ x\}) \to \neg ⋂ \{x \in On \| A ≺ x\} \approx y$
33		ensym	$⊢ y \approx ⋂ \{x \in On \| A ≺ x\} \to ⋂ \{x \in On \| A ≺ x\} \approx y$
34	32 33	nsyl	$⊢ (\exists x \in On A ≺ x \land y \in ⋂ \{x \in On \| A ≺ x\}) \to \neg y \approx ⋂ \{x \in On \| A ≺ x\}$
35		brsdom	$⊢ y ≺ ⋂ \{x \in On \| A ≺ x\} \leftrightarrow (y ≼ ⋂ \{x \in On \| A ≺ x\} \land \neg y \approx ⋂ \{x \in On \| A ≺ x\})$
36	9 34 35	sylanbrc	$⊢ (\exists x \in On A ≺ x \land y \in ⋂ \{x \in On \| A ≺ x\}) \to y ≺ ⋂ \{x \in On \| A ≺ x\}$
37	36	ralrimiva	$⊢ \exists x \in On A ≺ x \to \forall y \in ⋂ \{x \in On \| A ≺ x\} y ≺ ⋂ \{x \in On \| A ≺ x\}$
38		iscard	$⊢ card (⋂ \{x \in On \| A ≺ x\}) = ⋂ \{x \in On \| A ≺ x\} \leftrightarrow (⋂ \{x \in On \| A ≺ x\} \in On \land \forall y \in ⋂ \{x \in On \| A ≺ x\} y ≺ ⋂ \{x \in On \| A ≺ x\})$
39	2 37 38	sylanbrc	$⊢ \exists x \in On A ≺ x \to card (⋂ \{x \in On \| A ≺ x\}) = ⋂ \{x \in On \| A ≺ x\}$
40		vprc	$⊢ \neg V \in V$
41		inteq	$⊢ \{x \in On \| A ≺ x\} = \emptyset \to ⋂ \{x \in On \| A ≺ x\} = ⋂ \emptyset$
42		int0	$⊢ ⋂ \emptyset = V$
43	41 42	eqtrdi	$⊢ \{x \in On \| A ≺ x\} = \emptyset \to ⋂ \{x \in On \| A ≺ x\} = V$
44	43	eleq1d	$⊢ \{x \in On \| A ≺ x\} = \emptyset \to (⋂ \{x \in On \| A ≺ x\} \in V \leftrightarrow V \in V)$
45	40 44	mtbiri	$⊢ \{x \in On \| A ≺ x\} = \emptyset \to \neg ⋂ \{x \in On \| A ≺ x\} \in V$
46		fvex	$⊢ card (⋂ \{x \in On \| A ≺ x\}) \in V$
47		eleq1	$⊢ card (⋂ \{x \in On \| A ≺ x\}) = ⋂ \{x \in On \| A ≺ x\} \to (card (⋂ \{x \in On \| A ≺ x\}) \in V \leftrightarrow ⋂ \{x \in On \| A ≺ x\} \in V)$
48	46 47	mpbii	$⊢ card (⋂ \{x \in On \| A ≺ x\}) = ⋂ \{x \in On \| A ≺ x\} \to ⋂ \{x \in On \| A ≺ x\} \in V$
49	45 48	nsyl	$⊢ \{x \in On \| A ≺ x\} = \emptyset \to \neg card (⋂ \{x \in On \| A ≺ x\}) = ⋂ \{x \in On \| A ≺ x\}$
50	49	necon2ai	$⊢ card (⋂ \{x \in On \| A ≺ x\}) = ⋂ \{x \in On \| A ≺ x\} \to \{x \in On \| A ≺ x\} \neq \emptyset$
51		rabn0	$⊢ \{x \in On \| A ≺ x\} \neq \emptyset \leftrightarrow \exists x \in On A ≺ x$
52	50 51	sylib	$⊢ card (⋂ \{x \in On \| A ≺ x\}) = ⋂ \{x \in On \| A ≺ x\} \to \exists x \in On A ≺ x$
53	39 52	impbii	$⊢ \exists x \in On A ≺ x \leftrightarrow card (⋂ \{x \in On \| A ≺ x\}) = ⋂ \{x \in On \| A ≺ x\}$

Metamath Proof Explorer

Theorem cardmin2

Proof