Theorem fvconstr

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

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

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		simpr	⊢ ( ( 𝜑 ∧ ( 𝐴 𝐹 𝐵 ) = 𝑌 ) → ( 𝐴 𝐹 𝐵 ) = 𝑌 )
13	3	adantr	⊢ ( ( 𝜑 ∧ ( 𝐴 𝐹 𝐵 ) = 𝑌 ) → 𝑌 ≠ ∅ )
14	12 13	eqnetrd	⊢ ( ( 𝜑 ∧ ( 𝐴 𝐹 𝐵 ) = 𝑌 ) → ( 𝐴 𝐹 𝐵 ) ≠ ∅ )
15	7	neeq1d	⊢ ( 𝜑 → ( ( 𝐴 𝐹 𝐵 ) ≠ ∅ ↔ ( ( 𝑅 × { 𝑌 } ) ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ≠ ∅ ) )
16	15	adantr	⊢ ( ( 𝜑 ∧ ( 𝐴 𝐹 𝐵 ) = 𝑌 ) → ( ( 𝐴 𝐹 𝐵 ) ≠ ∅ ↔ ( ( 𝑅 × { 𝑌 } ) ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ≠ ∅ ) )
17	14 16	mpbid	⊢ ( ( 𝜑 ∧ ( 𝐴 𝐹 𝐵 ) = 𝑌 ) → ( ( 𝑅 × { 𝑌 } ) ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ≠ ∅ )
18		dmxpss	⊢ dom ( 𝑅 × { 𝑌 } ) ⊆ 𝑅
19		ndmfv	⊢ ( ¬ ⟨ 𝐴 , 𝐵 ⟩ ∈ dom ( 𝑅 × { 𝑌 } ) → ( ( 𝑅 × { 𝑌 } ) ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = ∅ )
20	19	necon1ai	⊢ ( ( ( 𝑅 × { 𝑌 } ) ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ≠ ∅ → ⟨ 𝐴 , 𝐵 ⟩ ∈ dom ( 𝑅 × { 𝑌 } ) )
21	18 20	sselid	⊢ ( ( ( 𝑅 × { 𝑌 } ) ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ≠ ∅ → ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑅 )
22	17 21	syl	⊢ ( ( 𝜑 ∧ ( 𝐴 𝐹 𝐵 ) = 𝑌 ) → ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑅 )
23	11 22	impbida	⊢ ( 𝜑 → ( ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑅 ↔ ( 𝐴 𝐹 𝐵 ) = 𝑌 ) )
24	4 23	bitrid	⊢ ( 𝜑 → ( 𝐴 𝑅 𝐵 ↔ ( 𝐴 𝐹 𝐵 ) = 𝑌 ) )