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

Metamath Proof Explorer

Theorem fvconstrn0

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

Ref Expression
Hypotheses fvconstr.1 ⊢ ( 𝜑 → 𝐹 = ( 𝑅 × { 𝑌 } ) )
fvconstr.2 ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
fvconstr.3 ⊢ ( 𝜑 → 𝑌 ≠ ∅ )
Assertion fvconstrn0 ( 𝜑 → ( 𝐴 𝑅 𝐵 ↔ ( 𝐴 𝐹 𝐵 ) ≠ ∅ ) )

Proof

Step Hyp Ref Expression
1 fvconstr.1 ⊢ ( 𝜑 → 𝐹 = ( 𝑅 × { 𝑌 } ) )
2 fvconstr.2 ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
3 fvconstr.3 ⊢ ( 𝜑 → 𝑌 ≠ ∅ )
4 df-br ⊢ ( 𝐴 𝑅 𝐵 ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑅 )
5 1 oveqd ⊢ ( 𝜑 → ( 𝐴 𝐹 𝐵 ) = ( 𝐴 ( 𝑅 × { 𝑌 } ) 𝐵 ) )
6 df-ov ⊢ ( 𝐴 ( 𝑅 × { 𝑌 } ) 𝐵 ) = ( ( 𝑅 × { 𝑌 } ) ‘ ⟨ 𝐴 , 𝐵 ⟩ )
7 5 6 eqtrdi ⊢ ( 𝜑 → ( 𝐴 𝐹 𝐵 ) = ( ( 𝑅 × { 𝑌 } ) ‘ ⟨ 𝐴 , 𝐵 ⟩ ) )
8 7 adantr ⊢ ( ( 𝜑 ∧ ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑅 ) → ( 𝐴 𝐹 𝐵 ) = ( ( 𝑅 × { 𝑌 } ) ‘ ⟨ 𝐴 , 𝐵 ⟩ ) )
9 fvconst2g ⊢ ( ( 𝑌 ∈ 𝑉 ∧ ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑅 ) → ( ( 𝑅 × { 𝑌 } ) ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = 𝑌 )
10 2 9 sylan ⊢ ( ( 𝜑 ∧ ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑅 ) → ( ( 𝑅 × { 𝑌 } ) ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = 𝑌 )
11 8 10 eqtrd ⊢ ( ( 𝜑 ∧ ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑅 ) → ( 𝐴 𝐹 𝐵 ) = 𝑌 )
12 3 adantr ⊢ ( ( 𝜑 ∧ ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑅 ) → 𝑌 ≠ ∅ )
13 11 12 eqnetrd ⊢ ( ( 𝜑 ∧ ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑅 ) → ( 𝐴 𝐹 𝐵 ) ≠ ∅ )
14 7 neeq1d ⊢ ( 𝜑 → ( ( 𝐴 𝐹 𝐵 ) ≠ ∅ ↔ ( ( 𝑅 × { 𝑌 } ) ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ≠ ∅ ) )
15 14 biimpa ⊢ ( ( 𝜑 ∧ ( 𝐴 𝐹 𝐵 ) ≠ ∅ ) → ( ( 𝑅 × { 𝑌 } ) ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ≠ ∅ )
16 dmxpss ⊢ dom ( 𝑅 × { 𝑌 } ) ⊆ 𝑅
17 ndmfv ⊢ ( ¬ ⟨ 𝐴 , 𝐵 ⟩ ∈ dom ( 𝑅 × { 𝑌 } ) → ( ( 𝑅 × { 𝑌 } ) ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = ∅ )
18 17 necon1ai ⊢ ( ( ( 𝑅 × { 𝑌 } ) ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ≠ ∅ → ⟨ 𝐴 , 𝐵 ⟩ ∈ dom ( 𝑅 × { 𝑌 } ) )
19 16 18 sselid ⊢ ( ( ( 𝑅 × { 𝑌 } ) ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ≠ ∅ → ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑅 )
20 15 19 syl ⊢ ( ( 𝜑 ∧ ( 𝐴 𝐹 𝐵 ) ≠ ∅ ) → ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑅 )
21 13 20 impbida ⊢ ( 𝜑 → ( ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑅 ↔ ( 𝐴 𝐹 𝐵 ) ≠ ∅ ) )
22 4 21 bitrid ⊢ ( 𝜑 → ( 𝐴 𝑅 𝐵 ↔ ( 𝐴 𝐹 𝐵 ) ≠ ∅ ) )