Proof of Theorem neiin
Step | Hyp | Ref
| Expression |
1 | | simpr 488 |
. . . . . . 7
⊢ ((𝐽 ∈ Top ∧ 𝑀 ∈ ((nei‘𝐽)‘𝐴)) → 𝑀 ∈ ((nei‘𝐽)‘𝐴)) |
2 | | simpl 486 |
. . . . . . . 8
⊢ ((𝐽 ∈ Top ∧ 𝑀 ∈ ((nei‘𝐽)‘𝐴)) → 𝐽 ∈ Top) |
3 | | eqid 2737 |
. . . . . . . . 9
⊢ ∪ 𝐽 =
∪ 𝐽 |
4 | 3 | neiss2 21998 |
. . . . . . . 8
⊢ ((𝐽 ∈ Top ∧ 𝑀 ∈ ((nei‘𝐽)‘𝐴)) → 𝐴 ⊆ ∪ 𝐽) |
5 | 3 | neii1 22003 |
. . . . . . . 8
⊢ ((𝐽 ∈ Top ∧ 𝑀 ∈ ((nei‘𝐽)‘𝐴)) → 𝑀 ⊆ ∪ 𝐽) |
6 | 3 | neiint 22001 |
. . . . . . . 8
⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ ∪ 𝐽
∧ 𝑀 ⊆ ∪ 𝐽)
→ (𝑀 ∈
((nei‘𝐽)‘𝐴) ↔ 𝐴 ⊆ ((int‘𝐽)‘𝑀))) |
7 | 2, 4, 5, 6 | syl3anc 1373 |
. . . . . . 7
⊢ ((𝐽 ∈ Top ∧ 𝑀 ∈ ((nei‘𝐽)‘𝐴)) → (𝑀 ∈ ((nei‘𝐽)‘𝐴) ↔ 𝐴 ⊆ ((int‘𝐽)‘𝑀))) |
8 | 1, 7 | mpbid 235 |
. . . . . 6
⊢ ((𝐽 ∈ Top ∧ 𝑀 ∈ ((nei‘𝐽)‘𝐴)) → 𝐴 ⊆ ((int‘𝐽)‘𝑀)) |
9 | | ssinss1 4152 |
. . . . . 6
⊢ (𝐴 ⊆ ((int‘𝐽)‘𝑀) → (𝐴 ∩ 𝐵) ⊆ ((int‘𝐽)‘𝑀)) |
10 | 8, 9 | syl 17 |
. . . . 5
⊢ ((𝐽 ∈ Top ∧ 𝑀 ∈ ((nei‘𝐽)‘𝐴)) → (𝐴 ∩ 𝐵) ⊆ ((int‘𝐽)‘𝑀)) |
11 | 10 | 3adant3 1134 |
. . . 4
⊢ ((𝐽 ∈ Top ∧ 𝑀 ∈ ((nei‘𝐽)‘𝐴) ∧ 𝑁 ∈ ((nei‘𝐽)‘𝐵)) → (𝐴 ∩ 𝐵) ⊆ ((int‘𝐽)‘𝑀)) |
12 | | inss2 4144 |
. . . . 5
⊢ (𝐴 ∩ 𝐵) ⊆ 𝐵 |
13 | | simpr 488 |
. . . . . . 7
⊢ ((𝐽 ∈ Top ∧ 𝑁 ∈ ((nei‘𝐽)‘𝐵)) → 𝑁 ∈ ((nei‘𝐽)‘𝐵)) |
14 | | simpl 486 |
. . . . . . . 8
⊢ ((𝐽 ∈ Top ∧ 𝑁 ∈ ((nei‘𝐽)‘𝐵)) → 𝐽 ∈ Top) |
15 | 3 | neiss2 21998 |
. . . . . . . 8
⊢ ((𝐽 ∈ Top ∧ 𝑁 ∈ ((nei‘𝐽)‘𝐵)) → 𝐵 ⊆ ∪ 𝐽) |
16 | 3 | neii1 22003 |
. . . . . . . 8
⊢ ((𝐽 ∈ Top ∧ 𝑁 ∈ ((nei‘𝐽)‘𝐵)) → 𝑁 ⊆ ∪ 𝐽) |
17 | 3 | neiint 22001 |
. . . . . . . 8
⊢ ((𝐽 ∈ Top ∧ 𝐵 ⊆ ∪ 𝐽
∧ 𝑁 ⊆ ∪ 𝐽)
→ (𝑁 ∈
((nei‘𝐽)‘𝐵) ↔ 𝐵 ⊆ ((int‘𝐽)‘𝑁))) |
18 | 14, 15, 16, 17 | syl3anc 1373 |
. . . . . . 7
⊢ ((𝐽 ∈ Top ∧ 𝑁 ∈ ((nei‘𝐽)‘𝐵)) → (𝑁 ∈ ((nei‘𝐽)‘𝐵) ↔ 𝐵 ⊆ ((int‘𝐽)‘𝑁))) |
19 | 13, 18 | mpbid 235 |
. . . . . 6
⊢ ((𝐽 ∈ Top ∧ 𝑁 ∈ ((nei‘𝐽)‘𝐵)) → 𝐵 ⊆ ((int‘𝐽)‘𝑁)) |
20 | 19 | 3adant2 1133 |
. . . . 5
⊢ ((𝐽 ∈ Top ∧ 𝑀 ∈ ((nei‘𝐽)‘𝐴) ∧ 𝑁 ∈ ((nei‘𝐽)‘𝐵)) → 𝐵 ⊆ ((int‘𝐽)‘𝑁)) |
21 | 12, 20 | sstrid 3912 |
. . . 4
⊢ ((𝐽 ∈ Top ∧ 𝑀 ∈ ((nei‘𝐽)‘𝐴) ∧ 𝑁 ∈ ((nei‘𝐽)‘𝐵)) → (𝐴 ∩ 𝐵) ⊆ ((int‘𝐽)‘𝑁)) |
22 | 11, 21 | ssind 4147 |
. . 3
⊢ ((𝐽 ∈ Top ∧ 𝑀 ∈ ((nei‘𝐽)‘𝐴) ∧ 𝑁 ∈ ((nei‘𝐽)‘𝐵)) → (𝐴 ∩ 𝐵) ⊆ (((int‘𝐽)‘𝑀) ∩ ((int‘𝐽)‘𝑁))) |
23 | | simp1 1138 |
. . . 4
⊢ ((𝐽 ∈ Top ∧ 𝑀 ∈ ((nei‘𝐽)‘𝐴) ∧ 𝑁 ∈ ((nei‘𝐽)‘𝐵)) → 𝐽 ∈ Top) |
24 | 5 | 3adant3 1134 |
. . . 4
⊢ ((𝐽 ∈ Top ∧ 𝑀 ∈ ((nei‘𝐽)‘𝐴) ∧ 𝑁 ∈ ((nei‘𝐽)‘𝐵)) → 𝑀 ⊆ ∪ 𝐽) |
25 | 16 | 3adant2 1133 |
. . . 4
⊢ ((𝐽 ∈ Top ∧ 𝑀 ∈ ((nei‘𝐽)‘𝐴) ∧ 𝑁 ∈ ((nei‘𝐽)‘𝐵)) → 𝑁 ⊆ ∪ 𝐽) |
26 | 3 | ntrin 21958 |
. . . 4
⊢ ((𝐽 ∈ Top ∧ 𝑀 ⊆ ∪ 𝐽
∧ 𝑁 ⊆ ∪ 𝐽)
→ ((int‘𝐽)‘(𝑀 ∩ 𝑁)) = (((int‘𝐽)‘𝑀) ∩ ((int‘𝐽)‘𝑁))) |
27 | 23, 24, 25, 26 | syl3anc 1373 |
. . 3
⊢ ((𝐽 ∈ Top ∧ 𝑀 ∈ ((nei‘𝐽)‘𝐴) ∧ 𝑁 ∈ ((nei‘𝐽)‘𝐵)) → ((int‘𝐽)‘(𝑀 ∩ 𝑁)) = (((int‘𝐽)‘𝑀) ∩ ((int‘𝐽)‘𝑁))) |
28 | 22, 27 | sseqtrrd 3942 |
. 2
⊢ ((𝐽 ∈ Top ∧ 𝑀 ∈ ((nei‘𝐽)‘𝐴) ∧ 𝑁 ∈ ((nei‘𝐽)‘𝐵)) → (𝐴 ∩ 𝐵) ⊆ ((int‘𝐽)‘(𝑀 ∩ 𝑁))) |
29 | | ssinss1 4152 |
. . . . 5
⊢ (𝐴 ⊆ ∪ 𝐽
→ (𝐴 ∩ 𝐵) ⊆ ∪ 𝐽) |
30 | 4, 29 | syl 17 |
. . . 4
⊢ ((𝐽 ∈ Top ∧ 𝑀 ∈ ((nei‘𝐽)‘𝐴)) → (𝐴 ∩ 𝐵) ⊆ ∪ 𝐽) |
31 | | ssinss1 4152 |
. . . . 5
⊢ (𝑀 ⊆ ∪ 𝐽
→ (𝑀 ∩ 𝑁) ⊆ ∪ 𝐽) |
32 | 5, 31 | syl 17 |
. . . 4
⊢ ((𝐽 ∈ Top ∧ 𝑀 ∈ ((nei‘𝐽)‘𝐴)) → (𝑀 ∩ 𝑁) ⊆ ∪ 𝐽) |
33 | 3 | neiint 22001 |
. . . 4
⊢ ((𝐽 ∈ Top ∧ (𝐴 ∩ 𝐵) ⊆ ∪ 𝐽 ∧ (𝑀 ∩ 𝑁) ⊆ ∪ 𝐽) → ((𝑀 ∩ 𝑁) ∈ ((nei‘𝐽)‘(𝐴 ∩ 𝐵)) ↔ (𝐴 ∩ 𝐵) ⊆ ((int‘𝐽)‘(𝑀 ∩ 𝑁)))) |
34 | 2, 30, 32, 33 | syl3anc 1373 |
. . 3
⊢ ((𝐽 ∈ Top ∧ 𝑀 ∈ ((nei‘𝐽)‘𝐴)) → ((𝑀 ∩ 𝑁) ∈ ((nei‘𝐽)‘(𝐴 ∩ 𝐵)) ↔ (𝐴 ∩ 𝐵) ⊆ ((int‘𝐽)‘(𝑀 ∩ 𝑁)))) |
35 | 34 | 3adant3 1134 |
. 2
⊢ ((𝐽 ∈ Top ∧ 𝑀 ∈ ((nei‘𝐽)‘𝐴) ∧ 𝑁 ∈ ((nei‘𝐽)‘𝐵)) → ((𝑀 ∩ 𝑁) ∈ ((nei‘𝐽)‘(𝐴 ∩ 𝐵)) ↔ (𝐴 ∩ 𝐵) ⊆ ((int‘𝐽)‘(𝑀 ∩ 𝑁)))) |
36 | 28, 35 | mpbird 260 |
1
⊢ ((𝐽 ∈ Top ∧ 𝑀 ∈ ((nei‘𝐽)‘𝐴) ∧ 𝑁 ∈ ((nei‘𝐽)‘𝐵)) → (𝑀 ∩ 𝑁) ∈ ((nei‘𝐽)‘(𝐴 ∩ 𝐵))) |