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

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 eqid x A F -1 x = x A F -1 x
5 sneq x = w x = w
6 5 imaeq2d x = w F -1 x = F -1 w
7 6 inteqd x = w F -1 x = F -1 w
8 simpr φ w A w A
9 cnvimass F -1 w dom F
10 1 tfr1 F Fn On
11 fndm F Fn On dom F = On
12 10 11 ax-mp dom F = On
13 9 12 sseqtri F -1 w On
14 1 2 3 dnnumch2 φ A ran F
15 14 sselda φ w A w ran F
16 inisegn0 w ran F F -1 w
17 15 16 sylib φ w A F -1 w
18 oninton F -1 w On F -1 w F -1 w On
19 13 17 18 sylancr φ w A F -1 w On
20 4 7 8 19 fvmptd3 φ w A x A F -1 x w = F -1 w