# Metamath Proof Explorer

## Theorem dnnumch1

Description: Define an enumeration of a set from a choice function; second part, it restricts to a bijection.EDITORIAL: overlaps dfac8a . (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 dnnumch1 ${⊢}{\phi }\to \exists {x}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}\left({{F}↾}_{{x}}\right):{x}\underset{1-1 onto}{⟶}{A}$

### 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 recsval ${⊢}{x}\in \mathrm{On}\to \mathrm{recs}\left(\left({z}\in \mathrm{V}⟼{G}\left({A}\setminus \mathrm{ran}{z}\right)\right)\right)\left({x}\right)=\left({z}\in \mathrm{V}⟼{G}\left({A}\setminus \mathrm{ran}{z}\right)\right)\left({\mathrm{recs}\left(\left({z}\in \mathrm{V}⟼{G}\left({A}\setminus \mathrm{ran}{z}\right)\right)\right)↾}_{{x}}\right)$
5 1 fveq1i ${⊢}{F}\left({x}\right)=\mathrm{recs}\left(\left({z}\in \mathrm{V}⟼{G}\left({A}\setminus \mathrm{ran}{z}\right)\right)\right)\left({x}\right)$
6 1 tfr1 ${⊢}{F}Fn\mathrm{On}$
7 fnfun ${⊢}{F}Fn\mathrm{On}\to \mathrm{Fun}{F}$
8 6 7 ax-mp ${⊢}\mathrm{Fun}{F}$
9 vex ${⊢}{x}\in \mathrm{V}$
10 resfunexg ${⊢}\left(\mathrm{Fun}{F}\wedge {x}\in \mathrm{V}\right)\to {{F}↾}_{{x}}\in \mathrm{V}$
11 8 9 10 mp2an ${⊢}{{F}↾}_{{x}}\in \mathrm{V}$
12 rneq ${⊢}{w}={{F}↾}_{{x}}\to \mathrm{ran}{w}=\mathrm{ran}\left({{F}↾}_{{x}}\right)$
13 df-ima ${⊢}{F}\left[{x}\right]=\mathrm{ran}\left({{F}↾}_{{x}}\right)$
14 12 13 syl6eqr ${⊢}{w}={{F}↾}_{{x}}\to \mathrm{ran}{w}={F}\left[{x}\right]$
15 14 difeq2d ${⊢}{w}={{F}↾}_{{x}}\to {A}\setminus \mathrm{ran}{w}={A}\setminus {F}\left[{x}\right]$
16 15 fveq2d ${⊢}{w}={{F}↾}_{{x}}\to {G}\left({A}\setminus \mathrm{ran}{w}\right)={G}\left({A}\setminus {F}\left[{x}\right]\right)$
17 rneq ${⊢}{z}={w}\to \mathrm{ran}{z}=\mathrm{ran}{w}$
18 17 difeq2d ${⊢}{z}={w}\to {A}\setminus \mathrm{ran}{z}={A}\setminus \mathrm{ran}{w}$
19 18 fveq2d ${⊢}{z}={w}\to {G}\left({A}\setminus \mathrm{ran}{z}\right)={G}\left({A}\setminus \mathrm{ran}{w}\right)$
20 19 cbvmptv ${⊢}\left({z}\in \mathrm{V}⟼{G}\left({A}\setminus \mathrm{ran}{z}\right)\right)=\left({w}\in \mathrm{V}⟼{G}\left({A}\setminus \mathrm{ran}{w}\right)\right)$
21 fvex ${⊢}{G}\left({A}\setminus {F}\left[{x}\right]\right)\in \mathrm{V}$
22 16 20 21 fvmpt ${⊢}{{F}↾}_{{x}}\in \mathrm{V}\to \left({z}\in \mathrm{V}⟼{G}\left({A}\setminus \mathrm{ran}{z}\right)\right)\left({{F}↾}_{{x}}\right)={G}\left({A}\setminus {F}\left[{x}\right]\right)$
23 11 22 ax-mp ${⊢}\left({z}\in \mathrm{V}⟼{G}\left({A}\setminus \mathrm{ran}{z}\right)\right)\left({{F}↾}_{{x}}\right)={G}\left({A}\setminus {F}\left[{x}\right]\right)$
24 1 reseq1i ${⊢}{{F}↾}_{{x}}={\mathrm{recs}\left(\left({z}\in \mathrm{V}⟼{G}\left({A}\setminus \mathrm{ran}{z}\right)\right)\right)↾}_{{x}}$
25 24 fveq2i ${⊢}\left({z}\in \mathrm{V}⟼{G}\left({A}\setminus \mathrm{ran}{z}\right)\right)\left({{F}↾}_{{x}}\right)=\left({z}\in \mathrm{V}⟼{G}\left({A}\setminus \mathrm{ran}{z}\right)\right)\left({\mathrm{recs}\left(\left({z}\in \mathrm{V}⟼{G}\left({A}\setminus \mathrm{ran}{z}\right)\right)\right)↾}_{{x}}\right)$
26 23 25 eqtr3i ${⊢}{G}\left({A}\setminus {F}\left[{x}\right]\right)=\left({z}\in \mathrm{V}⟼{G}\left({A}\setminus \mathrm{ran}{z}\right)\right)\left({\mathrm{recs}\left(\left({z}\in \mathrm{V}⟼{G}\left({A}\setminus \mathrm{ran}{z}\right)\right)\right)↾}_{{x}}\right)$
27 4 5 26 3eqtr4g ${⊢}{x}\in \mathrm{On}\to {F}\left({x}\right)={G}\left({A}\setminus {F}\left[{x}\right]\right)$
28 27 ad2antlr ${⊢}\left(\left({\phi }\wedge {x}\in \mathrm{On}\right)\wedge {A}\setminus {F}\left[{x}\right]\ne \varnothing \right)\to {F}\left({x}\right)={G}\left({A}\setminus {F}\left[{x}\right]\right)$
29 difss ${⊢}{A}\setminus {F}\left[{x}\right]\subseteq {A}$
30 elpw2g ${⊢}{A}\in {V}\to \left({A}\setminus {F}\left[{x}\right]\in 𝒫{A}↔{A}\setminus {F}\left[{x}\right]\subseteq {A}\right)$
31 2 30 syl ${⊢}{\phi }\to \left({A}\setminus {F}\left[{x}\right]\in 𝒫{A}↔{A}\setminus {F}\left[{x}\right]\subseteq {A}\right)$
32 29 31 mpbiri ${⊢}{\phi }\to {A}\setminus {F}\left[{x}\right]\in 𝒫{A}$
33 neeq1 ${⊢}{y}={A}\setminus {F}\left[{x}\right]\to \left({y}\ne \varnothing ↔{A}\setminus {F}\left[{x}\right]\ne \varnothing \right)$
34 fveq2 ${⊢}{y}={A}\setminus {F}\left[{x}\right]\to {G}\left({y}\right)={G}\left({A}\setminus {F}\left[{x}\right]\right)$
35 id ${⊢}{y}={A}\setminus {F}\left[{x}\right]\to {y}={A}\setminus {F}\left[{x}\right]$
36 34 35 eleq12d ${⊢}{y}={A}\setminus {F}\left[{x}\right]\to \left({G}\left({y}\right)\in {y}↔{G}\left({A}\setminus {F}\left[{x}\right]\right)\in \left({A}\setminus {F}\left[{x}\right]\right)\right)$
37 33 36 imbi12d ${⊢}{y}={A}\setminus {F}\left[{x}\right]\to \left(\left({y}\ne \varnothing \to {G}\left({y}\right)\in {y}\right)↔\left({A}\setminus {F}\left[{x}\right]\ne \varnothing \to {G}\left({A}\setminus {F}\left[{x}\right]\right)\in \left({A}\setminus {F}\left[{x}\right]\right)\right)\right)$
38 37 rspcva ${⊢}\left({A}\setminus {F}\left[{x}\right]\in 𝒫{A}\wedge \forall {y}\in 𝒫{A}\phantom{\rule{.4em}{0ex}}\left({y}\ne \varnothing \to {G}\left({y}\right)\in {y}\right)\right)\to \left({A}\setminus {F}\left[{x}\right]\ne \varnothing \to {G}\left({A}\setminus {F}\left[{x}\right]\right)\in \left({A}\setminus {F}\left[{x}\right]\right)\right)$
39 32 3 38 syl2anc ${⊢}{\phi }\to \left({A}\setminus {F}\left[{x}\right]\ne \varnothing \to {G}\left({A}\setminus {F}\left[{x}\right]\right)\in \left({A}\setminus {F}\left[{x}\right]\right)\right)$
40 39 adantr ${⊢}\left({\phi }\wedge {x}\in \mathrm{On}\right)\to \left({A}\setminus {F}\left[{x}\right]\ne \varnothing \to {G}\left({A}\setminus {F}\left[{x}\right]\right)\in \left({A}\setminus {F}\left[{x}\right]\right)\right)$
41 40 imp ${⊢}\left(\left({\phi }\wedge {x}\in \mathrm{On}\right)\wedge {A}\setminus {F}\left[{x}\right]\ne \varnothing \right)\to {G}\left({A}\setminus {F}\left[{x}\right]\right)\in \left({A}\setminus {F}\left[{x}\right]\right)$
42 28 41 eqeltrd ${⊢}\left(\left({\phi }\wedge {x}\in \mathrm{On}\right)\wedge {A}\setminus {F}\left[{x}\right]\ne \varnothing \right)\to {F}\left({x}\right)\in \left({A}\setminus {F}\left[{x}\right]\right)$
43 42 ex ${⊢}\left({\phi }\wedge {x}\in \mathrm{On}\right)\to \left({A}\setminus {F}\left[{x}\right]\ne \varnothing \to {F}\left({x}\right)\in \left({A}\setminus {F}\left[{x}\right]\right)\right)$
44 43 ralrimiva ${⊢}{\phi }\to \forall {x}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}\left({A}\setminus {F}\left[{x}\right]\ne \varnothing \to {F}\left({x}\right)\in \left({A}\setminus {F}\left[{x}\right]\right)\right)$
45 6 tz7.49c ${⊢}\left({A}\in {V}\wedge \forall {x}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}\left({A}\setminus {F}\left[{x}\right]\ne \varnothing \to {F}\left({x}\right)\in \left({A}\setminus {F}\left[{x}\right]\right)\right)\right)\to \exists {x}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}\left({{F}↾}_{{x}}\right):{x}\underset{1-1 onto}{⟶}{A}$
46 2 44 45 syl2anc ${⊢}{\phi }\to \exists {x}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}\left({{F}↾}_{{x}}\right):{x}\underset{1-1 onto}{⟶}{A}$