Metamath Proof Explorer

Theorem oprres

Description: The restriction of an operation is an operation. (Contributed by NM, 1-Feb-2008) (Revised by AV, 19-Oct-2021)

Ref Expression
Hypotheses oprres.v ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑌 ) → ( 𝑥 𝐹 𝑦 ) = ( 𝑥 𝐺 𝑦 ) )
oprres.s ⊢ ( 𝜑 → 𝑌 ⊆ 𝑋 )
oprres.f ⊢ ( 𝜑 → 𝐹 : ( 𝑌 × 𝑌 ) ⟶ 𝑅 )
oprres.g ⊢ ( 𝜑 → 𝐺 : ( 𝑋 × 𝑋 ) ⟶ 𝑆 )
Assertion oprres ( 𝜑 → 𝐹 = ( 𝐺 ↾ ( 𝑌 × 𝑌 ) ) )

Proof

Step Hyp Ref Expression
1 oprres.v ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑌 ) → ( 𝑥 𝐹 𝑦 ) = ( 𝑥 𝐺 𝑦 ) )
2 oprres.s ⊢ ( 𝜑 → 𝑌 ⊆ 𝑋 )
3 oprres.f ⊢ ( 𝜑 → 𝐹 : ( 𝑌 × 𝑌 ) ⟶ 𝑅 )
4 oprres.g ⊢ ( 𝜑 → 𝐺 : ( 𝑋 × 𝑋 ) ⟶ 𝑆 )
5 1 3expb ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑌 ) ) → ( 𝑥 𝐹 𝑦 ) = ( 𝑥 𝐺 𝑦 ) )
6 ovres ⊢ ( ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑌 ) → ( 𝑥 ( 𝐺 ↾ ( 𝑌 × 𝑌 ) ) 𝑦 ) = ( 𝑥 𝐺 𝑦 ) )
7 6 adantl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑌 ) ) → ( 𝑥 ( 𝐺 ↾ ( 𝑌 × 𝑌 ) ) 𝑦 ) = ( 𝑥 𝐺 𝑦 ) )
8 5 7 eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑌 ) ) → ( 𝑥 𝐹 𝑦 ) = ( 𝑥 ( 𝐺 ↾ ( 𝑌 × 𝑌 ) ) 𝑦 ) )
9 8 ralrimivva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑌 ∀ 𝑦 ∈ 𝑌 ( 𝑥 𝐹 𝑦 ) = ( 𝑥 ( 𝐺 ↾ ( 𝑌 × 𝑌 ) ) 𝑦 ) )
10 eqid ⊢ ( 𝑌 × 𝑌 ) = ( 𝑌 × 𝑌 )
11 9 10 jctil ⊢ ( 𝜑 → ( ( 𝑌 × 𝑌 ) = ( 𝑌 × 𝑌 ) ∧ ∀ 𝑥 ∈ 𝑌 ∀ 𝑦 ∈ 𝑌 ( 𝑥 𝐹 𝑦 ) = ( 𝑥 ( 𝐺 ↾ ( 𝑌 × 𝑌 ) ) 𝑦 ) ) )
12 3 ffnd ⊢ ( 𝜑 → 𝐹 Fn ( 𝑌 × 𝑌 ) )
13 4 ffnd ⊢ ( 𝜑 → 𝐺 Fn ( 𝑋 × 𝑋 ) )
14 xpss12 ⊢ ( ( 𝑌 ⊆ 𝑋 ∧ 𝑌 ⊆ 𝑋 ) → ( 𝑌 × 𝑌 ) ⊆ ( 𝑋 × 𝑋 ) )
15 2 2 14 syl2anc ⊢ ( 𝜑 → ( 𝑌 × 𝑌 ) ⊆ ( 𝑋 × 𝑋 ) )
16 fnssres ⊢ ( ( 𝐺 Fn ( 𝑋 × 𝑋 ) ∧ ( 𝑌 × 𝑌 ) ⊆ ( 𝑋 × 𝑋 ) ) → ( 𝐺 ↾ ( 𝑌 × 𝑌 ) ) Fn ( 𝑌 × 𝑌 ) )
17 13 15 16 syl2anc ⊢ ( 𝜑 → ( 𝐺 ↾ ( 𝑌 × 𝑌 ) ) Fn ( 𝑌 × 𝑌 ) )
18 eqfnov ⊢ ( ( 𝐹 Fn ( 𝑌 × 𝑌 ) ∧ ( 𝐺 ↾ ( 𝑌 × 𝑌 ) ) Fn ( 𝑌 × 𝑌 ) ) → ( 𝐹 = ( 𝐺 ↾ ( 𝑌 × 𝑌 ) ) ↔ ( ( 𝑌 × 𝑌 ) = ( 𝑌 × 𝑌 ) ∧ ∀ 𝑥 ∈ 𝑌 ∀ 𝑦 ∈ 𝑌 ( 𝑥 𝐹 𝑦 ) = ( 𝑥 ( 𝐺 ↾ ( 𝑌 × 𝑌 ) ) 𝑦 ) ) ) )
19 12 17 18 syl2anc ⊢ ( 𝜑 → ( 𝐹 = ( 𝐺 ↾ ( 𝑌 × 𝑌 ) ) ↔ ( ( 𝑌 × 𝑌 ) = ( 𝑌 × 𝑌 ) ∧ ∀ 𝑥 ∈ 𝑌 ∀ 𝑦 ∈ 𝑌 ( 𝑥 𝐹 𝑦 ) = ( 𝑥 ( 𝐺 ↾ ( 𝑌 × 𝑌 ) ) 𝑦 ) ) ) )
20 11 19 mpbird ⊢ ( 𝜑 → 𝐹 = ( 𝐺 ↾ ( 𝑌 × 𝑌 ) ) )