fovcld

Description: Closure law for an operation. (Contributed by NM, 19-Apr-2007) (Revised by Thierry Arnoux, 17-Feb-2017)

		Ref	Expression
	Hypothesis	fovcld.1	$⊢ φ \to F : R \times S ⟶ C$
	Assertion	fovcld	$⊢ (φ \land A \in R \land B \in S) \to A F B \in C$

Step	Hyp	Ref	Expression
1		fovcld.1	$⊢ φ \to F : R \times S ⟶ C$
2		3simpc	$⊢ (φ \land A \in R \land B \in S) \to (A \in R \land B \in S)$
3		ffnov	$⊢ F : R \times S ⟶ C \leftrightarrow (F Fn (R \times S) \land \forall x \in R \forall y \in S x F y \in C)$
4	3	simprbi	$⊢ F : R \times S ⟶ C \to \forall x \in R \forall y \in S x F y \in C$
5	1 4	syl	$⊢ φ \to \forall x \in R \forall y \in S x F y \in C$
6	5	3ad2ant1	$⊢ (φ \land A \in R \land B \in S) \to \forall x \in R \forall y \in S x F y \in C$
7		oveq1	$⊢ x = A \to x F y = A F y$
8	7	eleq1d	$⊢ x = A \to (x F y \in C \leftrightarrow A F y \in C)$
9		oveq2	$⊢ y = B \to A F y = A F B$
10	9	eleq1d	$⊢ y = B \to (A F y \in C \leftrightarrow A F B \in C)$
11	8 10	rspc2v	$⊢ (A \in R \land B \in S) \to (\forall x \in R \forall y \in S x F y \in C \to A F B \in C)$
12	2 6 11	sylc	$⊢ (φ \land A \in R \land B \in S) \to A F B \in C$

Metamath Proof Explorer