fvconstrn0

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

	Ref	Expression
Hypotheses	fvconstr.1	$⊢ φ \to F = R \times \{Y\}$
	fvconstr.2	$⊢ φ \to Y \in V$
	fvconstr.3	$⊢ φ \to Y \neq \emptyset$
Assertion	fvconstrn0	$⊢ φ \to (A R B \leftrightarrow A F B \neq \emptyset)$

Proof

Step	Hyp	Ref	Expression
1		fvconstr.1	$⊢ φ \to F = R \times \{Y\}$
2		fvconstr.2	$⊢ φ \to Y \in V$
3		fvconstr.3	$⊢ φ \to Y \neq \emptyset$
4		df-br	$⊢ A R B \leftrightarrow ⟨A, B⟩ \in R$
5	1	oveqd	$⊢ φ \to A F B = A (R \times \{Y\}) B$
6		df-ov	$⊢ A (R \times \{Y\}) B = (R \times \{Y\}) (⟨A, B⟩)$
7	5 6	eqtrdi	$⊢ φ \to A F B = (R \times \{Y\}) (⟨A, B⟩)$
8	7	adantr	$⊢ (φ \land ⟨A, B⟩ \in R) \to A F B = (R \times \{Y\}) (⟨A, B⟩)$
9		fvconst2g	$⊢ (Y \in V \land ⟨A, B⟩ \in R) \to (R \times \{Y\}) (⟨A, B⟩) = Y$
10	2 9	sylan	$⊢ (φ \land ⟨A, B⟩ \in R) \to (R \times \{Y\}) (⟨A, B⟩) = Y$
11	8 10	eqtrd	$⊢ (φ \land ⟨A, B⟩ \in R) \to A F B = Y$
12	3	adantr	$⊢ (φ \land ⟨A, B⟩ \in R) \to Y \neq \emptyset$
13	11 12	eqnetrd	$⊢ (φ \land ⟨A, B⟩ \in R) \to A F B \neq \emptyset$
14	7	neeq1d	$⊢ φ \to (A F B \neq \emptyset \leftrightarrow (R \times \{Y\}) (⟨A, B⟩) \neq \emptyset)$
15	14	biimpa	$⊢ (φ \land A F B \neq \emptyset) \to (R \times \{Y\}) (⟨A, B⟩) \neq \emptyset$
16		dmxpss	$⊢ dom (R \times \{Y\}) \subseteq R$
17		ndmfv	$⊢ \neg ⟨A, B⟩ \in dom (R \times \{Y\}) \to (R \times \{Y\}) (⟨A, B⟩) = \emptyset$
18	17	necon1ai	$⊢ (R \times \{Y\}) (⟨A, B⟩) \neq \emptyset \to ⟨A, B⟩ \in dom (R \times \{Y\})$
19	16 18	sselid	$⊢ (R \times \{Y\}) (⟨A, B⟩) \neq \emptyset \to ⟨A, B⟩ \in R$
20	15 19	syl	$⊢ (φ \land A F B \neq \emptyset) \to ⟨A, B⟩ \in R$
21	13 20	impbida	$⊢ φ \to (⟨A, B⟩ \in R \leftrightarrow A F B \neq \emptyset)$
22	4 21	syl5bb	$⊢ φ \to (A R B \leftrightarrow A F B \neq \emptyset)$

Metamath Proof Explorer

Theorem fvconstrn0

Proof