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 ⊢ ( 𝐹 ‘ 𝑋 ) = { 𝑦 ∈ ( 𝐺 ‘ 𝑌 ) ∣ 𝜓 }