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

Metamath Proof Explorer

Theorem of0r

Description: Function operation with the empty function. (Contributed by Thierry Arnoux, 27-May-2025)

Ref Expression
Assertion of0r ( 𝐹 ∘f 𝑅 ∅ ) = ∅

Proof

Step Hyp Ref Expression
1 df-of ⊢ ∘f 𝑅 = ( 𝑓 ∈ V , 𝑔 ∈ V ↦ ( 𝑥 ∈ ( dom 𝑓 ∩ dom 𝑔 ) ↦ ( ( 𝑓 ‘ 𝑥 ) 𝑅 ( 𝑔 ‘ 𝑥 ) ) ) )
2 1 a1i ⊢ ( 𝐹 ∈ V → ∘f 𝑅 = ( 𝑓 ∈ V , 𝑔 ∈ V ↦ ( 𝑥 ∈ ( dom 𝑓 ∩ dom 𝑔 ) ↦ ( ( 𝑓 ‘ 𝑥 ) 𝑅 ( 𝑔 ‘ 𝑥 ) ) ) ) )
3 dmeq ⊢ ( 𝑓 = 𝐹 → dom 𝑓 = dom 𝐹 )
4 dmeq ⊢ ( 𝑔 = ∅ → dom 𝑔 = dom ∅ )
5 3 4 ineqan12d ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = ∅ ) → ( dom 𝑓 ∩ dom 𝑔 ) = ( dom 𝐹 ∩ dom ∅ ) )
6 5 mpteq1d ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = ∅ ) → ( 𝑥 ∈ ( dom 𝑓 ∩ dom 𝑔 ) ↦ ( ( 𝑓 ‘ 𝑥 ) 𝑅 ( 𝑔 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ( dom 𝐹 ∩ dom ∅ ) ↦ ( ( 𝑓 ‘ 𝑥 ) 𝑅 ( 𝑔 ‘ 𝑥 ) ) ) )
7 6 adantl ⊢ ( ( 𝐹 ∈ V ∧ ( 𝑓 = 𝐹 ∧ 𝑔 = ∅ ) ) → ( 𝑥 ∈ ( dom 𝑓 ∩ dom 𝑔 ) ↦ ( ( 𝑓 ‘ 𝑥 ) 𝑅 ( 𝑔 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ( dom 𝐹 ∩ dom ∅ ) ↦ ( ( 𝑓 ‘ 𝑥 ) 𝑅 ( 𝑔 ‘ 𝑥 ) ) ) )
8 dm0 ⊢ dom ∅ = ∅
9 8 ineq2i ⊢ ( dom 𝐹 ∩ dom ∅ ) = ( dom 𝐹 ∩ ∅ )
10 in0 ⊢ ( dom 𝐹 ∩ ∅ ) = ∅
11 9 10 eqtri ⊢ ( dom 𝐹 ∩ dom ∅ ) = ∅
12 11 a1i ⊢ ( ( 𝐹 ∈ V ∧ ( 𝑓 = 𝐹 ∧ 𝑔 = ∅ ) ) → ( dom 𝐹 ∩ dom ∅ ) = ∅ )
13 12 mpteq1d ⊢ ( ( 𝐹 ∈ V ∧ ( 𝑓 = 𝐹 ∧ 𝑔 = ∅ ) ) → ( 𝑥 ∈ ( dom 𝐹 ∩ dom ∅ ) ↦ ( ( 𝑓 ‘ 𝑥 ) 𝑅 ( 𝑔 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ∅ ↦ ( ( 𝑓 ‘ 𝑥 ) 𝑅 ( 𝑔 ‘ 𝑥 ) ) ) )
14 mpt0 ⊢ ( 𝑥 ∈ ∅ ↦ ( ( 𝑓 ‘ 𝑥 ) 𝑅 ( 𝑔 ‘ 𝑥 ) ) ) = ∅
15 14 a1i ⊢ ( ( 𝐹 ∈ V ∧ ( 𝑓 = 𝐹 ∧ 𝑔 = ∅ ) ) → ( 𝑥 ∈ ∅ ↦ ( ( 𝑓 ‘ 𝑥 ) 𝑅 ( 𝑔 ‘ 𝑥 ) ) ) = ∅ )
16 7 13 15 3eqtrd ⊢ ( ( 𝐹 ∈ V ∧ ( 𝑓 = 𝐹 ∧ 𝑔 = ∅ ) ) → ( 𝑥 ∈ ( dom 𝑓 ∩ dom 𝑔 ) ↦ ( ( 𝑓 ‘ 𝑥 ) 𝑅 ( 𝑔 ‘ 𝑥 ) ) ) = ∅ )
17 id ⊢ ( 𝐹 ∈ V → 𝐹 ∈ V )
18 0ex ⊢ ∅ ∈ V
19 18 a1i ⊢ ( 𝐹 ∈ V → ∅ ∈ V )
20 2 16 17 19 19 ovmpod ⊢ ( 𝐹 ∈ V → ( 𝐹 ∘f 𝑅 ∅ ) = ∅ )
21 1 reldmmpo ⊢ Rel dom ∘f 𝑅
22 21 ovprc1 ⊢ ( ¬ 𝐹 ∈ V → ( 𝐹 ∘f 𝑅 ∅ ) = ∅ )
23 20 22 pm2.61i ⊢ ( 𝐹 ∘f 𝑅 ∅ ) = ∅