# Metamath Proof Explorer

## Theorem dnnumch3lem

Description: Value of the ordinal injection function. (Contributed by Stefan O'Rear, 18-Jan-2015)

Ref Expression
Hypotheses dnnumch.f ${⊢}{F}=\mathrm{recs}\left(\left({z}\in \mathrm{V}⟼{G}\left({A}\setminus \mathrm{ran}{z}\right)\right)\right)$
dnnumch.a ${⊢}{\phi }\to {A}\in {V}$
dnnumch.g ${⊢}{\phi }\to \forall {y}\in 𝒫{A}\phantom{\rule{.4em}{0ex}}\left({y}\ne \varnothing \to {G}\left({y}\right)\in {y}\right)$
Assertion dnnumch3lem ${⊢}\left({\phi }\wedge {w}\in {A}\right)\to \left({x}\in {A}⟼\bigcap {{F}}^{-1}\left[\left\{{x}\right\}\right]\right)\left({w}\right)=\bigcap {{F}}^{-1}\left[\left\{{w}\right\}\right]$

### Proof

Step Hyp Ref Expression
1 dnnumch.f ${⊢}{F}=\mathrm{recs}\left(\left({z}\in \mathrm{V}⟼{G}\left({A}\setminus \mathrm{ran}{z}\right)\right)\right)$
2 dnnumch.a ${⊢}{\phi }\to {A}\in {V}$
3 dnnumch.g ${⊢}{\phi }\to \forall {y}\in 𝒫{A}\phantom{\rule{.4em}{0ex}}\left({y}\ne \varnothing \to {G}\left({y}\right)\in {y}\right)$
4 eqid ${⊢}\left({x}\in {A}⟼\bigcap {{F}}^{-1}\left[\left\{{x}\right\}\right]\right)=\left({x}\in {A}⟼\bigcap {{F}}^{-1}\left[\left\{{x}\right\}\right]\right)$
5 sneq ${⊢}{x}={w}\to \left\{{x}\right\}=\left\{{w}\right\}$
6 5 imaeq2d ${⊢}{x}={w}\to {{F}}^{-1}\left[\left\{{x}\right\}\right]={{F}}^{-1}\left[\left\{{w}\right\}\right]$
7 6 inteqd ${⊢}{x}={w}\to \bigcap {{F}}^{-1}\left[\left\{{x}\right\}\right]=\bigcap {{F}}^{-1}\left[\left\{{w}\right\}\right]$
8 simpr ${⊢}\left({\phi }\wedge {w}\in {A}\right)\to {w}\in {A}$
9 cnvimass ${⊢}{{F}}^{-1}\left[\left\{{w}\right\}\right]\subseteq \mathrm{dom}{F}$
10 1 tfr1 ${⊢}{F}Fn\mathrm{On}$
11 fndm ${⊢}{F}Fn\mathrm{On}\to \mathrm{dom}{F}=\mathrm{On}$
12 10 11 ax-mp ${⊢}\mathrm{dom}{F}=\mathrm{On}$
13 9 12 sseqtri ${⊢}{{F}}^{-1}\left[\left\{{w}\right\}\right]\subseteq \mathrm{On}$
14 1 2 3 dnnumch2 ${⊢}{\phi }\to {A}\subseteq \mathrm{ran}{F}$
15 14 sselda ${⊢}\left({\phi }\wedge {w}\in {A}\right)\to {w}\in \mathrm{ran}{F}$
16 inisegn0 ${⊢}{w}\in \mathrm{ran}{F}↔{{F}}^{-1}\left[\left\{{w}\right\}\right]\ne \varnothing$
17 15 16 sylib ${⊢}\left({\phi }\wedge {w}\in {A}\right)\to {{F}}^{-1}\left[\left\{{w}\right\}\right]\ne \varnothing$
18 oninton ${⊢}\left({{F}}^{-1}\left[\left\{{w}\right\}\right]\subseteq \mathrm{On}\wedge {{F}}^{-1}\left[\left\{{w}\right\}\right]\ne \varnothing \right)\to \bigcap {{F}}^{-1}\left[\left\{{w}\right\}\right]\in \mathrm{On}$
19 13 17 18 sylancr ${⊢}\left({\phi }\wedge {w}\in {A}\right)\to \bigcap {{F}}^{-1}\left[\left\{{w}\right\}\right]\in \mathrm{On}$
20 4 7 8 19 fvmptd3 ${⊢}\left({\phi }\wedge {w}\in {A}\right)\to \left({x}\in {A}⟼\bigcap {{F}}^{-1}\left[\left\{{x}\right\}\right]\right)\left({w}\right)=\bigcap {{F}}^{-1}\left[\left\{{w}\right\}\right]$