fvconstr

Description: Two ways of expressing A R B . (Contributed by Zhi Wang, 18-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	fvconstr	$⊢ φ \to (A R B \leftrightarrow A F B = Y)$

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		simpr	$⊢ (φ \land A F B = Y) \to A F B = Y$
13	3	adantr	$⊢ (φ \land A F B = Y) \to Y \neq \emptyset$
14	12 13	eqnetrd	$⊢ (φ \land A F B = Y) \to A F B \neq \emptyset$
15	7	neeq1d	$⊢ φ \to (A F B \neq \emptyset \leftrightarrow (R \times \{Y\}) (⟨A, B⟩) \neq \emptyset)$
16	15	adantr	$⊢ (φ \land A F B = Y) \to (A F B \neq \emptyset \leftrightarrow (R \times \{Y\}) (⟨A, B⟩) \neq \emptyset)$
17	14 16	mpbid	$⊢ (φ \land A F B = Y) \to (R \times \{Y\}) (⟨A, B⟩) \neq \emptyset$
18		dmxpss	$⊢ dom (R \times \{Y\}) \subseteq R$
19		ndmfv	$⊢ \neg ⟨A, B⟩ \in dom (R \times \{Y\}) \to (R \times \{Y\}) (⟨A, B⟩) = \emptyset$
20	19	necon1ai	$⊢ (R \times \{Y\}) (⟨A, B⟩) \neq \emptyset \to ⟨A, B⟩ \in dom (R \times \{Y\})$
21	18 20	sselid	$⊢ (R \times \{Y\}) (⟨A, B⟩) \neq \emptyset \to ⟨A, B⟩ \in R$
22	17 21	syl	$⊢ (φ \land A F B = Y) \to ⟨A, B⟩ \in R$
23	11 22	impbida	$⊢ φ \to (⟨A, B⟩ \in R \leftrightarrow A F B = Y)$
24	4 23	bitrid	$⊢ φ \to (A R B \leftrightarrow A F B = Y)$

Metamath Proof Explorer

Theorem fvconstr

Proof