Metamath Proof Explorer

Theorem 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 ⊢ φ → F : R × S ⟶ C
Assertion fovcld ⊢ φ ∧ A ∈ R ∧ B ∈ S → A F B ∈ C

Proof

Step Hyp Ref Expression
1 fovcld.1 ⊢ φ → F : R × S ⟶ C
2 3simpc ⊢ φ ∧ A ∈ R ∧ B ∈ S → A ∈ R ∧ B ∈ S
3 ffnov ⊢ F : R × S ⟶ C ↔ F Fn R × S ∧ ∀ x ∈ R ∀ y ∈ S x F y ∈ C
4 3 simprbi ⊢ F : R × S ⟶ C → ∀ x ∈ R ∀ y ∈ S x F y ∈ C
5 1 4 syl ⊢ φ → ∀ x ∈ R ∀ y ∈ S x F y ∈ C
6 5 3ad2ant1 ⊢ φ ∧ A ∈ R ∧ B ∈ S → ∀ x ∈ R ∀ y ∈ S x F y ∈ C
7 oveq1 ⊢ x = A → x F y = A F y
8 7 eleq1d ⊢ x = A → x F y ∈ C ↔ A F y ∈ C
9 oveq2 ⊢ y = B → A F y = A F B
10 9 eleq1d ⊢ y = B → A F y ∈ C ↔ A F B ∈ C
11 8 10 rspc2v ⊢ A ∈ R ∧ B ∈ S → ∀ x ∈ R ∀ y ∈ S x F y ∈ C → A F B ∈ C
12 2 6 11 sylc ⊢ φ ∧ A ∈ R ∧ B ∈ S → A F B ∈ C