Step | Hyp | Ref
| Expression |
1 | | restcls.2 |
. . . . . . 7
⊢ 𝐾 = (𝐽 ↾t 𝑌) |
2 | 1 | fveq2i 6106 |
. . . . . 6
⊢
(int‘𝐾) =
(int‘(𝐽
↾t 𝑌)) |
3 | 2 | fveq1i 6104 |
. . . . 5
⊢
((int‘𝐾)‘𝑆) = ((int‘(𝐽 ↾t 𝑌))‘𝑆) |
4 | | restcls.1 |
. . . . . . . . . 10
⊢ 𝑋 = ∪
𝐽 |
5 | 4 | topopn 20536 |
. . . . . . . . 9
⊢ (𝐽 ∈ Top → 𝑋 ∈ 𝐽) |
6 | | ssexg 4732 |
. . . . . . . . . 10
⊢ ((𝑌 ⊆ 𝑋 ∧ 𝑋 ∈ 𝐽) → 𝑌 ∈ V) |
7 | 6 | ancoms 468 |
. . . . . . . . 9
⊢ ((𝑋 ∈ 𝐽 ∧ 𝑌 ⊆ 𝑋) → 𝑌 ∈ V) |
8 | 5, 7 | sylan 487 |
. . . . . . . 8
⊢ ((𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋) → 𝑌 ∈ V) |
9 | | resttop 20774 |
. . . . . . . 8
⊢ ((𝐽 ∈ Top ∧ 𝑌 ∈ V) → (𝐽 ↾t 𝑌) ∈ Top) |
10 | 8, 9 | syldan 486 |
. . . . . . 7
⊢ ((𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋) → (𝐽 ↾t 𝑌) ∈ Top) |
11 | 10 | 3adant3 1074 |
. . . . . 6
⊢ ((𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌) → (𝐽 ↾t 𝑌) ∈ Top) |
12 | 4 | restuni 20776 |
. . . . . . . 8
⊢ ((𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋) → 𝑌 = ∪ (𝐽 ↾t 𝑌)) |
13 | 12 | sseq2d 3596 |
. . . . . . 7
⊢ ((𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋) → (𝑆 ⊆ 𝑌 ↔ 𝑆 ⊆ ∪ (𝐽 ↾t 𝑌))) |
14 | 13 | biimp3a 1424 |
. . . . . 6
⊢ ((𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌) → 𝑆 ⊆ ∪ (𝐽 ↾t 𝑌)) |
15 | | eqid 2610 |
. . . . . . 7
⊢ ∪ (𝐽
↾t 𝑌) =
∪ (𝐽 ↾t 𝑌) |
16 | 15 | ntropn 20663 |
. . . . . 6
⊢ (((𝐽 ↾t 𝑌) ∈ Top ∧ 𝑆 ⊆ ∪ (𝐽
↾t 𝑌))
→ ((int‘(𝐽
↾t 𝑌))‘𝑆) ∈ (𝐽 ↾t 𝑌)) |
17 | 11, 14, 16 | syl2anc 691 |
. . . . 5
⊢ ((𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌) → ((int‘(𝐽 ↾t 𝑌))‘𝑆) ∈ (𝐽 ↾t 𝑌)) |
18 | 3, 17 | syl5eqel 2692 |
. . . 4
⊢ ((𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌) → ((int‘𝐾)‘𝑆) ∈ (𝐽 ↾t 𝑌)) |
19 | | simp1 1054 |
. . . . 5
⊢ ((𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌) → 𝐽 ∈ Top) |
20 | | uniexg 6853 |
. . . . . . . . 9
⊢ (𝐽 ∈ Top → ∪ 𝐽
∈ V) |
21 | 4, 20 | syl5eqel 2692 |
. . . . . . . 8
⊢ (𝐽 ∈ Top → 𝑋 ∈ V) |
22 | | ssexg 4732 |
. . . . . . . 8
⊢ ((𝑌 ⊆ 𝑋 ∧ 𝑋 ∈ V) → 𝑌 ∈ V) |
23 | 21, 22 | sylan2 490 |
. . . . . . 7
⊢ ((𝑌 ⊆ 𝑋 ∧ 𝐽 ∈ Top) → 𝑌 ∈ V) |
24 | 23 | ancoms 468 |
. . . . . 6
⊢ ((𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋) → 𝑌 ∈ V) |
25 | 24 | 3adant3 1074 |
. . . . 5
⊢ ((𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌) → 𝑌 ∈ V) |
26 | | elrest 15911 |
. . . . 5
⊢ ((𝐽 ∈ Top ∧ 𝑌 ∈ V) →
(((int‘𝐾)‘𝑆) ∈ (𝐽 ↾t 𝑌) ↔ ∃𝑜 ∈ 𝐽 ((int‘𝐾)‘𝑆) = (𝑜 ∩ 𝑌))) |
27 | 19, 25, 26 | syl2anc 691 |
. . . 4
⊢ ((𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌) → (((int‘𝐾)‘𝑆) ∈ (𝐽 ↾t 𝑌) ↔ ∃𝑜 ∈ 𝐽 ((int‘𝐾)‘𝑆) = (𝑜 ∩ 𝑌))) |
28 | 18, 27 | mpbid 221 |
. . 3
⊢ ((𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌) → ∃𝑜 ∈ 𝐽 ((int‘𝐾)‘𝑆) = (𝑜 ∩ 𝑌)) |
29 | 4 | eltopss 20537 |
. . . . . . . . . . 11
⊢ ((𝐽 ∈ Top ∧ 𝑜 ∈ 𝐽) → 𝑜 ⊆ 𝑋) |
30 | 29 | sseld 3567 |
. . . . . . . . . 10
⊢ ((𝐽 ∈ Top ∧ 𝑜 ∈ 𝐽) → (𝑥 ∈ 𝑜 → 𝑥 ∈ 𝑋)) |
31 | 30 | adantrr 749 |
. . . . . . . . 9
⊢ ((𝐽 ∈ Top ∧ (𝑜 ∈ 𝐽 ∧ ((int‘𝐾)‘𝑆) = (𝑜 ∩ 𝑌))) → (𝑥 ∈ 𝑜 → 𝑥 ∈ 𝑋)) |
32 | 31 | 3ad2antl1 1216 |
. . . . . . . 8
⊢ (((𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌) ∧ (𝑜 ∈ 𝐽 ∧ ((int‘𝐾)‘𝑆) = (𝑜 ∩ 𝑌))) → (𝑥 ∈ 𝑜 → 𝑥 ∈ 𝑋)) |
33 | | eldif 3550 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (𝑋 ∖ 𝑌) ↔ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ 𝑌)) |
34 | 33 | simplbi2 653 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝑋 → (¬ 𝑥 ∈ 𝑌 → 𝑥 ∈ (𝑋 ∖ 𝑌))) |
35 | 34 | orrd 392 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝑋 → (𝑥 ∈ 𝑌 ∨ 𝑥 ∈ (𝑋 ∖ 𝑌))) |
36 | 32, 35 | syl6 34 |
. . . . . . 7
⊢ (((𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌) ∧ (𝑜 ∈ 𝐽 ∧ ((int‘𝐾)‘𝑆) = (𝑜 ∩ 𝑌))) → (𝑥 ∈ 𝑜 → (𝑥 ∈ 𝑌 ∨ 𝑥 ∈ (𝑋 ∖ 𝑌)))) |
37 | | elin 3758 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (𝑜 ∩ 𝑌) ↔ (𝑥 ∈ 𝑜 ∧ 𝑥 ∈ 𝑌)) |
38 | | eleq2 2677 |
. . . . . . . . . . . . 13
⊢
(((int‘𝐾)‘𝑆) = (𝑜 ∩ 𝑌) → (𝑥 ∈ ((int‘𝐾)‘𝑆) ↔ 𝑥 ∈ (𝑜 ∩ 𝑌))) |
39 | | elun1 3742 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ((int‘𝐾)‘𝑆) → 𝑥 ∈ (((int‘𝐾)‘𝑆) ∪ (𝑋 ∖ 𝑌))) |
40 | 38, 39 | syl6bir 243 |
. . . . . . . . . . . 12
⊢
(((int‘𝐾)‘𝑆) = (𝑜 ∩ 𝑌) → (𝑥 ∈ (𝑜 ∩ 𝑌) → 𝑥 ∈ (((int‘𝐾)‘𝑆) ∪ (𝑋 ∖ 𝑌)))) |
41 | 40 | ad2antll 761 |
. . . . . . . . . . 11
⊢ (((𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌) ∧ (𝑜 ∈ 𝐽 ∧ ((int‘𝐾)‘𝑆) = (𝑜 ∩ 𝑌))) → (𝑥 ∈ (𝑜 ∩ 𝑌) → 𝑥 ∈ (((int‘𝐾)‘𝑆) ∪ (𝑋 ∖ 𝑌)))) |
42 | 37, 41 | syl5bir 232 |
. . . . . . . . . 10
⊢ (((𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌) ∧ (𝑜 ∈ 𝐽 ∧ ((int‘𝐾)‘𝑆) = (𝑜 ∩ 𝑌))) → ((𝑥 ∈ 𝑜 ∧ 𝑥 ∈ 𝑌) → 𝑥 ∈ (((int‘𝐾)‘𝑆) ∪ (𝑋 ∖ 𝑌)))) |
43 | 42 | expdimp 452 |
. . . . . . . . 9
⊢ ((((𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌) ∧ (𝑜 ∈ 𝐽 ∧ ((int‘𝐾)‘𝑆) = (𝑜 ∩ 𝑌))) ∧ 𝑥 ∈ 𝑜) → (𝑥 ∈ 𝑌 → 𝑥 ∈ (((int‘𝐾)‘𝑆) ∪ (𝑋 ∖ 𝑌)))) |
44 | | elun2 3743 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (𝑋 ∖ 𝑌) → 𝑥 ∈ (((int‘𝐾)‘𝑆) ∪ (𝑋 ∖ 𝑌))) |
45 | 44 | a1i 11 |
. . . . . . . . 9
⊢ ((((𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌) ∧ (𝑜 ∈ 𝐽 ∧ ((int‘𝐾)‘𝑆) = (𝑜 ∩ 𝑌))) ∧ 𝑥 ∈ 𝑜) → (𝑥 ∈ (𝑋 ∖ 𝑌) → 𝑥 ∈ (((int‘𝐾)‘𝑆) ∪ (𝑋 ∖ 𝑌)))) |
46 | 43, 45 | jaod 394 |
. . . . . . . 8
⊢ ((((𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌) ∧ (𝑜 ∈ 𝐽 ∧ ((int‘𝐾)‘𝑆) = (𝑜 ∩ 𝑌))) ∧ 𝑥 ∈ 𝑜) → ((𝑥 ∈ 𝑌 ∨ 𝑥 ∈ (𝑋 ∖ 𝑌)) → 𝑥 ∈ (((int‘𝐾)‘𝑆) ∪ (𝑋 ∖ 𝑌)))) |
47 | 46 | ex 449 |
. . . . . . 7
⊢ (((𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌) ∧ (𝑜 ∈ 𝐽 ∧ ((int‘𝐾)‘𝑆) = (𝑜 ∩ 𝑌))) → (𝑥 ∈ 𝑜 → ((𝑥 ∈ 𝑌 ∨ 𝑥 ∈ (𝑋 ∖ 𝑌)) → 𝑥 ∈ (((int‘𝐾)‘𝑆) ∪ (𝑋 ∖ 𝑌))))) |
48 | 36, 47 | mpdd 42 |
. . . . . 6
⊢ (((𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌) ∧ (𝑜 ∈ 𝐽 ∧ ((int‘𝐾)‘𝑆) = (𝑜 ∩ 𝑌))) → (𝑥 ∈ 𝑜 → 𝑥 ∈ (((int‘𝐾)‘𝑆) ∪ (𝑋 ∖ 𝑌)))) |
49 | 48 | ssrdv 3574 |
. . . . 5
⊢ (((𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌) ∧ (𝑜 ∈ 𝐽 ∧ ((int‘𝐾)‘𝑆) = (𝑜 ∩ 𝑌))) → 𝑜 ⊆ (((int‘𝐾)‘𝑆) ∪ (𝑋 ∖ 𝑌))) |
50 | 11 | adantr 480 |
. . . . . . . 8
⊢ (((𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌) ∧ (𝑜 ∈ 𝐽 ∧ ((int‘𝐾)‘𝑆) = (𝑜 ∩ 𝑌))) → (𝐽 ↾t 𝑌) ∈ Top) |
51 | 1, 50 | syl5eqel 2692 |
. . . . . . 7
⊢ (((𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌) ∧ (𝑜 ∈ 𝐽 ∧ ((int‘𝐾)‘𝑆) = (𝑜 ∩ 𝑌))) → 𝐾 ∈ Top) |
52 | 14 | adantr 480 |
. . . . . . 7
⊢ (((𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌) ∧ (𝑜 ∈ 𝐽 ∧ ((int‘𝐾)‘𝑆) = (𝑜 ∩ 𝑌))) → 𝑆 ⊆ ∪ (𝐽 ↾t 𝑌)) |
53 | 1 | unieqi 4381 |
. . . . . . . . 9
⊢ ∪ 𝐾 =
∪ (𝐽 ↾t 𝑌) |
54 | 53 | eqcomi 2619 |
. . . . . . . 8
⊢ ∪ (𝐽
↾t 𝑌) =
∪ 𝐾 |
55 | 54 | ntrss2 20671 |
. . . . . . 7
⊢ ((𝐾 ∈ Top ∧ 𝑆 ⊆ ∪ (𝐽
↾t 𝑌))
→ ((int‘𝐾)‘𝑆) ⊆ 𝑆) |
56 | 51, 52, 55 | syl2anc 691 |
. . . . . 6
⊢ (((𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌) ∧ (𝑜 ∈ 𝐽 ∧ ((int‘𝐾)‘𝑆) = (𝑜 ∩ 𝑌))) → ((int‘𝐾)‘𝑆) ⊆ 𝑆) |
57 | | unss1 3744 |
. . . . . 6
⊢
(((int‘𝐾)‘𝑆) ⊆ 𝑆 → (((int‘𝐾)‘𝑆) ∪ (𝑋 ∖ 𝑌)) ⊆ (𝑆 ∪ (𝑋 ∖ 𝑌))) |
58 | 56, 57 | syl 17 |
. . . . 5
⊢ (((𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌) ∧ (𝑜 ∈ 𝐽 ∧ ((int‘𝐾)‘𝑆) = (𝑜 ∩ 𝑌))) → (((int‘𝐾)‘𝑆) ∪ (𝑋 ∖ 𝑌)) ⊆ (𝑆 ∪ (𝑋 ∖ 𝑌))) |
59 | 49, 58 | sstrd 3578 |
. . . 4
⊢ (((𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌) ∧ (𝑜 ∈ 𝐽 ∧ ((int‘𝐾)‘𝑆) = (𝑜 ∩ 𝑌))) → 𝑜 ⊆ (𝑆 ∪ (𝑋 ∖ 𝑌))) |
60 | | simpl1 1057 |
. . . . . . . . . 10
⊢ (((𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌) ∧ (𝑜 ∈ 𝐽 ∧ 𝑜 ⊆ (𝑆 ∪ (𝑋 ∖ 𝑌)))) → 𝐽 ∈ Top) |
61 | | sstr 3576 |
. . . . . . . . . . . . . . 15
⊢ ((𝑆 ⊆ 𝑌 ∧ 𝑌 ⊆ 𝑋) → 𝑆 ⊆ 𝑋) |
62 | 61 | ancoms 468 |
. . . . . . . . . . . . . 14
⊢ ((𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌) → 𝑆 ⊆ 𝑋) |
63 | 62 | 3adant1 1072 |
. . . . . . . . . . . . 13
⊢ ((𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌) → 𝑆 ⊆ 𝑋) |
64 | 63 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌) ∧ (𝑜 ∈ 𝐽 ∧ 𝑜 ⊆ (𝑆 ∪ (𝑋 ∖ 𝑌)))) → 𝑆 ⊆ 𝑋) |
65 | | difss 3699 |
. . . . . . . . . . . 12
⊢ (𝑋 ∖ 𝑌) ⊆ 𝑋 |
66 | 64, 65 | jctir 559 |
. . . . . . . . . . 11
⊢ (((𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌) ∧ (𝑜 ∈ 𝐽 ∧ 𝑜 ⊆ (𝑆 ∪ (𝑋 ∖ 𝑌)))) → (𝑆 ⊆ 𝑋 ∧ (𝑋 ∖ 𝑌) ⊆ 𝑋)) |
67 | | unss 3749 |
. . . . . . . . . . 11
⊢ ((𝑆 ⊆ 𝑋 ∧ (𝑋 ∖ 𝑌) ⊆ 𝑋) ↔ (𝑆 ∪ (𝑋 ∖ 𝑌)) ⊆ 𝑋) |
68 | 66, 67 | sylib 207 |
. . . . . . . . . 10
⊢ (((𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌) ∧ (𝑜 ∈ 𝐽 ∧ 𝑜 ⊆ (𝑆 ∪ (𝑋 ∖ 𝑌)))) → (𝑆 ∪ (𝑋 ∖ 𝑌)) ⊆ 𝑋) |
69 | | simprl 790 |
. . . . . . . . . 10
⊢ (((𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌) ∧ (𝑜 ∈ 𝐽 ∧ 𝑜 ⊆ (𝑆 ∪ (𝑋 ∖ 𝑌)))) → 𝑜 ∈ 𝐽) |
70 | | simprr 792 |
. . . . . . . . . 10
⊢ (((𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌) ∧ (𝑜 ∈ 𝐽 ∧ 𝑜 ⊆ (𝑆 ∪ (𝑋 ∖ 𝑌)))) → 𝑜 ⊆ (𝑆 ∪ (𝑋 ∖ 𝑌))) |
71 | 4 | ssntr 20672 |
. . . . . . . . . 10
⊢ (((𝐽 ∈ Top ∧ (𝑆 ∪ (𝑋 ∖ 𝑌)) ⊆ 𝑋) ∧ (𝑜 ∈ 𝐽 ∧ 𝑜 ⊆ (𝑆 ∪ (𝑋 ∖ 𝑌)))) → 𝑜 ⊆ ((int‘𝐽)‘(𝑆 ∪ (𝑋 ∖ 𝑌)))) |
72 | 60, 68, 69, 70, 71 | syl22anc 1319 |
. . . . . . . . 9
⊢ (((𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌) ∧ (𝑜 ∈ 𝐽 ∧ 𝑜 ⊆ (𝑆 ∪ (𝑋 ∖ 𝑌)))) → 𝑜 ⊆ ((int‘𝐽)‘(𝑆 ∪ (𝑋 ∖ 𝑌)))) |
73 | | ssrin 3800 |
. . . . . . . . 9
⊢ (𝑜 ⊆ ((int‘𝐽)‘(𝑆 ∪ (𝑋 ∖ 𝑌))) → (𝑜 ∩ 𝑌) ⊆ (((int‘𝐽)‘(𝑆 ∪ (𝑋 ∖ 𝑌))) ∩ 𝑌)) |
74 | 72, 73 | syl 17 |
. . . . . . . 8
⊢ (((𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌) ∧ (𝑜 ∈ 𝐽 ∧ 𝑜 ⊆ (𝑆 ∪ (𝑋 ∖ 𝑌)))) → (𝑜 ∩ 𝑌) ⊆ (((int‘𝐽)‘(𝑆 ∪ (𝑋 ∖ 𝑌))) ∩ 𝑌)) |
75 | | sseq1 3589 |
. . . . . . . 8
⊢
(((int‘𝐾)‘𝑆) = (𝑜 ∩ 𝑌) → (((int‘𝐾)‘𝑆) ⊆ (((int‘𝐽)‘(𝑆 ∪ (𝑋 ∖ 𝑌))) ∩ 𝑌) ↔ (𝑜 ∩ 𝑌) ⊆ (((int‘𝐽)‘(𝑆 ∪ (𝑋 ∖ 𝑌))) ∩ 𝑌))) |
76 | 74, 75 | syl5ibrcom 236 |
. . . . . . 7
⊢ (((𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌) ∧ (𝑜 ∈ 𝐽 ∧ 𝑜 ⊆ (𝑆 ∪ (𝑋 ∖ 𝑌)))) → (((int‘𝐾)‘𝑆) = (𝑜 ∩ 𝑌) → ((int‘𝐾)‘𝑆) ⊆ (((int‘𝐽)‘(𝑆 ∪ (𝑋 ∖ 𝑌))) ∩ 𝑌))) |
77 | 76 | expr 641 |
. . . . . 6
⊢ (((𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌) ∧ 𝑜 ∈ 𝐽) → (𝑜 ⊆ (𝑆 ∪ (𝑋 ∖ 𝑌)) → (((int‘𝐾)‘𝑆) = (𝑜 ∩ 𝑌) → ((int‘𝐾)‘𝑆) ⊆ (((int‘𝐽)‘(𝑆 ∪ (𝑋 ∖ 𝑌))) ∩ 𝑌)))) |
78 | 77 | com23 84 |
. . . . 5
⊢ (((𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌) ∧ 𝑜 ∈ 𝐽) → (((int‘𝐾)‘𝑆) = (𝑜 ∩ 𝑌) → (𝑜 ⊆ (𝑆 ∪ (𝑋 ∖ 𝑌)) → ((int‘𝐾)‘𝑆) ⊆ (((int‘𝐽)‘(𝑆 ∪ (𝑋 ∖ 𝑌))) ∩ 𝑌)))) |
79 | 78 | impr 647 |
. . . 4
⊢ (((𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌) ∧ (𝑜 ∈ 𝐽 ∧ ((int‘𝐾)‘𝑆) = (𝑜 ∩ 𝑌))) → (𝑜 ⊆ (𝑆 ∪ (𝑋 ∖ 𝑌)) → ((int‘𝐾)‘𝑆) ⊆ (((int‘𝐽)‘(𝑆 ∪ (𝑋 ∖ 𝑌))) ∩ 𝑌))) |
80 | 59, 79 | mpd 15 |
. . 3
⊢ (((𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌) ∧ (𝑜 ∈ 𝐽 ∧ ((int‘𝐾)‘𝑆) = (𝑜 ∩ 𝑌))) → ((int‘𝐾)‘𝑆) ⊆ (((int‘𝐽)‘(𝑆 ∪ (𝑋 ∖ 𝑌))) ∩ 𝑌)) |
81 | 28, 80 | rexlimddv 3017 |
. 2
⊢ ((𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌) → ((int‘𝐾)‘𝑆) ⊆ (((int‘𝐽)‘(𝑆 ∪ (𝑋 ∖ 𝑌))) ∩ 𝑌)) |
82 | 1, 11 | syl5eqel 2692 |
. . 3
⊢ ((𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌) → 𝐾 ∈ Top) |
83 | 8 | 3adant3 1074 |
. . . . 5
⊢ ((𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌) → 𝑌 ∈ V) |
84 | 63, 65 | jctir 559 |
. . . . . . 7
⊢ ((𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌) → (𝑆 ⊆ 𝑋 ∧ (𝑋 ∖ 𝑌) ⊆ 𝑋)) |
85 | 84, 67 | sylib 207 |
. . . . . 6
⊢ ((𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌) → (𝑆 ∪ (𝑋 ∖ 𝑌)) ⊆ 𝑋) |
86 | 4 | ntropn 20663 |
. . . . . 6
⊢ ((𝐽 ∈ Top ∧ (𝑆 ∪ (𝑋 ∖ 𝑌)) ⊆ 𝑋) → ((int‘𝐽)‘(𝑆 ∪ (𝑋 ∖ 𝑌))) ∈ 𝐽) |
87 | 19, 85, 86 | syl2anc 691 |
. . . . 5
⊢ ((𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌) → ((int‘𝐽)‘(𝑆 ∪ (𝑋 ∖ 𝑌))) ∈ 𝐽) |
88 | | elrestr 15912 |
. . . . 5
⊢ ((𝐽 ∈ Top ∧ 𝑌 ∈ V ∧
((int‘𝐽)‘(𝑆 ∪ (𝑋 ∖ 𝑌))) ∈ 𝐽) → (((int‘𝐽)‘(𝑆 ∪ (𝑋 ∖ 𝑌))) ∩ 𝑌) ∈ (𝐽 ↾t 𝑌)) |
89 | 19, 83, 87, 88 | syl3anc 1318 |
. . . 4
⊢ ((𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌) → (((int‘𝐽)‘(𝑆 ∪ (𝑋 ∖ 𝑌))) ∩ 𝑌) ∈ (𝐽 ↾t 𝑌)) |
90 | 89, 1 | syl6eleqr 2699 |
. . 3
⊢ ((𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌) → (((int‘𝐽)‘(𝑆 ∪ (𝑋 ∖ 𝑌))) ∩ 𝑌) ∈ 𝐾) |
91 | 4 | ntrss2 20671 |
. . . . . 6
⊢ ((𝐽 ∈ Top ∧ (𝑆 ∪ (𝑋 ∖ 𝑌)) ⊆ 𝑋) → ((int‘𝐽)‘(𝑆 ∪ (𝑋 ∖ 𝑌))) ⊆ (𝑆 ∪ (𝑋 ∖ 𝑌))) |
92 | 19, 85, 91 | syl2anc 691 |
. . . . 5
⊢ ((𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌) → ((int‘𝐽)‘(𝑆 ∪ (𝑋 ∖ 𝑌))) ⊆ (𝑆 ∪ (𝑋 ∖ 𝑌))) |
93 | | ssrin 3800 |
. . . . 5
⊢
(((int‘𝐽)‘(𝑆 ∪ (𝑋 ∖ 𝑌))) ⊆ (𝑆 ∪ (𝑋 ∖ 𝑌)) → (((int‘𝐽)‘(𝑆 ∪ (𝑋 ∖ 𝑌))) ∩ 𝑌) ⊆ ((𝑆 ∪ (𝑋 ∖ 𝑌)) ∩ 𝑌)) |
94 | 92, 93 | syl 17 |
. . . 4
⊢ ((𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌) → (((int‘𝐽)‘(𝑆 ∪ (𝑋 ∖ 𝑌))) ∩ 𝑌) ⊆ ((𝑆 ∪ (𝑋 ∖ 𝑌)) ∩ 𝑌)) |
95 | | elin 3758 |
. . . . . . 7
⊢ (𝑥 ∈ ((𝑆 ∪ (𝑋 ∖ 𝑌)) ∩ 𝑌) ↔ (𝑥 ∈ (𝑆 ∪ (𝑋 ∖ 𝑌)) ∧ 𝑥 ∈ 𝑌)) |
96 | | elun 3715 |
. . . . . . . . 9
⊢ (𝑥 ∈ (𝑆 ∪ (𝑋 ∖ 𝑌)) ↔ (𝑥 ∈ 𝑆 ∨ 𝑥 ∈ (𝑋 ∖ 𝑌))) |
97 | | orcom 401 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝑆 ∨ 𝑥 ∈ (𝑋 ∖ 𝑌)) ↔ (𝑥 ∈ (𝑋 ∖ 𝑌) ∨ 𝑥 ∈ 𝑆)) |
98 | | df-or 384 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ (𝑋 ∖ 𝑌) ∨ 𝑥 ∈ 𝑆) ↔ (¬ 𝑥 ∈ (𝑋 ∖ 𝑌) → 𝑥 ∈ 𝑆)) |
99 | 97, 98 | bitri 263 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝑆 ∨ 𝑥 ∈ (𝑋 ∖ 𝑌)) ↔ (¬ 𝑥 ∈ (𝑋 ∖ 𝑌) → 𝑥 ∈ 𝑆)) |
100 | 96, 99 | bitri 263 |
. . . . . . . 8
⊢ (𝑥 ∈ (𝑆 ∪ (𝑋 ∖ 𝑌)) ↔ (¬ 𝑥 ∈ (𝑋 ∖ 𝑌) → 𝑥 ∈ 𝑆)) |
101 | 100 | anbi1i 727 |
. . . . . . 7
⊢ ((𝑥 ∈ (𝑆 ∪ (𝑋 ∖ 𝑌)) ∧ 𝑥 ∈ 𝑌) ↔ ((¬ 𝑥 ∈ (𝑋 ∖ 𝑌) → 𝑥 ∈ 𝑆) ∧ 𝑥 ∈ 𝑌)) |
102 | 95, 101 | bitri 263 |
. . . . . 6
⊢ (𝑥 ∈ ((𝑆 ∪ (𝑋 ∖ 𝑌)) ∩ 𝑌) ↔ ((¬ 𝑥 ∈ (𝑋 ∖ 𝑌) → 𝑥 ∈ 𝑆) ∧ 𝑥 ∈ 𝑌)) |
103 | | elndif 3696 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝑌 → ¬ 𝑥 ∈ (𝑋 ∖ 𝑌)) |
104 | | pm2.27 41 |
. . . . . . . . 9
⊢ (¬
𝑥 ∈ (𝑋 ∖ 𝑌) → ((¬ 𝑥 ∈ (𝑋 ∖ 𝑌) → 𝑥 ∈ 𝑆) → 𝑥 ∈ 𝑆)) |
105 | 103, 104 | syl 17 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝑌 → ((¬ 𝑥 ∈ (𝑋 ∖ 𝑌) → 𝑥 ∈ 𝑆) → 𝑥 ∈ 𝑆)) |
106 | 105 | impcom 445 |
. . . . . . 7
⊢ (((¬
𝑥 ∈ (𝑋 ∖ 𝑌) → 𝑥 ∈ 𝑆) ∧ 𝑥 ∈ 𝑌) → 𝑥 ∈ 𝑆) |
107 | 106 | a1i 11 |
. . . . . 6
⊢ ((𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌) → (((¬ 𝑥 ∈ (𝑋 ∖ 𝑌) → 𝑥 ∈ 𝑆) ∧ 𝑥 ∈ 𝑌) → 𝑥 ∈ 𝑆)) |
108 | 102, 107 | syl5bi 231 |
. . . . 5
⊢ ((𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌) → (𝑥 ∈ ((𝑆 ∪ (𝑋 ∖ 𝑌)) ∩ 𝑌) → 𝑥 ∈ 𝑆)) |
109 | 108 | ssrdv 3574 |
. . . 4
⊢ ((𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌) → ((𝑆 ∪ (𝑋 ∖ 𝑌)) ∩ 𝑌) ⊆ 𝑆) |
110 | 94, 109 | sstrd 3578 |
. . 3
⊢ ((𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌) → (((int‘𝐽)‘(𝑆 ∪ (𝑋 ∖ 𝑌))) ∩ 𝑌) ⊆ 𝑆) |
111 | 54 | ssntr 20672 |
. . 3
⊢ (((𝐾 ∈ Top ∧ 𝑆 ⊆ ∪ (𝐽
↾t 𝑌))
∧ ((((int‘𝐽)‘(𝑆 ∪ (𝑋 ∖ 𝑌))) ∩ 𝑌) ∈ 𝐾 ∧ (((int‘𝐽)‘(𝑆 ∪ (𝑋 ∖ 𝑌))) ∩ 𝑌) ⊆ 𝑆)) → (((int‘𝐽)‘(𝑆 ∪ (𝑋 ∖ 𝑌))) ∩ 𝑌) ⊆ ((int‘𝐾)‘𝑆)) |
112 | 82, 14, 90, 110, 111 | syl22anc 1319 |
. 2
⊢ ((𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌) → (((int‘𝐽)‘(𝑆 ∪ (𝑋 ∖ 𝑌))) ∩ 𝑌) ⊆ ((int‘𝐾)‘𝑆)) |
113 | 81, 112 | eqssd 3585 |
1
⊢ ((𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌) → ((int‘𝐾)‘𝑆) = (((int‘𝐽)‘(𝑆 ∪ (𝑋 ∖ 𝑌))) ∩ 𝑌)) |