# Metamath Proof Explorer

## Theorem dnnumch3

Description: Define an injection from a set into the ordinals using a choice 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 dnnumch3 ${⊢}{\phi }\to \left({x}\in {A}⟼\bigcap {{F}}^{-1}\left[\left\{{x}\right\}\right]\right):{A}\underset{1-1}{⟶}\mathrm{On}$

### 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 cnvimass ${⊢}{{F}}^{-1}\left[\left\{{x}\right\}\right]\subseteq \mathrm{dom}{F}$
5 1 tfr1 ${⊢}{F}Fn\mathrm{On}$
6 fndm ${⊢}{F}Fn\mathrm{On}\to \mathrm{dom}{F}=\mathrm{On}$
7 5 6 ax-mp ${⊢}\mathrm{dom}{F}=\mathrm{On}$
8 4 7 sseqtri ${⊢}{{F}}^{-1}\left[\left\{{x}\right\}\right]\subseteq \mathrm{On}$
9 1 2 3 dnnumch2 ${⊢}{\phi }\to {A}\subseteq \mathrm{ran}{F}$
10 9 sselda ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {x}\in \mathrm{ran}{F}$
11 inisegn0 ${⊢}{x}\in \mathrm{ran}{F}↔{{F}}^{-1}\left[\left\{{x}\right\}\right]\ne \varnothing$
12 10 11 sylib ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {{F}}^{-1}\left[\left\{{x}\right\}\right]\ne \varnothing$
13 oninton ${⊢}\left({{F}}^{-1}\left[\left\{{x}\right\}\right]\subseteq \mathrm{On}\wedge {{F}}^{-1}\left[\left\{{x}\right\}\right]\ne \varnothing \right)\to \bigcap {{F}}^{-1}\left[\left\{{x}\right\}\right]\in \mathrm{On}$
14 8 12 13 sylancr ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to \bigcap {{F}}^{-1}\left[\left\{{x}\right\}\right]\in \mathrm{On}$
15 14 fmpttd ${⊢}{\phi }\to \left({x}\in {A}⟼\bigcap {{F}}^{-1}\left[\left\{{x}\right\}\right]\right):{A}⟶\mathrm{On}$
16 1 2 3 dnnumch3lem ${⊢}\left({\phi }\wedge {v}\in {A}\right)\to \left({x}\in {A}⟼\bigcap {{F}}^{-1}\left[\left\{{x}\right\}\right]\right)\left({v}\right)=\bigcap {{F}}^{-1}\left[\left\{{v}\right\}\right]$
17 16 adantrr ${⊢}\left({\phi }\wedge \left({v}\in {A}\wedge {w}\in {A}\right)\right)\to \left({x}\in {A}⟼\bigcap {{F}}^{-1}\left[\left\{{x}\right\}\right]\right)\left({v}\right)=\bigcap {{F}}^{-1}\left[\left\{{v}\right\}\right]$
18 1 2 3 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]$
19 18 adantrl ${⊢}\left({\phi }\wedge \left({v}\in {A}\wedge {w}\in {A}\right)\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]$
20 17 19 eqeq12d ${⊢}\left({\phi }\wedge \left({v}\in {A}\wedge {w}\in {A}\right)\right)\to \left(\left({x}\in {A}⟼\bigcap {{F}}^{-1}\left[\left\{{x}\right\}\right]\right)\left({v}\right)=\left({x}\in {A}⟼\bigcap {{F}}^{-1}\left[\left\{{x}\right\}\right]\right)\left({w}\right)↔\bigcap {{F}}^{-1}\left[\left\{{v}\right\}\right]=\bigcap {{F}}^{-1}\left[\left\{{w}\right\}\right]\right)$
21 fveq2 ${⊢}\bigcap {{F}}^{-1}\left[\left\{{v}\right\}\right]=\bigcap {{F}}^{-1}\left[\left\{{w}\right\}\right]\to {F}\left(\bigcap {{F}}^{-1}\left[\left\{{v}\right\}\right]\right)={F}\left(\bigcap {{F}}^{-1}\left[\left\{{w}\right\}\right]\right)$
22 21 adantl ${⊢}\left(\left({\phi }\wedge \left({v}\in {A}\wedge {w}\in {A}\right)\right)\wedge \bigcap {{F}}^{-1}\left[\left\{{v}\right\}\right]=\bigcap {{F}}^{-1}\left[\left\{{w}\right\}\right]\right)\to {F}\left(\bigcap {{F}}^{-1}\left[\left\{{v}\right\}\right]\right)={F}\left(\bigcap {{F}}^{-1}\left[\left\{{w}\right\}\right]\right)$
23 cnvimass ${⊢}{{F}}^{-1}\left[\left\{{v}\right\}\right]\subseteq \mathrm{dom}{F}$
24 23 7 sseqtri ${⊢}{{F}}^{-1}\left[\left\{{v}\right\}\right]\subseteq \mathrm{On}$
25 9 sselda ${⊢}\left({\phi }\wedge {v}\in {A}\right)\to {v}\in \mathrm{ran}{F}$
26 inisegn0 ${⊢}{v}\in \mathrm{ran}{F}↔{{F}}^{-1}\left[\left\{{v}\right\}\right]\ne \varnothing$
27 25 26 sylib ${⊢}\left({\phi }\wedge {v}\in {A}\right)\to {{F}}^{-1}\left[\left\{{v}\right\}\right]\ne \varnothing$
28 onint ${⊢}\left({{F}}^{-1}\left[\left\{{v}\right\}\right]\subseteq \mathrm{On}\wedge {{F}}^{-1}\left[\left\{{v}\right\}\right]\ne \varnothing \right)\to \bigcap {{F}}^{-1}\left[\left\{{v}\right\}\right]\in {{F}}^{-1}\left[\left\{{v}\right\}\right]$
29 24 27 28 sylancr ${⊢}\left({\phi }\wedge {v}\in {A}\right)\to \bigcap {{F}}^{-1}\left[\left\{{v}\right\}\right]\in {{F}}^{-1}\left[\left\{{v}\right\}\right]$
30 fniniseg ${⊢}{F}Fn\mathrm{On}\to \left(\bigcap {{F}}^{-1}\left[\left\{{v}\right\}\right]\in {{F}}^{-1}\left[\left\{{v}\right\}\right]↔\left(\bigcap {{F}}^{-1}\left[\left\{{v}\right\}\right]\in \mathrm{On}\wedge {F}\left(\bigcap {{F}}^{-1}\left[\left\{{v}\right\}\right]\right)={v}\right)\right)$
31 5 30 ax-mp ${⊢}\bigcap {{F}}^{-1}\left[\left\{{v}\right\}\right]\in {{F}}^{-1}\left[\left\{{v}\right\}\right]↔\left(\bigcap {{F}}^{-1}\left[\left\{{v}\right\}\right]\in \mathrm{On}\wedge {F}\left(\bigcap {{F}}^{-1}\left[\left\{{v}\right\}\right]\right)={v}\right)$
32 31 simprbi ${⊢}\bigcap {{F}}^{-1}\left[\left\{{v}\right\}\right]\in {{F}}^{-1}\left[\left\{{v}\right\}\right]\to {F}\left(\bigcap {{F}}^{-1}\left[\left\{{v}\right\}\right]\right)={v}$
33 29 32 syl ${⊢}\left({\phi }\wedge {v}\in {A}\right)\to {F}\left(\bigcap {{F}}^{-1}\left[\left\{{v}\right\}\right]\right)={v}$
34 33 adantrr ${⊢}\left({\phi }\wedge \left({v}\in {A}\wedge {w}\in {A}\right)\right)\to {F}\left(\bigcap {{F}}^{-1}\left[\left\{{v}\right\}\right]\right)={v}$
35 34 adantr ${⊢}\left(\left({\phi }\wedge \left({v}\in {A}\wedge {w}\in {A}\right)\right)\wedge \bigcap {{F}}^{-1}\left[\left\{{v}\right\}\right]=\bigcap {{F}}^{-1}\left[\left\{{w}\right\}\right]\right)\to {F}\left(\bigcap {{F}}^{-1}\left[\left\{{v}\right\}\right]\right)={v}$
36 cnvimass ${⊢}{{F}}^{-1}\left[\left\{{w}\right\}\right]\subseteq \mathrm{dom}{F}$
37 36 7 sseqtri ${⊢}{{F}}^{-1}\left[\left\{{w}\right\}\right]\subseteq \mathrm{On}$
38 9 sselda ${⊢}\left({\phi }\wedge {w}\in {A}\right)\to {w}\in \mathrm{ran}{F}$
39 inisegn0 ${⊢}{w}\in \mathrm{ran}{F}↔{{F}}^{-1}\left[\left\{{w}\right\}\right]\ne \varnothing$
40 38 39 sylib ${⊢}\left({\phi }\wedge {w}\in {A}\right)\to {{F}}^{-1}\left[\left\{{w}\right\}\right]\ne \varnothing$
41 onint ${⊢}\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 {{F}}^{-1}\left[\left\{{w}\right\}\right]$
42 37 40 41 sylancr ${⊢}\left({\phi }\wedge {w}\in {A}\right)\to \bigcap {{F}}^{-1}\left[\left\{{w}\right\}\right]\in {{F}}^{-1}\left[\left\{{w}\right\}\right]$
43 fniniseg ${⊢}{F}Fn\mathrm{On}\to \left(\bigcap {{F}}^{-1}\left[\left\{{w}\right\}\right]\in {{F}}^{-1}\left[\left\{{w}\right\}\right]↔\left(\bigcap {{F}}^{-1}\left[\left\{{w}\right\}\right]\in \mathrm{On}\wedge {F}\left(\bigcap {{F}}^{-1}\left[\left\{{w}\right\}\right]\right)={w}\right)\right)$
44 5 43 ax-mp ${⊢}\bigcap {{F}}^{-1}\left[\left\{{w}\right\}\right]\in {{F}}^{-1}\left[\left\{{w}\right\}\right]↔\left(\bigcap {{F}}^{-1}\left[\left\{{w}\right\}\right]\in \mathrm{On}\wedge {F}\left(\bigcap {{F}}^{-1}\left[\left\{{w}\right\}\right]\right)={w}\right)$
45 44 simprbi ${⊢}\bigcap {{F}}^{-1}\left[\left\{{w}\right\}\right]\in {{F}}^{-1}\left[\left\{{w}\right\}\right]\to {F}\left(\bigcap {{F}}^{-1}\left[\left\{{w}\right\}\right]\right)={w}$
46 42 45 syl ${⊢}\left({\phi }\wedge {w}\in {A}\right)\to {F}\left(\bigcap {{F}}^{-1}\left[\left\{{w}\right\}\right]\right)={w}$
47 46 adantrl ${⊢}\left({\phi }\wedge \left({v}\in {A}\wedge {w}\in {A}\right)\right)\to {F}\left(\bigcap {{F}}^{-1}\left[\left\{{w}\right\}\right]\right)={w}$
48 47 adantr ${⊢}\left(\left({\phi }\wedge \left({v}\in {A}\wedge {w}\in {A}\right)\right)\wedge \bigcap {{F}}^{-1}\left[\left\{{v}\right\}\right]=\bigcap {{F}}^{-1}\left[\left\{{w}\right\}\right]\right)\to {F}\left(\bigcap {{F}}^{-1}\left[\left\{{w}\right\}\right]\right)={w}$
49 22 35 48 3eqtr3d ${⊢}\left(\left({\phi }\wedge \left({v}\in {A}\wedge {w}\in {A}\right)\right)\wedge \bigcap {{F}}^{-1}\left[\left\{{v}\right\}\right]=\bigcap {{F}}^{-1}\left[\left\{{w}\right\}\right]\right)\to {v}={w}$
50 49 ex ${⊢}\left({\phi }\wedge \left({v}\in {A}\wedge {w}\in {A}\right)\right)\to \left(\bigcap {{F}}^{-1}\left[\left\{{v}\right\}\right]=\bigcap {{F}}^{-1}\left[\left\{{w}\right\}\right]\to {v}={w}\right)$
51 20 50 sylbid ${⊢}\left({\phi }\wedge \left({v}\in {A}\wedge {w}\in {A}\right)\right)\to \left(\left({x}\in {A}⟼\bigcap {{F}}^{-1}\left[\left\{{x}\right\}\right]\right)\left({v}\right)=\left({x}\in {A}⟼\bigcap {{F}}^{-1}\left[\left\{{x}\right\}\right]\right)\left({w}\right)\to {v}={w}\right)$
52 51 ralrimivva ${⊢}{\phi }\to \forall {v}\in {A}\phantom{\rule{.4em}{0ex}}\forall {w}\in {A}\phantom{\rule{.4em}{0ex}}\left(\left({x}\in {A}⟼\bigcap {{F}}^{-1}\left[\left\{{x}\right\}\right]\right)\left({v}\right)=\left({x}\in {A}⟼\bigcap {{F}}^{-1}\left[\left\{{x}\right\}\right]\right)\left({w}\right)\to {v}={w}\right)$
53 dff13 ${⊢}\left({x}\in {A}⟼\bigcap {{F}}^{-1}\left[\left\{{x}\right\}\right]\right):{A}\underset{1-1}{⟶}\mathrm{On}↔\left(\left({x}\in {A}⟼\bigcap {{F}}^{-1}\left[\left\{{x}\right\}\right]\right):{A}⟶\mathrm{On}\wedge \forall {v}\in {A}\phantom{\rule{.4em}{0ex}}\forall {w}\in {A}\phantom{\rule{.4em}{0ex}}\left(\left({x}\in {A}⟼\bigcap {{F}}^{-1}\left[\left\{{x}\right\}\right]\right)\left({v}\right)=\left({x}\in {A}⟼\bigcap {{F}}^{-1}\left[\left\{{x}\right\}\right]\right)\left({w}\right)\to {v}={w}\right)\right)$
54 15 52 53 sylanbrc ${⊢}{\phi }\to \left({x}\in {A}⟼\bigcap {{F}}^{-1}\left[\left\{{x}\right\}\right]\right):{A}\underset{1-1}{⟶}\mathrm{On}$