Metamath Proof Explorer

Theorem elovmpoeq

Description: If a value of an operation given by maps-to notation has a member, it equals the substituted body. (Contributed by Zhi Wang, 17-Sep-2026)

Ref Expression
Hypotheses elovmpoeq.f ⊢ 𝐹 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 )
elovmpoeq.s ⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → 𝐶 = 𝐷 )
Assertion elovmpoeq ( 𝑁 ∈ ( 𝑋 𝐹 𝑌 ) → ( 𝑋 𝐹 𝑌 ) = 𝐷 )

Proof

Step Hyp Ref Expression
1 elovmpoeq.f ⊢ 𝐹 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 )
2 elovmpoeq.s ⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → 𝐶 = 𝐷 )
3 ne0i ⊢ ( 𝑁 ∈ ( 𝑋 𝐹 𝑌 ) → ( 𝑋 𝐹 𝑌 ) ≠ ∅ )
4 df-ov ⊢ ( 𝑋 𝐹 𝑌 ) = ( 𝐹 ‘ ⟨ 𝑋 , 𝑌 ⟩ )
5 4 eqcomi ⊢ ( 𝐹 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = ( 𝑋 𝐹 𝑌 )
6 tz6.12i ⊢ ( ( 𝑋 𝐹 𝑌 ) ≠ ∅ → ( ( 𝐹 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = ( 𝑋 𝐹 𝑌 ) → ⟨ 𝑋 , 𝑌 ⟩ 𝐹 ( 𝑋 𝐹 𝑌 ) ) )
7 3 5 6 mpisyl ⊢ ( 𝑁 ∈ ( 𝑋 𝐹 𝑌 ) → ⟨ 𝑋 , 𝑌 ⟩ 𝐹 ( 𝑋 𝐹 𝑌 ) )
8 df-br ⊢ ( ⟨ 𝑋 , 𝑌 ⟩ 𝐹 ( 𝑋 𝐹 𝑌 ) ↔ ⟨ ⟨ 𝑋 , 𝑌 ⟩ , ( 𝑋 𝐹 𝑌 ) ⟩ ∈ 𝐹 )
9 7 8 sylib ⊢ ( 𝑁 ∈ ( 𝑋 𝐹 𝑌 ) → ⟨ ⟨ 𝑋 , 𝑌 ⟩ , ( 𝑋 𝐹 𝑌 ) ⟩ ∈ 𝐹 )
10 df-mpo ⊢ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) }
11 1 10 eqtri ⊢ 𝐹 = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) }
12 9 11 eleqtrdi ⊢ ( 𝑁 ∈ ( 𝑋 𝐹 𝑌 ) → ⟨ ⟨ 𝑋 , 𝑌 ⟩ , ( 𝑋 𝐹 𝑌 ) ⟩ ∈ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) } )
13 1 elmpocl1 ⊢ ( 𝑁 ∈ ( 𝑋 𝐹 𝑌 ) → 𝑋 ∈ 𝐴 )
14 13 elexd ⊢ ( 𝑁 ∈ ( 𝑋 𝐹 𝑌 ) → 𝑋 ∈ V )
15 1 elmpocl2 ⊢ ( 𝑁 ∈ ( 𝑋 𝐹 𝑌 ) → 𝑌 ∈ 𝐵 )
16 15 elexd ⊢ ( 𝑁 ∈ ( 𝑋 𝐹 𝑌 ) → 𝑌 ∈ V )
17 ovexd ⊢ ( 𝑁 ∈ ( 𝑋 𝐹 𝑌 ) → ( 𝑋 𝐹 𝑌 ) ∈ V )
18 simp1 ⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ∧ 𝑧 = ( 𝑋 𝐹 𝑌 ) ) → 𝑥 = 𝑋 )
19 18 eleq1d ⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ∧ 𝑧 = ( 𝑋 𝐹 𝑌 ) ) → ( 𝑥 ∈ 𝐴 ↔ 𝑋 ∈ 𝐴 ) )
20 simp2 ⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ∧ 𝑧 = ( 𝑋 𝐹 𝑌 ) ) → 𝑦 = 𝑌 )
21 20 eleq1d ⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ∧ 𝑧 = ( 𝑋 𝐹 𝑌 ) ) → ( 𝑦 ∈ 𝐵 ↔ 𝑌 ∈ 𝐵 ) )
22 19 21 anbi12d ⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ∧ 𝑧 = ( 𝑋 𝐹 𝑌 ) ) → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ↔ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) ) )
23 simp3 ⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ∧ 𝑧 = ( 𝑋 𝐹 𝑌 ) ) → 𝑧 = ( 𝑋 𝐹 𝑌 ) )
24 2 3adant3 ⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ∧ 𝑧 = ( 𝑋 𝐹 𝑌 ) ) → 𝐶 = 𝐷 )
25 23 24 eqeq12d ⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ∧ 𝑧 = ( 𝑋 𝐹 𝑌 ) ) → ( 𝑧 = 𝐶 ↔ ( 𝑋 𝐹 𝑌 ) = 𝐷 ) )
26 22 25 anbi12d ⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ∧ 𝑧 = ( 𝑋 𝐹 𝑌 ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) ↔ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑋 𝐹 𝑌 ) = 𝐷 ) ) )
27 26 eloprabga ⊢ ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ∧ ( 𝑋 𝐹 𝑌 ) ∈ V ) → ( ⟨ ⟨ 𝑋 , 𝑌 ⟩ , ( 𝑋 𝐹 𝑌 ) ⟩ ∈ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) } ↔ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑋 𝐹 𝑌 ) = 𝐷 ) ) )
28 14 16 17 27 syl3anc ⊢ ( 𝑁 ∈ ( 𝑋 𝐹 𝑌 ) → ( ⟨ ⟨ 𝑋 , 𝑌 ⟩ , ( 𝑋 𝐹 𝑌 ) ⟩ ∈ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) } ↔ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑋 𝐹 𝑌 ) = 𝐷 ) ) )
29 12 28 mpbid ⊢ ( 𝑁 ∈ ( 𝑋 𝐹 𝑌 ) → ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑋 𝐹 𝑌 ) = 𝐷 ) )
30 29 simprd ⊢ ( 𝑁 ∈ ( 𝑋 𝐹 𝑌 ) → ( 𝑋 𝐹 𝑌 ) = 𝐷 )