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

Metamath Proof Explorer

Theorem elfvmptrab1

Description: Implications for the value of a function defined by the maps-to notation with a class abstraction as a result having an element. Here, the base set of the class abstraction depends on the argument of the function. Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker elfvmptrab1w when possible. (Contributed by Alexander van der Vekens, 15-Jul-2018) (New usage is discouraged.)

Ref Expression
Hypotheses elfvmptrab1.f ⊢ F = x ∈ V ⟼ y ∈ ⦋ x / m⦌ M | φ
elfvmptrab1.v ⊢ X ∈ V → ⦋ X / m⦌ M ∈ V
Assertion elfvmptrab1 ⊢ Y ∈ F ⁡ X → X ∈ V ∧ Y ∈ ⦋ X / m⦌ M

Proof

Step Hyp Ref Expression
1 elfvmptrab1.f ⊢ F = x ∈ V ⟼ y ∈ ⦋ x / m⦌ M | φ
2 elfvmptrab1.v ⊢ X ∈ V → ⦋ X / m⦌ M ∈ V
3 ne0i ⊢ Y ∈ F ⁡ X → F ⁡ X ≠ ∅
4 ndmfv ⊢ ¬ X ∈ dom ⁡ F → F ⁡ X = ∅
5 4 necon1ai ⊢ F ⁡ X ≠ ∅ → X ∈ dom ⁡ F
6 1 dmmptss ⊢ dom ⁡ F ⊆ V
7 6 sseli ⊢ X ∈ dom ⁡ F → X ∈ V
8 rabexg ⊢ ⦋ X / m⦌ M ∈ V → y ∈ ⦋ X / m⦌ M | [˙X / x]˙ φ ∈ V
9 7 2 8 3syl ⊢ X ∈ dom ⁡ F → y ∈ ⦋ X / m⦌ M | [˙X / x]˙ φ ∈ V
10 nfcv ⊢ Ⅎ _ x X
11 nfsbc1v ⊢ Ⅎ x [˙X / x]˙ φ
12 nfcv ⊢ Ⅎ _ x M
13 10 12 nfcsb ⊢ Ⅎ _ x ⦋ X / m⦌ M
14 11 13 nfrab ⊢ Ⅎ _ x y ∈ ⦋ X / m⦌ M | [˙X / x]˙ φ
15 csbeq1 ⊢ x = X → ⦋ x / m⦌ M = ⦋ X / m⦌ M
16 sbceq1a ⊢ x = X → φ ↔ [˙X / x]˙ φ
17 15 16 rabeqbidv ⊢ x = X → y ∈ ⦋ x / m⦌ M | φ = y ∈ ⦋ X / m⦌ M | [˙X / x]˙ φ
18 10 14 17 1 fvmptf ⊢ X ∈ V ∧ y ∈ ⦋ X / m⦌ M | [˙X / x]˙ φ ∈ V → F ⁡ X = y ∈ ⦋ X / m⦌ M | [˙X / x]˙ φ
19 7 9 18 syl2anc ⊢ X ∈ dom ⁡ F → F ⁡ X = y ∈ ⦋ X / m⦌ M | [˙X / x]˙ φ
20 19 eleq2d ⊢ X ∈ dom ⁡ F → Y ∈ F ⁡ X ↔ Y ∈ y ∈ ⦋ X / m⦌ M | [˙X / x]˙ φ
21 elrabi ⊢ Y ∈ y ∈ ⦋ X / m⦌ M | [˙X / x]˙ φ → Y ∈ ⦋ X / m⦌ M
22 7 21 anim12i ⊢ X ∈ dom ⁡ F ∧ Y ∈ y ∈ ⦋ X / m⦌ M | [˙X / x]˙ φ → X ∈ V ∧ Y ∈ ⦋ X / m⦌ M
23 22 ex ⊢ X ∈ dom ⁡ F → Y ∈ y ∈ ⦋ X / m⦌ M | [˙X / x]˙ φ → X ∈ V ∧ Y ∈ ⦋ X / m⦌ M
24 20 23 sylbid ⊢ X ∈ dom ⁡ F → Y ∈ F ⁡ X → X ∈ V ∧ Y ∈ ⦋ X / m⦌ M
25 3 5 24 3syl ⊢ Y ∈ F ⁡ X → Y ∈ F ⁡ X → X ∈ V ∧ Y ∈ ⦋ X / m⦌ M
26 25 pm2.43i ⊢ Y ∈ F ⁡ X → X ∈ V ∧ Y ∈ ⦋ X / m⦌ M