fvconstr2

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

Step	Hyp	Ref	Expression
1		fvconstr.1	$⊢ φ \to F = R \times \{Y\}$
2		fvconstr2.2	$⊢ φ \to X \in (A F B)$
3	2	ne0d	$⊢ φ \to A F B \neq \emptyset$
4	1	oveqd	$⊢ φ \to A F B = A (R \times \{Y\}) B$
5		df-ov	$⊢ A (R \times \{Y\}) B = (R \times \{Y\}) (⟨A, B⟩)$
6	4 5	eqtrdi	$⊢ φ \to A F B = (R \times \{Y\}) (⟨A, B⟩)$
7	6	neeq1d	$⊢ φ \to (A F B \neq \emptyset \leftrightarrow (R \times \{Y\}) (⟨A, B⟩) \neq \emptyset)$
8		dmxpss	$⊢ dom (R \times \{Y\}) \subseteq R$
9		ndmfv	$⊢ \neg ⟨A, B⟩ \in dom (R \times \{Y\}) \to (R \times \{Y\}) (⟨A, B⟩) = \emptyset$
10	9	necon1ai	$⊢ (R \times \{Y\}) (⟨A, B⟩) \neq \emptyset \to ⟨A, B⟩ \in dom (R \times \{Y\})$
11	8 10	sselid	$⊢ (R \times \{Y\}) (⟨A, B⟩) \neq \emptyset \to ⟨A, B⟩ \in R$
12	7 11	biimtrdi	$⊢ φ \to (A F B \neq \emptyset \to ⟨A, B⟩ \in R)$
13	3 12	mpd	$⊢ φ \to ⟨A, B⟩ \in R$
14		df-br	$⊢ A R B \leftrightarrow ⟨A, B⟩ \in R$
15	13 14	sylibr	$⊢ φ \to A R B$

Metamath Proof Explorer