Step | Hyp | Ref
| Expression |
1 | | inss1 4056 |
. . 3
⊢ (𝑆 ∩ 𝑇) ⊆ 𝑆 |
2 | | inss2 4057 |
. . . . . . 7
⊢ (𝑆 ∩ 𝑇) ⊆ 𝑇 |
3 | | simpl 476 |
. . . . . . 7
⊢ ((𝑥 ∈ (𝑆 ∩ 𝑇) ∧ 𝑦 ∈ (𝑆 ∩ 𝑇)) → 𝑥 ∈ (𝑆 ∩ 𝑇)) |
4 | 2, 3 | sseldi 3824 |
. . . . . 6
⊢ ((𝑥 ∈ (𝑆 ∩ 𝑇) ∧ 𝑦 ∈ (𝑆 ∩ 𝑇)) → 𝑥 ∈ 𝑇) |
5 | | simpr 479 |
. . . . . . 7
⊢ ((𝑥 ∈ (𝑆 ∩ 𝑇) ∧ 𝑦 ∈ (𝑆 ∩ 𝑇)) → 𝑦 ∈ (𝑆 ∩ 𝑇)) |
6 | 2, 5 | sseldi 3824 |
. . . . . 6
⊢ ((𝑥 ∈ (𝑆 ∩ 𝑇) ∧ 𝑦 ∈ (𝑆 ∩ 𝑇)) → 𝑦 ∈ 𝑇) |
7 | 4, 6 | ovresd 7060 |
. . . . 5
⊢ ((𝑥 ∈ (𝑆 ∩ 𝑇) ∧ 𝑦 ∈ (𝑆 ∩ 𝑇)) → (𝑥(𝐻 ↾ (𝑇 × 𝑇))𝑦) = (𝑥𝐻𝑦)) |
8 | | eqimss 3881 |
. . . . 5
⊢ ((𝑥(𝐻 ↾ (𝑇 × 𝑇))𝑦) = (𝑥𝐻𝑦) → (𝑥(𝐻 ↾ (𝑇 × 𝑇))𝑦) ⊆ (𝑥𝐻𝑦)) |
9 | 7, 8 | syl 17 |
. . . 4
⊢ ((𝑥 ∈ (𝑆 ∩ 𝑇) ∧ 𝑦 ∈ (𝑆 ∩ 𝑇)) → (𝑥(𝐻 ↾ (𝑇 × 𝑇))𝑦) ⊆ (𝑥𝐻𝑦)) |
10 | 9 | rgen2a 3185 |
. . 3
⊢
∀𝑥 ∈
(𝑆 ∩ 𝑇)∀𝑦 ∈ (𝑆 ∩ 𝑇)(𝑥(𝐻 ↾ (𝑇 × 𝑇))𝑦) ⊆ (𝑥𝐻𝑦) |
11 | 1, 10 | pm3.2i 464 |
. 2
⊢ ((𝑆 ∩ 𝑇) ⊆ 𝑆 ∧ ∀𝑥 ∈ (𝑆 ∩ 𝑇)∀𝑦 ∈ (𝑆 ∩ 𝑇)(𝑥(𝐻 ↾ (𝑇 × 𝑇))𝑦) ⊆ (𝑥𝐻𝑦)) |
12 | | simpl 476 |
. . . . 5
⊢ ((𝐻 Fn (𝑆 × 𝑆) ∧ 𝑆 ∈ 𝑉) → 𝐻 Fn (𝑆 × 𝑆)) |
13 | | inss1 4056 |
. . . . 5
⊢ ((𝑆 × 𝑆) ∩ (𝑇 × 𝑇)) ⊆ (𝑆 × 𝑆) |
14 | | fnssres 6236 |
. . . . 5
⊢ ((𝐻 Fn (𝑆 × 𝑆) ∧ ((𝑆 × 𝑆) ∩ (𝑇 × 𝑇)) ⊆ (𝑆 × 𝑆)) → (𝐻 ↾ ((𝑆 × 𝑆) ∩ (𝑇 × 𝑇))) Fn ((𝑆 × 𝑆) ∩ (𝑇 × 𝑇))) |
15 | 12, 13, 14 | sylancl 582 |
. . . 4
⊢ ((𝐻 Fn (𝑆 × 𝑆) ∧ 𝑆 ∈ 𝑉) → (𝐻 ↾ ((𝑆 × 𝑆) ∩ (𝑇 × 𝑇))) Fn ((𝑆 × 𝑆) ∩ (𝑇 × 𝑇))) |
16 | | resres 5645 |
. . . . . 6
⊢ ((𝐻 ↾ (𝑆 × 𝑆)) ↾ (𝑇 × 𝑇)) = (𝐻 ↾ ((𝑆 × 𝑆) ∩ (𝑇 × 𝑇))) |
17 | | fnresdm 6232 |
. . . . . . . 8
⊢ (𝐻 Fn (𝑆 × 𝑆) → (𝐻 ↾ (𝑆 × 𝑆)) = 𝐻) |
18 | 17 | adantr 474 |
. . . . . . 7
⊢ ((𝐻 Fn (𝑆 × 𝑆) ∧ 𝑆 ∈ 𝑉) → (𝐻 ↾ (𝑆 × 𝑆)) = 𝐻) |
19 | 18 | reseq1d 5627 |
. . . . . 6
⊢ ((𝐻 Fn (𝑆 × 𝑆) ∧ 𝑆 ∈ 𝑉) → ((𝐻 ↾ (𝑆 × 𝑆)) ↾ (𝑇 × 𝑇)) = (𝐻 ↾ (𝑇 × 𝑇))) |
20 | 16, 19 | syl5eqr 2874 |
. . . . 5
⊢ ((𝐻 Fn (𝑆 × 𝑆) ∧ 𝑆 ∈ 𝑉) → (𝐻 ↾ ((𝑆 × 𝑆) ∩ (𝑇 × 𝑇))) = (𝐻 ↾ (𝑇 × 𝑇))) |
21 | | inxp 5486 |
. . . . . 6
⊢ ((𝑆 × 𝑆) ∩ (𝑇 × 𝑇)) = ((𝑆 ∩ 𝑇) × (𝑆 ∩ 𝑇)) |
22 | 21 | a1i 11 |
. . . . 5
⊢ ((𝐻 Fn (𝑆 × 𝑆) ∧ 𝑆 ∈ 𝑉) → ((𝑆 × 𝑆) ∩ (𝑇 × 𝑇)) = ((𝑆 ∩ 𝑇) × (𝑆 ∩ 𝑇))) |
23 | 20, 22 | fneq12d 6215 |
. . . 4
⊢ ((𝐻 Fn (𝑆 × 𝑆) ∧ 𝑆 ∈ 𝑉) → ((𝐻 ↾ ((𝑆 × 𝑆) ∩ (𝑇 × 𝑇))) Fn ((𝑆 × 𝑆) ∩ (𝑇 × 𝑇)) ↔ (𝐻 ↾ (𝑇 × 𝑇)) Fn ((𝑆 ∩ 𝑇) × (𝑆 ∩ 𝑇)))) |
24 | 15, 23 | mpbid 224 |
. . 3
⊢ ((𝐻 Fn (𝑆 × 𝑆) ∧ 𝑆 ∈ 𝑉) → (𝐻 ↾ (𝑇 × 𝑇)) Fn ((𝑆 ∩ 𝑇) × (𝑆 ∩ 𝑇))) |
25 | | simpr 479 |
. . 3
⊢ ((𝐻 Fn (𝑆 × 𝑆) ∧ 𝑆 ∈ 𝑉) → 𝑆 ∈ 𝑉) |
26 | 24, 12, 25 | isssc 16831 |
. 2
⊢ ((𝐻 Fn (𝑆 × 𝑆) ∧ 𝑆 ∈ 𝑉) → ((𝐻 ↾ (𝑇 × 𝑇)) ⊆cat 𝐻 ↔ ((𝑆 ∩ 𝑇) ⊆ 𝑆 ∧ ∀𝑥 ∈ (𝑆 ∩ 𝑇)∀𝑦 ∈ (𝑆 ∩ 𝑇)(𝑥(𝐻 ↾ (𝑇 × 𝑇))𝑦) ⊆ (𝑥𝐻𝑦)))) |
27 | 11, 26 | mpbiri 250 |
1
⊢ ((𝐻 Fn (𝑆 × 𝑆) ∧ 𝑆 ∈ 𝑉) → (𝐻 ↾ (𝑇 × 𝑇)) ⊆cat 𝐻) |