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 ⊢ 𝐹 = ( 𝑥 ∈ 𝑉 ↦ { 𝑦 ∈ ⦋ 𝑥 / 𝑚 ⦌ 𝑀 ∣ 𝜑 } )
elfvmptrab1.v ⊢ ( 𝑋 ∈ 𝑉 → ⦋ 𝑋 / 𝑚 ⦌ 𝑀 ∈ V )
Assertion elfvmptrab1 ( 𝑌 ∈ ( 𝐹 ‘ 𝑋 ) → ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ ⦋ 𝑋 / 𝑚 ⦌ 𝑀 ) )

Proof

Step Hyp Ref Expression
1 elfvmptrab1.f ⊢ 𝐹 = ( 𝑥 ∈ 𝑉 ↦ { 𝑦 ∈ ⦋ 𝑥 / 𝑚 ⦌ 𝑀 ∣ 𝜑 } )
2 elfvmptrab1.v ⊢ ( 𝑋 ∈ 𝑉 → ⦋ 𝑋 / 𝑚 ⦌ 𝑀 ∈ V )
3 ne0i ⊢ ( 𝑌 ∈ ( 𝐹 ‘ 𝑋 ) → ( 𝐹 ‘ 𝑋 ) ≠ ∅ )
4 ndmfv ⊢ ( ¬ 𝑋 ∈ dom 𝐹 → ( 𝐹 ‘ 𝑋 ) = ∅ )
5 4 necon1ai ⊢ ( ( 𝐹 ‘ 𝑋 ) ≠ ∅ → 𝑋 ∈ dom 𝐹 )
6 1 dmmptss ⊢ dom 𝐹 ⊆ 𝑉
7 6 sseli ⊢ ( 𝑋 ∈ dom 𝐹 → 𝑋 ∈ 𝑉 )
8 rabexg ⊢ ( ⦋ 𝑋 / 𝑚 ⦌ 𝑀 ∈ V → { 𝑦 ∈ ⦋ 𝑋 / 𝑚 ⦌ 𝑀 ∣ [ 𝑋 / 𝑥 ] 𝜑 } ∈ V )
9 7 2 8 3syl ⊢ ( 𝑋 ∈ dom 𝐹 → { 𝑦 ∈ ⦋ 𝑋 / 𝑚 ⦌ 𝑀 ∣ [ 𝑋 / 𝑥 ] 𝜑 } ∈ V )
10 nfcv ⊢ Ⅎ 𝑥 𝑋
11 nfsbc1v ⊢ Ⅎ 𝑥 [ 𝑋 / 𝑥 ] 𝜑
12 nfcv ⊢ Ⅎ 𝑥 𝑀
13 10 12 nfcsb ⊢ Ⅎ 𝑥 ⦋ 𝑋 / 𝑚 ⦌ 𝑀
14 11 13 nfrab ⊢ Ⅎ 𝑥 { 𝑦 ∈ ⦋ 𝑋 / 𝑚 ⦌ 𝑀 ∣ [ 𝑋 / 𝑥 ] 𝜑 }
15 csbeq1 ⊢ ( 𝑥 = 𝑋 → ⦋ 𝑥 / 𝑚 ⦌ 𝑀 = ⦋ 𝑋 / 𝑚 ⦌ 𝑀 )
16 sbceq1a ⊢ ( 𝑥 = 𝑋 → ( 𝜑 ↔ [ 𝑋 / 𝑥 ] 𝜑 ) )
17 15 16 rabeqbidv ⊢ ( 𝑥 = 𝑋 → { 𝑦 ∈ ⦋ 𝑥 / 𝑚 ⦌ 𝑀 ∣ 𝜑 } = { 𝑦 ∈ ⦋ 𝑋 / 𝑚 ⦌ 𝑀 ∣ [ 𝑋 / 𝑥 ] 𝜑 } )
18 10 14 17 1 fvmptf ⊢ ( ( 𝑋 ∈ 𝑉 ∧ { 𝑦 ∈ ⦋ 𝑋 / 𝑚 ⦌ 𝑀 ∣ [ 𝑋 / 𝑥 ] 𝜑 } ∈ V ) → ( 𝐹 ‘ 𝑋 ) = { 𝑦 ∈ ⦋ 𝑋 / 𝑚 ⦌ 𝑀 ∣ [ 𝑋 / 𝑥 ] 𝜑 } )
19 7 9 18 syl2anc ⊢ ( 𝑋 ∈ dom 𝐹 → ( 𝐹 ‘ 𝑋 ) = { 𝑦 ∈ ⦋ 𝑋 / 𝑚 ⦌ 𝑀 ∣ [ 𝑋 / 𝑥 ] 𝜑 } )
20 19 eleq2d ⊢ ( 𝑋 ∈ dom 𝐹 → ( 𝑌 ∈ ( 𝐹 ‘ 𝑋 ) ↔ 𝑌 ∈ { 𝑦 ∈ ⦋ 𝑋 / 𝑚 ⦌ 𝑀 ∣ [ 𝑋 / 𝑥 ] 𝜑 } ) )
21 elrabi ⊢ ( 𝑌 ∈ { 𝑦 ∈ ⦋ 𝑋 / 𝑚 ⦌ 𝑀 ∣ [ 𝑋 / 𝑥 ] 𝜑 } → 𝑌 ∈ ⦋ 𝑋 / 𝑚 ⦌ 𝑀 )
22 7 21 anim12i ⊢ ( ( 𝑋 ∈ dom 𝐹 ∧ 𝑌 ∈ { 𝑦 ∈ ⦋ 𝑋 / 𝑚 ⦌ 𝑀 ∣ [ 𝑋 / 𝑥 ] 𝜑 } ) → ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ ⦋ 𝑋 / 𝑚 ⦌ 𝑀 ) )
23 22 ex ⊢ ( 𝑋 ∈ dom 𝐹 → ( 𝑌 ∈ { 𝑦 ∈ ⦋ 𝑋 / 𝑚 ⦌ 𝑀 ∣ [ 𝑋 / 𝑥 ] 𝜑 } → ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ ⦋ 𝑋 / 𝑚 ⦌ 𝑀 ) ) )
24 20 23 sylbid ⊢ ( 𝑋 ∈ dom 𝐹 → ( 𝑌 ∈ ( 𝐹 ‘ 𝑋 ) → ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ ⦋ 𝑋 / 𝑚 ⦌ 𝑀 ) ) )
25 3 5 24 3syl ⊢ ( 𝑌 ∈ ( 𝐹 ‘ 𝑋 ) → ( 𝑌 ∈ ( 𝐹 ‘ 𝑋 ) → ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ ⦋ 𝑋 / 𝑚 ⦌ 𝑀 ) ) )
26 25 pm2.43i ⊢ ( 𝑌 ∈ ( 𝐹 ‘ 𝑋 ) → ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ ⦋ 𝑋 / 𝑚 ⦌ 𝑀 ) )