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	sseldi	⊢ ( ( ( 𝑅 × { 𝑌 } ) ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ≠ ∅ → ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑅 )
12	7 11	syl6bi	⊢ ( 𝜑 → ( ( 𝐴 𝐹 𝐵 ) ≠ ∅ → ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑅 ) )
13	3 12	mpd	⊢ ( 𝜑 → ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑅 )
14		df-br	⊢ ( 𝐴 𝑅 𝐵 ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑅 )
15	13 14	sylibr	⊢ ( 𝜑 → 𝐴 𝑅 𝐵 )