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

Metamath Proof Explorer

Theorem elfvmptrab1w

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. Version of elfvmptrab1 with a disjoint variable condition, which does not require ax-13 . (Contributed by Alexander van der Vekens, 15-Jul-2018) Avoid ax-13 . (Revised by GG, 26-Jan-2024)

Ref Expression
Hypotheses elfvmptrab1w.f ⊢ 𝐹 = ( 𝑥 ∈ 𝑉 ↦ { 𝑦 ∈ ⦋ 𝑥 / 𝑚 ⦌ 𝑀 ∣ 𝜑 } )
elfvmptrab1w.v ⊢ ( 𝑋 ∈ 𝑉 → ⦋ 𝑋 / 𝑚 ⦌ 𝑀 ∈ V )
Assertion elfvmptrab1w ( 𝑌 ∈ ( 𝐹 ‘ 𝑋 ) → ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ ⦋ 𝑋 / 𝑚 ⦌ 𝑀 ) )

Proof

Step Hyp Ref Expression
1 elfvmptrab1w.f ⊢ 𝐹 = ( 𝑥 ∈ 𝑉 ↦ { 𝑦 ∈ ⦋ 𝑥 / 𝑚 ⦌ 𝑀 ∣ 𝜑 } )
2 elfvmptrab1w.v ⊢ ( 𝑋 ∈ 𝑉 → ⦋ 𝑋 / 𝑚 ⦌ 𝑀 ∈ V )
3 elfvdm ⊢ ( 𝑌 ∈ ( 𝐹 ‘ 𝑋 ) → 𝑋 ∈ dom 𝐹 )
4 1 dmmptss ⊢ dom 𝐹 ⊆ 𝑉
5 4 sseli ⊢ ( 𝑋 ∈ dom 𝐹 → 𝑋 ∈ 𝑉 )
6 rabexg ⊢ ( ⦋ 𝑋 / 𝑚 ⦌ 𝑀 ∈ V → { 𝑦 ∈ ⦋ 𝑋 / 𝑚 ⦌ 𝑀 ∣ [ 𝑋 / 𝑥 ] 𝜑 } ∈ V )
7 5 2 6 3syl ⊢ ( 𝑋 ∈ dom 𝐹 → { 𝑦 ∈ ⦋ 𝑋 / 𝑚 ⦌ 𝑀 ∣ [ 𝑋 / 𝑥 ] 𝜑 } ∈ V )
8 nfcv ⊢ Ⅎ 𝑥 𝑋
9 nfsbc1v ⊢ Ⅎ 𝑥 [ 𝑋 / 𝑥 ] 𝜑
10 nfcv ⊢ Ⅎ 𝑥 𝑀
11 8 10 nfcsbw ⊢ Ⅎ 𝑥 ⦋ 𝑋 / 𝑚 ⦌ 𝑀
12 9 11 nfrabw ⊢ Ⅎ 𝑥 { 𝑦 ∈ ⦋ 𝑋 / 𝑚 ⦌ 𝑀 ∣ [ 𝑋 / 𝑥 ] 𝜑 }
13 csbeq1 ⊢ ( 𝑥 = 𝑋 → ⦋ 𝑥 / 𝑚 ⦌ 𝑀 = ⦋ 𝑋 / 𝑚 ⦌ 𝑀 )
14 sbceq1a ⊢ ( 𝑥 = 𝑋 → ( 𝜑 ↔ [ 𝑋 / 𝑥 ] 𝜑 ) )
15 13 14 rabeqbidv ⊢ ( 𝑥 = 𝑋 → { 𝑦 ∈ ⦋ 𝑥 / 𝑚 ⦌ 𝑀 ∣ 𝜑 } = { 𝑦 ∈ ⦋ 𝑋 / 𝑚 ⦌ 𝑀 ∣ [ 𝑋 / 𝑥 ] 𝜑 } )
16 8 12 15 1 fvmptf ⊢ ( ( 𝑋 ∈ 𝑉 ∧ { 𝑦 ∈ ⦋ 𝑋 / 𝑚 ⦌ 𝑀 ∣ [ 𝑋 / 𝑥 ] 𝜑 } ∈ V ) → ( 𝐹 ‘ 𝑋 ) = { 𝑦 ∈ ⦋ 𝑋 / 𝑚 ⦌ 𝑀 ∣ [ 𝑋 / 𝑥 ] 𝜑 } )
17 5 7 16 syl2anc ⊢ ( 𝑋 ∈ dom 𝐹 → ( 𝐹 ‘ 𝑋 ) = { 𝑦 ∈ ⦋ 𝑋 / 𝑚 ⦌ 𝑀 ∣ [ 𝑋 / 𝑥 ] 𝜑 } )
18 17 eleq2d ⊢ ( 𝑋 ∈ dom 𝐹 → ( 𝑌 ∈ ( 𝐹 ‘ 𝑋 ) ↔ 𝑌 ∈ { 𝑦 ∈ ⦋ 𝑋 / 𝑚 ⦌ 𝑀 ∣ [ 𝑋 / 𝑥 ] 𝜑 } ) )
19 elrabi ⊢ ( 𝑌 ∈ { 𝑦 ∈ ⦋ 𝑋 / 𝑚 ⦌ 𝑀 ∣ [ 𝑋 / 𝑥 ] 𝜑 } → 𝑌 ∈ ⦋ 𝑋 / 𝑚 ⦌ 𝑀 )
20 5 19 anim12i ⊢ ( ( 𝑋 ∈ dom 𝐹 ∧ 𝑌 ∈ { 𝑦 ∈ ⦋ 𝑋 / 𝑚 ⦌ 𝑀 ∣ [ 𝑋 / 𝑥 ] 𝜑 } ) → ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ ⦋ 𝑋 / 𝑚 ⦌ 𝑀 ) )
21 20 ex ⊢ ( 𝑋 ∈ dom 𝐹 → ( 𝑌 ∈ { 𝑦 ∈ ⦋ 𝑋 / 𝑚 ⦌ 𝑀 ∣ [ 𝑋 / 𝑥 ] 𝜑 } → ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ ⦋ 𝑋 / 𝑚 ⦌ 𝑀 ) ) )
22 18 21 sylbid ⊢ ( 𝑋 ∈ dom 𝐹 → ( 𝑌 ∈ ( 𝐹 ‘ 𝑋 ) → ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ ⦋ 𝑋 / 𝑚 ⦌ 𝑀 ) ) )
23 3 22 mpcom ⊢ ( 𝑌 ∈ ( 𝐹 ‘ 𝑋 ) → ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ ⦋ 𝑋 / 𝑚 ⦌ 𝑀 ) )