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 𝐹 = recs ( ( 𝑧 ∈ V ↦ ( 𝐺 ‘ ( 𝐴 ∖ ran 𝑧 ) ) ) )
dnnumch.a ( 𝜑𝐴𝑉 )
dnnumch.g ( 𝜑 → ∀ 𝑦 ∈ 𝒫 𝐴 ( 𝑦 ≠ ∅ → ( 𝐺𝑦 ) ∈ 𝑦 ) )
Assertion dnnumch3lem ( ( 𝜑𝑤𝐴 ) → ( ( 𝑥𝐴 ( 𝐹 “ { 𝑥 } ) ) ‘ 𝑤 ) = ( 𝐹 “ { 𝑤 } ) )

Proof

Step Hyp Ref Expression
1 dnnumch.f 𝐹 = recs ( ( 𝑧 ∈ V ↦ ( 𝐺 ‘ ( 𝐴 ∖ ran 𝑧 ) ) ) )
2 dnnumch.a ( 𝜑𝐴𝑉 )
3 dnnumch.g ( 𝜑 → ∀ 𝑦 ∈ 𝒫 𝐴 ( 𝑦 ≠ ∅ → ( 𝐺𝑦 ) ∈ 𝑦 ) )
4 eqid ( 𝑥𝐴 ( 𝐹 “ { 𝑥 } ) ) = ( 𝑥𝐴 ( 𝐹 “ { 𝑥 } ) )
5 sneq ( 𝑥 = 𝑤 → { 𝑥 } = { 𝑤 } )
6 5 imaeq2d ( 𝑥 = 𝑤 → ( 𝐹 “ { 𝑥 } ) = ( 𝐹 “ { 𝑤 } ) )
7 6 inteqd ( 𝑥 = 𝑤 ( 𝐹 “ { 𝑥 } ) = ( 𝐹 “ { 𝑤 } ) )
8 simpr ( ( 𝜑𝑤𝐴 ) → 𝑤𝐴 )
9 cnvimass ( 𝐹 “ { 𝑤 } ) ⊆ dom 𝐹
10 1 tfr1 𝐹 Fn On
11 fndm ( 𝐹 Fn On → dom 𝐹 = On )
12 10 11 ax-mp dom 𝐹 = On
13 9 12 sseqtri ( 𝐹 “ { 𝑤 } ) ⊆ On
14 1 2 3 dnnumch2 ( 𝜑𝐴 ⊆ ran 𝐹 )
15 14 sselda ( ( 𝜑𝑤𝐴 ) → 𝑤 ∈ ran 𝐹 )
16 inisegn0 ( 𝑤 ∈ ran 𝐹 ↔ ( 𝐹 “ { 𝑤 } ) ≠ ∅ )
17 15 16 sylib ( ( 𝜑𝑤𝐴 ) → ( 𝐹 “ { 𝑤 } ) ≠ ∅ )
18 oninton ( ( ( 𝐹 “ { 𝑤 } ) ⊆ On ∧ ( 𝐹 “ { 𝑤 } ) ≠ ∅ ) → ( 𝐹 “ { 𝑤 } ) ∈ On )
19 13 17 18 sylancr ( ( 𝜑𝑤𝐴 ) → ( 𝐹 “ { 𝑤 } ) ∈ On )
20 4 7 8 19 fvmptd3 ( ( 𝜑𝑤𝐴 ) → ( ( 𝑥𝐴 ( 𝐹 “ { 𝑥 } ) ) ‘ 𝑤 ) = ( 𝐹 “ { 𝑤 } ) )