ofc12

Description: Function operation on two constant functions. (Contributed by Mario Carneiro, 28-Jul-2014)

	Ref	Expression
Hypotheses	ofc12.1	$⊢ φ \to A \in V$
	ofc12.2	$⊢ φ \to B \in W$
	ofc12.3	$⊢ φ \to C \in X$
Assertion	ofc12	$⊢ φ \to (A \times \{B\}) R_{f} (A \times \{C\}) = A \times \{B R C\}$

Step	Hyp	Ref	Expression
1		ofc12.1	$⊢ φ \to A \in V$
2		ofc12.2	$⊢ φ \to B \in W$
3		ofc12.3	$⊢ φ \to C \in X$
4	2	adantr	$⊢ (φ \land x \in A) \to B \in W$
5	3	adantr	$⊢ (φ \land x \in A) \to C \in X$
6		fconstmpt	$⊢ A \times \{B\} = (x \in A ⟼ B)$
7	6	a1i	$⊢ φ \to A \times \{B\} = (x \in A ⟼ B)$
8		fconstmpt	$⊢ A \times \{C\} = (x \in A ⟼ C)$
9	8	a1i	$⊢ φ \to A \times \{C\} = (x \in A ⟼ C)$
10	1 4 5 7 9	offval2	$⊢ φ \to (A \times \{B\}) R_{f} (A \times \{C\}) = (x \in A ⟼ B R C)$
11		fconstmpt	$⊢ A \times \{B R C\} = (x \in A ⟼ B R C)$
12	10 11	eqtr4di	$⊢ φ \to (A \times \{B\}) R_{f} (A \times \{C\}) = A \times \{B R C\}$

Metamath Proof Explorer