# Metamath Proof Explorer

## Theorem 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 ${⊢}\mathrm{rank}:\bigcup {R}_{1}\left[\mathrm{On}\right]⟶\mathrm{On}$

### Proof

Step Hyp Ref Expression
1 df-rank ${⊢}\mathrm{rank}=\left({x}\in \mathrm{V}⟼\bigcap \left\{{y}\in \mathrm{On}|{x}\in {R}_{1}\left(\mathrm{suc}{y}\right)\right\}\right)$
2 1 funmpt2 ${⊢}\mathrm{Fun}\mathrm{rank}$
3 mptv ${⊢}\left({x}\in \mathrm{V}⟼\bigcap \left\{{y}\in \mathrm{On}|{x}\in {R}_{1}\left(\mathrm{suc}{y}\right)\right\}\right)=\left\{⟨{x},{z}⟩|{z}=\bigcap \left\{{y}\in \mathrm{On}|{x}\in {R}_{1}\left(\mathrm{suc}{y}\right)\right\}\right\}$
4 1 3 eqtri ${⊢}\mathrm{rank}=\left\{⟨{x},{z}⟩|{z}=\bigcap \left\{{y}\in \mathrm{On}|{x}\in {R}_{1}\left(\mathrm{suc}{y}\right)\right\}\right\}$
5 4 dmeqi ${⊢}\mathrm{dom}\mathrm{rank}=\mathrm{dom}\left\{⟨{x},{z}⟩|{z}=\bigcap \left\{{y}\in \mathrm{On}|{x}\in {R}_{1}\left(\mathrm{suc}{y}\right)\right\}\right\}$
6 dmopab ${⊢}\mathrm{dom}\left\{⟨{x},{z}⟩|{z}=\bigcap \left\{{y}\in \mathrm{On}|{x}\in {R}_{1}\left(\mathrm{suc}{y}\right)\right\}\right\}=\left\{{x}|\exists {z}\phantom{\rule{.4em}{0ex}}{z}=\bigcap \left\{{y}\in \mathrm{On}|{x}\in {R}_{1}\left(\mathrm{suc}{y}\right)\right\}\right\}$
7 abeq1 ${⊢}\left\{{x}|\exists {z}\phantom{\rule{.4em}{0ex}}{z}=\bigcap \left\{{y}\in \mathrm{On}|{x}\in {R}_{1}\left(\mathrm{suc}{y}\right)\right\}\right\}=\bigcup {R}_{1}\left[\mathrm{On}\right]↔\forall {x}\phantom{\rule{.4em}{0ex}}\left(\exists {z}\phantom{\rule{.4em}{0ex}}{z}=\bigcap \left\{{y}\in \mathrm{On}|{x}\in {R}_{1}\left(\mathrm{suc}{y}\right)\right\}↔{x}\in \bigcup {R}_{1}\left[\mathrm{On}\right]\right)$
8 rankwflemb ${⊢}{x}\in \bigcup {R}_{1}\left[\mathrm{On}\right]↔\exists {y}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}{x}\in {R}_{1}\left(\mathrm{suc}{y}\right)$
9 intexrab ${⊢}\exists {y}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}{x}\in {R}_{1}\left(\mathrm{suc}{y}\right)↔\bigcap \left\{{y}\in \mathrm{On}|{x}\in {R}_{1}\left(\mathrm{suc}{y}\right)\right\}\in \mathrm{V}$
10 isset ${⊢}\bigcap \left\{{y}\in \mathrm{On}|{x}\in {R}_{1}\left(\mathrm{suc}{y}\right)\right\}\in \mathrm{V}↔\exists {z}\phantom{\rule{.4em}{0ex}}{z}=\bigcap \left\{{y}\in \mathrm{On}|{x}\in {R}_{1}\left(\mathrm{suc}{y}\right)\right\}$
11 8 9 10 3bitrri ${⊢}\exists {z}\phantom{\rule{.4em}{0ex}}{z}=\bigcap \left\{{y}\in \mathrm{On}|{x}\in {R}_{1}\left(\mathrm{suc}{y}\right)\right\}↔{x}\in \bigcup {R}_{1}\left[\mathrm{On}\right]$
12 7 11 mpgbir ${⊢}\left\{{x}|\exists {z}\phantom{\rule{.4em}{0ex}}{z}=\bigcap \left\{{y}\in \mathrm{On}|{x}\in {R}_{1}\left(\mathrm{suc}{y}\right)\right\}\right\}=\bigcup {R}_{1}\left[\mathrm{On}\right]$
13 6 12 eqtri ${⊢}\mathrm{dom}\left\{⟨{x},{z}⟩|{z}=\bigcap \left\{{y}\in \mathrm{On}|{x}\in {R}_{1}\left(\mathrm{suc}{y}\right)\right\}\right\}=\bigcup {R}_{1}\left[\mathrm{On}\right]$
14 5 13 eqtri ${⊢}\mathrm{dom}\mathrm{rank}=\bigcup {R}_{1}\left[\mathrm{On}\right]$
15 df-fn ${⊢}\mathrm{rank}Fn\bigcup {R}_{1}\left[\mathrm{On}\right]↔\left(\mathrm{Fun}\mathrm{rank}\wedge \mathrm{dom}\mathrm{rank}=\bigcup {R}_{1}\left[\mathrm{On}\right]\right)$
16 2 14 15 mpbir2an ${⊢}\mathrm{rank}Fn\bigcup {R}_{1}\left[\mathrm{On}\right]$
17 rabn0 ${⊢}\left\{{y}\in \mathrm{On}|{x}\in {R}_{1}\left(\mathrm{suc}{y}\right)\right\}\ne \varnothing ↔\exists {y}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}{x}\in {R}_{1}\left(\mathrm{suc}{y}\right)$
18 8 17 bitr4i ${⊢}{x}\in \bigcup {R}_{1}\left[\mathrm{On}\right]↔\left\{{y}\in \mathrm{On}|{x}\in {R}_{1}\left(\mathrm{suc}{y}\right)\right\}\ne \varnothing$
19 intex ${⊢}\left\{{y}\in \mathrm{On}|{x}\in {R}_{1}\left(\mathrm{suc}{y}\right)\right\}\ne \varnothing ↔\bigcap \left\{{y}\in \mathrm{On}|{x}\in {R}_{1}\left(\mathrm{suc}{y}\right)\right\}\in \mathrm{V}$
20 vex ${⊢}{x}\in \mathrm{V}$
21 1 fvmpt2 ${⊢}\left({x}\in \mathrm{V}\wedge \bigcap \left\{{y}\in \mathrm{On}|{x}\in {R}_{1}\left(\mathrm{suc}{y}\right)\right\}\in \mathrm{V}\right)\to \mathrm{rank}\left({x}\right)=\bigcap \left\{{y}\in \mathrm{On}|{x}\in {R}_{1}\left(\mathrm{suc}{y}\right)\right\}$
22 20 21 mpan ${⊢}\bigcap \left\{{y}\in \mathrm{On}|{x}\in {R}_{1}\left(\mathrm{suc}{y}\right)\right\}\in \mathrm{V}\to \mathrm{rank}\left({x}\right)=\bigcap \left\{{y}\in \mathrm{On}|{x}\in {R}_{1}\left(\mathrm{suc}{y}\right)\right\}$
23 19 22 sylbi ${⊢}\left\{{y}\in \mathrm{On}|{x}\in {R}_{1}\left(\mathrm{suc}{y}\right)\right\}\ne \varnothing \to \mathrm{rank}\left({x}\right)=\bigcap \left\{{y}\in \mathrm{On}|{x}\in {R}_{1}\left(\mathrm{suc}{y}\right)\right\}$
24 ssrab2 ${⊢}\left\{{y}\in \mathrm{On}|{x}\in {R}_{1}\left(\mathrm{suc}{y}\right)\right\}\subseteq \mathrm{On}$
25 oninton ${⊢}\left(\left\{{y}\in \mathrm{On}|{x}\in {R}_{1}\left(\mathrm{suc}{y}\right)\right\}\subseteq \mathrm{On}\wedge \left\{{y}\in \mathrm{On}|{x}\in {R}_{1}\left(\mathrm{suc}{y}\right)\right\}\ne \varnothing \right)\to \bigcap \left\{{y}\in \mathrm{On}|{x}\in {R}_{1}\left(\mathrm{suc}{y}\right)\right\}\in \mathrm{On}$
26 24 25 mpan ${⊢}\left\{{y}\in \mathrm{On}|{x}\in {R}_{1}\left(\mathrm{suc}{y}\right)\right\}\ne \varnothing \to \bigcap \left\{{y}\in \mathrm{On}|{x}\in {R}_{1}\left(\mathrm{suc}{y}\right)\right\}\in \mathrm{On}$
27 23 26 eqeltrd ${⊢}\left\{{y}\in \mathrm{On}|{x}\in {R}_{1}\left(\mathrm{suc}{y}\right)\right\}\ne \varnothing \to \mathrm{rank}\left({x}\right)\in \mathrm{On}$
28 18 27 sylbi ${⊢}{x}\in \bigcup {R}_{1}\left[\mathrm{On}\right]\to \mathrm{rank}\left({x}\right)\in \mathrm{On}$
29 28 rgen ${⊢}\forall {x}\in \bigcup {R}_{1}\left[\mathrm{On}\right]\phantom{\rule{.4em}{0ex}}\mathrm{rank}\left({x}\right)\in \mathrm{On}$
30 ffnfv ${⊢}\mathrm{rank}:\bigcup {R}_{1}\left[\mathrm{On}\right]⟶\mathrm{On}↔\left(\mathrm{rank}Fn\bigcup {R}_{1}\left[\mathrm{On}\right]\wedge \forall {x}\in \bigcup {R}_{1}\left[\mathrm{On}\right]\phantom{\rule{.4em}{0ex}}\mathrm{rank}\left({x}\right)\in \mathrm{On}\right)$
31 16 29 30 mpbir2an ${⊢}\mathrm{rank}:\bigcup {R}_{1}\left[\mathrm{On}\right]⟶\mathrm{On}$