rankf

Description: The domain and range of the rank function. (Contributed by Mario Carneiro, 28-May-2013) (Revised by Mario Carneiro, 12-Sep-2013)

		Ref	Expression
	Assertion	rankf	$⊢ rank : ⋃ R_{1} [On] ⟶ On$

Proof

Step	Hyp	Ref	Expression
1		df-rank	$⊢ rank = (x \in V ⟼ ⋂ \{y \in On \| x \in R_{1} (suc y)\})$
2	1	funmpt2	$⊢ Fun rank$
3		mptv	$⊢ (x \in V ⟼ ⋂ \{y \in On \| x \in R_{1} (suc y)\}) = \{⟨x, z⟩ \| z = ⋂ \{y \in On \| x \in R_{1} (suc y)\}\}$
4	1 3	eqtri	$⊢ rank = \{⟨x, z⟩ \| z = ⋂ \{y \in On \| x \in R_{1} (suc y)\}\}$
5	4	dmeqi	$⊢ dom rank = dom \{⟨x, z⟩ \| z = ⋂ \{y \in On \| x \in R_{1} (suc y)\}\}$
6		dmopab	$⊢ dom \{⟨x, z⟩ \| z = ⋂ \{y \in On \| x \in R_{1} (suc y)\}\} = \{x \| \exists z z = ⋂ \{y \in On \| x \in R_{1} (suc y)\}\}$
7		abeq1	$⊢ \{x \| \exists z z = ⋂ \{y \in On \| x \in R_{1} (suc y)\}\} = ⋃ R_{1} [On] \leftrightarrow \forall x (\exists z z = ⋂ \{y \in On \| x \in R_{1} (suc y)\} \leftrightarrow x \in ⋃ R_{1} [On])$
8		rankwflemb	$⊢ x \in ⋃ R_{1} [On] \leftrightarrow \exists y \in On x \in R_{1} (suc y)$
9		intexrab	$⊢ \exists y \in On x \in R_{1} (suc y) \leftrightarrow ⋂ \{y \in On \| x \in R_{1} (suc y)\} \in V$
10		isset	$⊢ ⋂ \{y \in On \| x \in R_{1} (suc y)\} \in V \leftrightarrow \exists z z = ⋂ \{y \in On \| x \in R_{1} (suc y)\}$
11	8 9 10	3bitrri	$⊢ \exists z z = ⋂ \{y \in On \| x \in R_{1} (suc y)\} \leftrightarrow x \in ⋃ R_{1} [On]$
12	7 11	mpgbir	$⊢ \{x \| \exists z z = ⋂ \{y \in On \| x \in R_{1} (suc y)\}\} = ⋃ R_{1} [On]$
13	6 12	eqtri	$⊢ dom \{⟨x, z⟩ \| z = ⋂ \{y \in On \| x \in R_{1} (suc y)\}\} = ⋃ R_{1} [On]$
14	5 13	eqtri	$⊢ dom rank = ⋃ R_{1} [On]$
15		df-fn	$⊢ rank Fn ⋃ R_{1} [On] \leftrightarrow (Fun rank \land dom rank = ⋃ R_{1} [On])$
16	2 14 15	mpbir2an	$⊢ rank Fn ⋃ R_{1} [On]$
17		rabn0	$⊢ \{y \in On \| x \in R_{1} (suc y)\} \neq \emptyset \leftrightarrow \exists y \in On x \in R_{1} (suc y)$
18	8 17	bitr4i	$⊢ x \in ⋃ R_{1} [On] \leftrightarrow \{y \in On \| x \in R_{1} (suc y)\} \neq \emptyset$
19		intex	$⊢ \{y \in On \| x \in R_{1} (suc y)\} \neq \emptyset \leftrightarrow ⋂ \{y \in On \| x \in R_{1} (suc y)\} \in V$
20		vex	$⊢ x \in V$
21	1	fvmpt2	$⊢ (x \in V \land ⋂ \{y \in On \| x \in R_{1} (suc y)\} \in V) \to rank (x) = ⋂ \{y \in On \| x \in R_{1} (suc y)\}$
22	20 21	mpan	$⊢ ⋂ \{y \in On \| x \in R_{1} (suc y)\} \in V \to rank (x) = ⋂ \{y \in On \| x \in R_{1} (suc y)\}$
23	19 22	sylbi	$⊢ \{y \in On \| x \in R_{1} (suc y)\} \neq \emptyset \to rank (x) = ⋂ \{y \in On \| x \in R_{1} (suc y)\}$
24		ssrab2	$⊢ \{y \in On \| x \in R_{1} (suc y)\} \subseteq On$
25		oninton	$⊢ (\{y \in On \| x \in R_{1} (suc y)\} \subseteq On \land \{y \in On \| x \in R_{1} (suc y)\} \neq \emptyset) \to ⋂ \{y \in On \| x \in R_{1} (suc y)\} \in On$
26	24 25	mpan	$⊢ \{y \in On \| x \in R_{1} (suc y)\} \neq \emptyset \to ⋂ \{y \in On \| x \in R_{1} (suc y)\} \in On$
27	23 26	eqeltrd	$⊢ \{y \in On \| x \in R_{1} (suc y)\} \neq \emptyset \to rank (x) \in On$
28	18 27	sylbi	$⊢ x \in ⋃ R_{1} [On] \to rank (x) \in On$
29	28	rgen	$⊢ \forall x \in ⋃ R_{1} [On] rank (x) \in On$
30		ffnfv	$⊢ rank : ⋃ R_{1} [On] ⟶ On \leftrightarrow (rank Fn ⋃ R_{1} [On] \land \forall x \in ⋃ R_{1} [On] rank (x) \in On)$
31	16 29 30	mpbir2an	$⊢ rank : ⋃ R_{1} [On] ⟶ On$

Metamath Proof Explorer

Theorem rankf

Proof