cardf2

Description: The cardinality function is a function with domain the well-orderable sets. Assuming AC, this is the universe. (Contributed by Mario Carneiro, 6-Jun-2013) (Revised by Mario Carneiro, 20-Sep-2014)

		Ref	Expression
	Assertion	cardf2	$⊢ card : \{x \| \exists y \in On y \approx x\} ⟶ On$

Proof

Step	Hyp	Ref	Expression
1		df-card	$⊢ card = (x \in V ⟼ ⋂ \{y \in On \| y \approx x\})$
2	1	funmpt2	$⊢ Fun card$
3		rabab	$⊢ \{x \in V \| ⋂ \{y \in On \| y \approx x\} \in V\} = \{x \| ⋂ \{y \in On \| y \approx x\} \in V\}$
4	1	dmmpt	$⊢ dom card = \{x \in V \| ⋂ \{y \in On \| y \approx x\} \in V\}$
5		intexrab	$⊢ \exists y \in On y \approx x \leftrightarrow ⋂ \{y \in On \| y \approx x\} \in V$
6	5	abbii	$⊢ \{x \| \exists y \in On y \approx x\} = \{x \| ⋂ \{y \in On \| y \approx x\} \in V\}$
7	3 4 6	3eqtr4i	$⊢ dom card = \{x \| \exists y \in On y \approx x\}$
8		df-fn	$⊢ card Fn \{x \| \exists y \in On y \approx x\} \leftrightarrow (Fun card \land dom card = \{x \| \exists y \in On y \approx x\})$
9	2 7 8	mpbir2an	$⊢ card Fn \{x \| \exists y \in On y \approx x\}$
10		simpr	$⊢ (z \in V \land w = ⋂ \{y \in On \| y \approx z\}) \to w = ⋂ \{y \in On \| y \approx z\}$
11		vex	$⊢ w \in V$
12	10 11	eqeltrrdi	$⊢ (z \in V \land w = ⋂ \{y \in On \| y \approx z\}) \to ⋂ \{y \in On \| y \approx z\} \in V$
13		intex	$⊢ \{y \in On \| y \approx z\} \neq \emptyset \leftrightarrow ⋂ \{y \in On \| y \approx z\} \in V$
14	12 13	sylibr	$⊢ (z \in V \land w = ⋂ \{y \in On \| y \approx z\}) \to \{y \in On \| y \approx z\} \neq \emptyset$
15		rabn0	$⊢ \{y \in On \| y \approx z\} \neq \emptyset \leftrightarrow \exists y \in On y \approx z$
16	14 15	sylib	$⊢ (z \in V \land w = ⋂ \{y \in On \| y \approx z\}) \to \exists y \in On y \approx z$
17		vex	$⊢ z \in V$
18		breq2	$⊢ x = z \to (y \approx x \leftrightarrow y \approx z)$
19	18	rexbidv	$⊢ x = z \to (\exists y \in On y \approx x \leftrightarrow \exists y \in On y \approx z)$
20	17 19	elab	$⊢ z \in \{x \| \exists y \in On y \approx x\} \leftrightarrow \exists y \in On y \approx z$
21	16 20	sylibr	$⊢ (z \in V \land w = ⋂ \{y \in On \| y \approx z\}) \to z \in \{x \| \exists y \in On y \approx x\}$
22		ssrab2	$⊢ \{y \in On \| y \approx z\} \subseteq On$
23		oninton	$⊢ (\{y \in On \| y \approx z\} \subseteq On \land \{y \in On \| y \approx z\} \neq \emptyset) \to ⋂ \{y \in On \| y \approx z\} \in On$
24	22 14 23	sylancr	$⊢ (z \in V \land w = ⋂ \{y \in On \| y \approx z\}) \to ⋂ \{y \in On \| y \approx z\} \in On$
25	10 24	eqeltrd	$⊢ (z \in V \land w = ⋂ \{y \in On \| y \approx z\}) \to w \in On$
26	21 25	jca	$⊢ (z \in V \land w = ⋂ \{y \in On \| y \approx z\}) \to (z \in \{x \| \exists y \in On y \approx x\} \land w \in On)$
27	26	ssopab2i	$⊢ \{⟨z, w⟩ \| (z \in V \land w = ⋂ \{y \in On \| y \approx z\})\} \subseteq \{⟨z, w⟩ \| (z \in \{x \| \exists y \in On y \approx x\} \land w \in On)\}$
28		df-card	$⊢ card = (z \in V ⟼ ⋂ \{y \in On \| y \approx z\})$
29		df-mpt	$⊢ (z \in V ⟼ ⋂ \{y \in On \| y \approx z\}) = \{⟨z, w⟩ \| (z \in V \land w = ⋂ \{y \in On \| y \approx z\})\}$
30	28 29	eqtri	$⊢ card = \{⟨z, w⟩ \| (z \in V \land w = ⋂ \{y \in On \| y \approx z\})\}$
31		df-xp	$⊢ \{x \| \exists y \in On y \approx x\} \times On = \{⟨z, w⟩ \| (z \in \{x \| \exists y \in On y \approx x\} \land w \in On)\}$
32	27 30 31	3sstr4i	$⊢ card \subseteq \{x \| \exists y \in On y \approx x\} \times On$
33		dff2	$⊢ card : \{x \| \exists y \in On y \approx x\} ⟶ On \leftrightarrow (card Fn \{x \| \exists y \in On y \approx x\} \land card \subseteq \{x \| \exists y \in On y \approx x\} \times On)$
34	9 32 33	mpbir2an	$⊢ card : \{x \| \exists y \in On y \approx x\} ⟶ On$

Metamath Proof Explorer

Theorem cardf2

Proof