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 = recs z V G A ran z
dnnumch.a φ A V
dnnumch.g φ y 𝒫 A y G y y
Assertion dnnumch1 φ x On F x : x 1-1 onto A

Proof

Step Hyp Ref Expression
1 dnnumch.f F = recs z V G A ran z
2 dnnumch.a φ A V
3 dnnumch.g φ y 𝒫 A y G y y
4 recsval x On recs z V G A ran z x = z V G A ran z recs z V G A ran z x
5 1 fveq1i F x = recs z V G A ran z x
6 1 tfr1 F Fn On
7 fnfun F Fn On Fun F
8 6 7 ax-mp Fun F
9 vex x V
10 resfunexg Fun F x V F x V
11 8 9 10 mp2an F x V
12 rneq w = F x ran w = ran F x
13 df-ima F x = ran F x
14 12 13 eqtr4di w = F x ran w = F x
15 14 difeq2d w = F x A ran w = A F x
16 15 fveq2d w = F x G A ran w = G A F x
17 rneq z = w ran z = ran w
18 17 difeq2d z = w A ran z = A ran w
19 18 fveq2d z = w G A ran z = G A ran w
20 19 cbvmptv z V G A ran z = w V G A ran w
21 fvex G A F x V
22 16 20 21 fvmpt F x V z V G A ran z F x = G A F x
23 11 22 ax-mp z V G A ran z F x = G A F x
24 1 reseq1i F x = recs z V G A ran z x
25 24 fveq2i z V G A ran z F x = z V G A ran z recs z V G A ran z x
26 23 25 eqtr3i G A F x = z V G A ran z recs z V G A ran z x
27 4 5 26 3eqtr4g x On F x = G A F x
28 27 ad2antlr φ x On A F x F x = G A F x
29 difss A F x A
30 elpw2g A V A F x 𝒫 A A F x A
31 2 30 syl φ A F x 𝒫 A A F x A
32 29 31 mpbiri φ A F x 𝒫 A
33 neeq1 y = A F x y A F x
34 fveq2 y = A F x G y = G A F x
35 id y = A F x y = A F x
36 34 35 eleq12d y = A F x G y y G A F x A F x
37 33 36 imbi12d y = A F x y G y y A F x G A F x A F x
38 37 rspcva A F x 𝒫 A y 𝒫 A y G y y A F x G A F x A F x
39 32 3 38 syl2anc φ A F x G A F x A F x
40 39 adantr φ x On A F x G A F x A F x
41 40 imp φ x On A F x G A F x A F x
42 28 41 eqeltrd φ x On A F x F x A F x
43 42 ex φ x On A F x F x A F x
44 43 ralrimiva φ x On A F x F x A F x
45 6 tz7.49c A V x On A F x F x A F x x On F x : x 1-1 onto A
46 2 44 45 syl2anc φ x On F x : x 1-1 onto A