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	⊢ ( 𝜑 → ( 𝐴 𝑅 𝐵 ↔ ( 𝐴 𝐹 𝐵 ) ≠ ∅ ) )