Metamath Proof Explorer

Theorem sscres

Description: Any function restricted to a square domain is a subcategory subset of the original. (Contributed by Mario Carneiro, 6-Jan-2017)

Ref Expression
Assertion sscres ( ( 𝐻 Fn ( 𝑆 × 𝑆 ) ∧ 𝑆 ∈ 𝑉 ) → ( 𝐻 ↾ ( 𝑇 × 𝑇 ) ) ⊆cat 𝐻 )

Proof

Step Hyp Ref Expression
1 inss1 ⊢ ( 𝑆 ∩ 𝑇 ) ⊆ 𝑆
2 simpl ⊢ ( ( 𝑥 ∈ ( 𝑆 ∩ 𝑇 ) ∧ 𝑦 ∈ ( 𝑆 ∩ 𝑇 ) ) → 𝑥 ∈ ( 𝑆 ∩ 𝑇 ) )
3 2 elin2d ⊢ ( ( 𝑥 ∈ ( 𝑆 ∩ 𝑇 ) ∧ 𝑦 ∈ ( 𝑆 ∩ 𝑇 ) ) → 𝑥 ∈ 𝑇 )
4 simpr ⊢ ( ( 𝑥 ∈ ( 𝑆 ∩ 𝑇 ) ∧ 𝑦 ∈ ( 𝑆 ∩ 𝑇 ) ) → 𝑦 ∈ ( 𝑆 ∩ 𝑇 ) )
5 4 elin2d ⊢ ( ( 𝑥 ∈ ( 𝑆 ∩ 𝑇 ) ∧ 𝑦 ∈ ( 𝑆 ∩ 𝑇 ) ) → 𝑦 ∈ 𝑇 )
6 3 5 ovresd ⊢ ( ( 𝑥 ∈ ( 𝑆 ∩ 𝑇 ) ∧ 𝑦 ∈ ( 𝑆 ∩ 𝑇 ) ) → ( 𝑥 ( 𝐻 ↾ ( 𝑇 × 𝑇 ) ) 𝑦 ) = ( 𝑥 𝐻 𝑦 ) )
7 eqimss ⊢ ( ( 𝑥 ( 𝐻 ↾ ( 𝑇 × 𝑇 ) ) 𝑦 ) = ( 𝑥 𝐻 𝑦 ) → ( 𝑥 ( 𝐻 ↾ ( 𝑇 × 𝑇 ) ) 𝑦 ) ⊆ ( 𝑥 𝐻 𝑦 ) )
8 6 7 syl ⊢ ( ( 𝑥 ∈ ( 𝑆 ∩ 𝑇 ) ∧ 𝑦 ∈ ( 𝑆 ∩ 𝑇 ) ) → ( 𝑥 ( 𝐻 ↾ ( 𝑇 × 𝑇 ) ) 𝑦 ) ⊆ ( 𝑥 𝐻 𝑦 ) )
9 8 rgen2 ⊢ ∀ 𝑥 ∈ ( 𝑆 ∩ 𝑇 ) ∀ 𝑦 ∈ ( 𝑆 ∩ 𝑇 ) ( 𝑥 ( 𝐻 ↾ ( 𝑇 × 𝑇 ) ) 𝑦 ) ⊆ ( 𝑥 𝐻 𝑦 )
10 1 9 pm3.2i ⊢ ( ( 𝑆 ∩ 𝑇 ) ⊆ 𝑆 ∧ ∀ 𝑥 ∈ ( 𝑆 ∩ 𝑇 ) ∀ 𝑦 ∈ ( 𝑆 ∩ 𝑇 ) ( 𝑥 ( 𝐻 ↾ ( 𝑇 × 𝑇 ) ) 𝑦 ) ⊆ ( 𝑥 𝐻 𝑦 ) )
11 simpl ⊢ ( ( 𝐻 Fn ( 𝑆 × 𝑆 ) ∧ 𝑆 ∈ 𝑉 ) → 𝐻 Fn ( 𝑆 × 𝑆 ) )
12 inss1 ⊢ ( ( 𝑆 × 𝑆 ) ∩ ( 𝑇 × 𝑇 ) ) ⊆ ( 𝑆 × 𝑆 )
13 fnssres ⊢ ( ( 𝐻 Fn ( 𝑆 × 𝑆 ) ∧ ( ( 𝑆 × 𝑆 ) ∩ ( 𝑇 × 𝑇 ) ) ⊆ ( 𝑆 × 𝑆 ) ) → ( 𝐻 ↾ ( ( 𝑆 × 𝑆 ) ∩ ( 𝑇 × 𝑇 ) ) ) Fn ( ( 𝑆 × 𝑆 ) ∩ ( 𝑇 × 𝑇 ) ) )
14 11 12 13 sylancl ⊢ ( ( 𝐻 Fn ( 𝑆 × 𝑆 ) ∧ 𝑆 ∈ 𝑉 ) → ( 𝐻 ↾ ( ( 𝑆 × 𝑆 ) ∩ ( 𝑇 × 𝑇 ) ) ) Fn ( ( 𝑆 × 𝑆 ) ∩ ( 𝑇 × 𝑇 ) ) )
15 resres ⊢ ( ( 𝐻 ↾ ( 𝑆 × 𝑆 ) ) ↾ ( 𝑇 × 𝑇 ) ) = ( 𝐻 ↾ ( ( 𝑆 × 𝑆 ) ∩ ( 𝑇 × 𝑇 ) ) )
16 fnresdm ⊢ ( 𝐻 Fn ( 𝑆 × 𝑆 ) → ( 𝐻 ↾ ( 𝑆 × 𝑆 ) ) = 𝐻 )
17 16 adantr ⊢ ( ( 𝐻 Fn ( 𝑆 × 𝑆 ) ∧ 𝑆 ∈ 𝑉 ) → ( 𝐻 ↾ ( 𝑆 × 𝑆 ) ) = 𝐻 )
18 17 reseq1d ⊢ ( ( 𝐻 Fn ( 𝑆 × 𝑆 ) ∧ 𝑆 ∈ 𝑉 ) → ( ( 𝐻 ↾ ( 𝑆 × 𝑆 ) ) ↾ ( 𝑇 × 𝑇 ) ) = ( 𝐻 ↾ ( 𝑇 × 𝑇 ) ) )
19 15 18 eqtr3id ⊢ ( ( 𝐻 Fn ( 𝑆 × 𝑆 ) ∧ 𝑆 ∈ 𝑉 ) → ( 𝐻 ↾ ( ( 𝑆 × 𝑆 ) ∩ ( 𝑇 × 𝑇 ) ) ) = ( 𝐻 ↾ ( 𝑇 × 𝑇 ) ) )
20 inxp ⊢ ( ( 𝑆 × 𝑆 ) ∩ ( 𝑇 × 𝑇 ) ) = ( ( 𝑆 ∩ 𝑇 ) × ( 𝑆 ∩ 𝑇 ) )
21 20 a1i ⊢ ( ( 𝐻 Fn ( 𝑆 × 𝑆 ) ∧ 𝑆 ∈ 𝑉 ) → ( ( 𝑆 × 𝑆 ) ∩ ( 𝑇 × 𝑇 ) ) = ( ( 𝑆 ∩ 𝑇 ) × ( 𝑆 ∩ 𝑇 ) ) )
22 19 21 fneq12d ⊢ ( ( 𝐻 Fn ( 𝑆 × 𝑆 ) ∧ 𝑆 ∈ 𝑉 ) → ( ( 𝐻 ↾ ( ( 𝑆 × 𝑆 ) ∩ ( 𝑇 × 𝑇 ) ) ) Fn ( ( 𝑆 × 𝑆 ) ∩ ( 𝑇 × 𝑇 ) ) ↔ ( 𝐻 ↾ ( 𝑇 × 𝑇 ) ) Fn ( ( 𝑆 ∩ 𝑇 ) × ( 𝑆 ∩ 𝑇 ) ) ) )
23 14 22 mpbid ⊢ ( ( 𝐻 Fn ( 𝑆 × 𝑆 ) ∧ 𝑆 ∈ 𝑉 ) → ( 𝐻 ↾ ( 𝑇 × 𝑇 ) ) Fn ( ( 𝑆 ∩ 𝑇 ) × ( 𝑆 ∩ 𝑇 ) ) )
24 simpr ⊢ ( ( 𝐻 Fn ( 𝑆 × 𝑆 ) ∧ 𝑆 ∈ 𝑉 ) → 𝑆 ∈ 𝑉 )
25 23 11 24 isssc ⊢ ( ( 𝐻 Fn ( 𝑆 × 𝑆 ) ∧ 𝑆 ∈ 𝑉 ) → ( ( 𝐻 ↾ ( 𝑇 × 𝑇 ) ) ⊆cat 𝐻 ↔ ( ( 𝑆 ∩ 𝑇 ) ⊆ 𝑆 ∧ ∀ 𝑥 ∈ ( 𝑆 ∩ 𝑇 ) ∀ 𝑦 ∈ ( 𝑆 ∩ 𝑇 ) ( 𝑥 ( 𝐻 ↾ ( 𝑇 × 𝑇 ) ) 𝑦 ) ⊆ ( 𝑥 𝐻 𝑦 ) ) ) )
26 10 25 mpbiri ⊢ ( ( 𝐻 Fn ( 𝑆 × 𝑆 ) ∧ 𝑆 ∈ 𝑉 ) → ( 𝐻 ↾ ( 𝑇 × 𝑇 ) ) ⊆cat 𝐻 )