This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 10 fndmi ⊢ dom 𝐹 = On
12 9 11 sseqtri ⊢ ( ◡ 𝐹 “ { 𝑤 } ) ⊆ On
13 1 2 3 dnnumch2 ⊢ ( 𝜑 → 𝐴 ⊆ ran 𝐹 )
14 13 sselda ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → 𝑤 ∈ ran 𝐹 )
15 inisegn0 ⊢ ( 𝑤 ∈ ran 𝐹 ↔ ( ◡ 𝐹 “ { 𝑤 } ) ≠ ∅ )
16 14 15 sylib ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → ( ◡ 𝐹 “ { 𝑤 } ) ≠ ∅ )
17 oninton ⊢ ( ( ( ◡ 𝐹 “ { 𝑤 } ) ⊆ On ∧ ( ◡ 𝐹 “ { 𝑤 } ) ≠ ∅ ) → ∩ ( ◡ 𝐹 “ { 𝑤 } ) ∈ On )
18 12 16 17 sylancr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → ∩ ( ◡ 𝐹 “ { 𝑤 } ) ∈ On )
19 4 7 8 18 fvmptd3 ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → ( ( 𝑥 ∈ 𝐴 ↦ ∩ ( ◡ 𝐹 “ { 𝑥 } ) ) ‘ 𝑤 ) = ∩ ( ◡ 𝐹 “ { 𝑤 } ) )