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

Metamath Proof Explorer

Theorem fvconstr2

Description: Two ways of expressing A R B . (Contributed by Zhi Wang, 18-Sep-2024)

Ref Expression
Hypotheses fvconstr.1 ⊢ ( 𝜑 → 𝐹 = ( 𝑅 × { 𝑌 } ) )
fvconstr2.2 ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐴 𝐹 𝐵 ) )
Assertion fvconstr2 ( 𝜑 → 𝐴 𝑅 𝐵 )

Proof

Step Hyp Ref Expression
1 fvconstr.1 ⊢ ( 𝜑 → 𝐹 = ( 𝑅 × { 𝑌 } ) )
2 fvconstr2.2 ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐴 𝐹 𝐵 ) )
3 2 ne0d ⊢ ( 𝜑 → ( 𝐴 𝐹 𝐵 ) ≠ ∅ )
4 1 oveqd ⊢ ( 𝜑 → ( 𝐴 𝐹 𝐵 ) = ( 𝐴 ( 𝑅 × { 𝑌 } ) 𝐵 ) )
5 df-ov ⊢ ( 𝐴 ( 𝑅 × { 𝑌 } ) 𝐵 ) = ( ( 𝑅 × { 𝑌 } ) ‘ ⟨ 𝐴 , 𝐵 ⟩ )
6 4 5 eqtrdi ⊢ ( 𝜑 → ( 𝐴 𝐹 𝐵 ) = ( ( 𝑅 × { 𝑌 } ) ‘ ⟨ 𝐴 , 𝐵 ⟩ ) )
7 6 neeq1d ⊢ ( 𝜑 → ( ( 𝐴 𝐹 𝐵 ) ≠ ∅ ↔ ( ( 𝑅 × { 𝑌 } ) ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ≠ ∅ ) )
8 dmxpss ⊢ dom ( 𝑅 × { 𝑌 } ) ⊆ 𝑅
9 ndmfv ⊢ ( ¬ ⟨ 𝐴 , 𝐵 ⟩ ∈ dom ( 𝑅 × { 𝑌 } ) → ( ( 𝑅 × { 𝑌 } ) ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = ∅ )
10 9 necon1ai ⊢ ( ( ( 𝑅 × { 𝑌 } ) ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ≠ ∅ → ⟨ 𝐴 , 𝐵 ⟩ ∈ dom ( 𝑅 × { 𝑌 } ) )
11 8 10 sselid ⊢ ( ( ( 𝑅 × { 𝑌 } ) ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ≠ ∅ → ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑅 )
12 7 11 biimtrdi ⊢ ( 𝜑 → ( ( 𝐴 𝐹 𝐵 ) ≠ ∅ → ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑅 ) )
13 3 12 mpd ⊢ ( 𝜑 → ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑅 )
14 df-br ⊢ ( 𝐴 𝑅 𝐵 ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑅 )
15 13 14 sylibr ⊢ ( 𝜑 → 𝐴 𝑅 𝐵 )