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 10 fndmi ⊢ dom ⁡ F = On
12 9 11 sseqtri ⊢ F -1 w ⊆ On
13 1 2 3 dnnumch2 ⊢ φ → A ⊆ ran ⁡ F
14 13 sselda ⊢ φ ∧ w ∈ A → w ∈ ran ⁡ F
15 inisegn0 ⊢ w ∈ ran ⁡ F ↔ F -1 w ≠ ∅
16 14 15 sylib ⊢ φ ∧ w ∈ A → F -1 w ≠ ∅
17 oninton ⊢ F -1 w ⊆ On ∧ F -1 w ≠ ∅ → ⋂ F -1 w ∈ On
18 12 16 17 sylancr ⊢ φ ∧ w ∈ A → ⋂ F -1 w ∈ On
19 4 7 8 18 fvmptd3 ⊢ φ ∧ w ∈ A → x ∈ A ⟼ ⋂ F -1 x ⁡ w = ⋂ F -1 w