# Metamath Proof Explorer

## Theorem fvmptrabdm

Description: Value of a function mapping a set to a class abstraction restricting the value of another function. See also fvmptrabfv . (Suggested by BJ, 18-Feb-2022.) (Contributed by AV, 18-Feb-2022)

Ref Expression
Hypotheses fvmptrabdm.f 𝐹 = ( 𝑥𝑉 ↦ { 𝑦 ∈ ( 𝐺𝑌 ) ∣ 𝜑 } )
fvmptrabdm.r ( 𝑥 = 𝑋 → ( 𝜑𝜓 ) )
fvmptrabdm.v ( 𝑌 ∈ dom 𝐺𝑋 ∈ dom 𝐹 )
Assertion fvmptrabdm ( 𝐹𝑋 ) = { 𝑦 ∈ ( 𝐺𝑌 ) ∣ 𝜓 }

### Proof

Step Hyp Ref Expression
1 fvmptrabdm.f 𝐹 = ( 𝑥𝑉 ↦ { 𝑦 ∈ ( 𝐺𝑌 ) ∣ 𝜑 } )
2 fvmptrabdm.r ( 𝑥 = 𝑋 → ( 𝜑𝜓 ) )
3 fvmptrabdm.v ( 𝑌 ∈ dom 𝐺𝑋 ∈ dom 𝐹 )
4 pm2.1 ( ¬ 𝑋 ∈ dom 𝐹𝑋 ∈ dom 𝐹 )
5 imor ( ( 𝑌 ∈ dom 𝐺𝑋 ∈ dom 𝐹 ) ↔ ( ¬ 𝑌 ∈ dom 𝐺𝑋 ∈ dom 𝐹 ) )
6 ordir ( ( ( ¬ 𝑋 ∈ dom 𝐹 ∧ ¬ 𝑌 ∈ dom 𝐺 ) ∨ 𝑋 ∈ dom 𝐹 ) ↔ ( ( ¬ 𝑋 ∈ dom 𝐹𝑋 ∈ dom 𝐹 ) ∧ ( ¬ 𝑌 ∈ dom 𝐺𝑋 ∈ dom 𝐹 ) ) )
7 ndmfv ( ¬ 𝑋 ∈ dom 𝐹 → ( 𝐹𝑋 ) = ∅ )
8 ndmfv ( ¬ 𝑌 ∈ dom 𝐺 → ( 𝐺𝑌 ) = ∅ )
9 8 rabeqdv ( ¬ 𝑌 ∈ dom 𝐺 → { 𝑦 ∈ ( 𝐺𝑌 ) ∣ 𝜓 } = { 𝑦 ∈ ∅ ∣ 𝜓 } )
10 rab0 { 𝑦 ∈ ∅ ∣ 𝜓 } = ∅
11 9 10 eqtr2di ( ¬ 𝑌 ∈ dom 𝐺 → ∅ = { 𝑦 ∈ ( 𝐺𝑌 ) ∣ 𝜓 } )
12 7 11 sylan9eq ( ( ¬ 𝑋 ∈ dom 𝐹 ∧ ¬ 𝑌 ∈ dom 𝐺 ) → ( 𝐹𝑋 ) = { 𝑦 ∈ ( 𝐺𝑌 ) ∣ 𝜓 } )
13 2 rabbidv ( 𝑥 = 𝑋 → { 𝑦 ∈ ( 𝐺𝑌 ) ∣ 𝜑 } = { 𝑦 ∈ ( 𝐺𝑌 ) ∣ 𝜓 } )
14 1 dmmpt dom 𝐹 = { 𝑥𝑉 ∣ { 𝑦 ∈ ( 𝐺𝑌 ) ∣ 𝜑 } ∈ V }
15 rabid2 ( 𝑉 = { 𝑥𝑉 ∣ { 𝑦 ∈ ( 𝐺𝑌 ) ∣ 𝜑 } ∈ V } ↔ ∀ 𝑥𝑉 { 𝑦 ∈ ( 𝐺𝑌 ) ∣ 𝜑 } ∈ V )
16 fvex ( 𝐺𝑌 ) ∈ V
17 16 rabex { 𝑦 ∈ ( 𝐺𝑌 ) ∣ 𝜑 } ∈ V
18 17 a1i ( 𝑥𝑉 → { 𝑦 ∈ ( 𝐺𝑌 ) ∣ 𝜑 } ∈ V )
19 15 18 mprgbir 𝑉 = { 𝑥𝑉 ∣ { 𝑦 ∈ ( 𝐺𝑌 ) ∣ 𝜑 } ∈ V }
20 14 19 eqtr4i dom 𝐹 = 𝑉
21 20 eleq2i ( 𝑋 ∈ dom 𝐹𝑋𝑉 )
22 21 biimpi ( 𝑋 ∈ dom 𝐹𝑋𝑉 )
23 16 rabex { 𝑦 ∈ ( 𝐺𝑌 ) ∣ 𝜓 } ∈ V
24 23 a1i ( 𝑋 ∈ dom 𝐹 → { 𝑦 ∈ ( 𝐺𝑌 ) ∣ 𝜓 } ∈ V )
25 1 13 22 24 fvmptd3 ( 𝑋 ∈ dom 𝐹 → ( 𝐹𝑋 ) = { 𝑦 ∈ ( 𝐺𝑌 ) ∣ 𝜓 } )
26 12 25 jaoi ( ( ( ¬ 𝑋 ∈ dom 𝐹 ∧ ¬ 𝑌 ∈ dom 𝐺 ) ∨ 𝑋 ∈ dom 𝐹 ) → ( 𝐹𝑋 ) = { 𝑦 ∈ ( 𝐺𝑌 ) ∣ 𝜓 } )
27 6 26 sylbir ( ( ( ¬ 𝑋 ∈ dom 𝐹𝑋 ∈ dom 𝐹 ) ∧ ( ¬ 𝑌 ∈ dom 𝐺𝑋 ∈ dom 𝐹 ) ) → ( 𝐹𝑋 ) = { 𝑦 ∈ ( 𝐺𝑌 ) ∣ 𝜓 } )
28 27 expcom ( ( ¬ 𝑌 ∈ dom 𝐺𝑋 ∈ dom 𝐹 ) → ( ( ¬ 𝑋 ∈ dom 𝐹𝑋 ∈ dom 𝐹 ) → ( 𝐹𝑋 ) = { 𝑦 ∈ ( 𝐺𝑌 ) ∣ 𝜓 } ) )
29 5 28 sylbi ( ( 𝑌 ∈ dom 𝐺𝑋 ∈ dom 𝐹 ) → ( ( ¬ 𝑋 ∈ dom 𝐹𝑋 ∈ dom 𝐹 ) → ( 𝐹𝑋 ) = { 𝑦 ∈ ( 𝐺𝑌 ) ∣ 𝜓 } ) )
30 3 4 29 mp2 ( 𝐹𝑋 ) = { 𝑦 ∈ ( 𝐺𝑌 ) ∣ 𝜓 }