This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem restntr

Description: An interior in a subspace topology. Willard inGeneral Topology says that there is no analogue of restcls for interiors. In some sense, that is true. (Contributed by Jeff Hankins, 23-Jan-2010) (Revised by Mario Carneiro, 15-Dec-2013)

Ref Expression
Hypotheses restcls.1 ⊢ 𝑋 = ∪ 𝐽
restcls.2 ⊢ 𝐾 = ( 𝐽 ↾t 𝑌 )
Assertion restntr ( ( 𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌 ) → ( ( int ‘ 𝐾 ) ‘ 𝑆 ) = ( ( ( int ‘ 𝐽 ) ‘ ( 𝑆 ∪ ( 𝑋 ∖ 𝑌 ) ) ) ∩ 𝑌 ) )

Proof

Step Hyp Ref Expression
1 restcls.1 ⊢ 𝑋 = ∪ 𝐽
2 restcls.2 ⊢ 𝐾 = ( 𝐽 ↾t 𝑌 )
3 2 fveq2i ⊢ ( int ‘ 𝐾 ) = ( int ‘ ( 𝐽 ↾t 𝑌 ) )
4 3 fveq1i ⊢ ( ( int ‘ 𝐾 ) ‘ 𝑆 ) = ( ( int ‘ ( 𝐽 ↾t 𝑌 ) ) ‘ 𝑆 )
5 1 topopn ⊢ ( 𝐽 ∈ Top → 𝑋 ∈ 𝐽 )
6 ssexg ⊢ ( ( 𝑌 ⊆ 𝑋 ∧ 𝑋 ∈ 𝐽 ) → 𝑌 ∈ V )
7 6 ancoms ⊢ ( ( 𝑋 ∈ 𝐽 ∧ 𝑌 ⊆ 𝑋 ) → 𝑌 ∈ V )
8 5 7 sylan ⊢ ( ( 𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ) → 𝑌 ∈ V )
9 resttop ⊢ ( ( 𝐽 ∈ Top ∧ 𝑌 ∈ V ) → ( 𝐽 ↾t 𝑌 ) ∈ Top )
10 8 9 syldan ⊢ ( ( 𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ) → ( 𝐽 ↾t 𝑌 ) ∈ Top )
11 10 3adant3 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌 ) → ( 𝐽 ↾t 𝑌 ) ∈ Top )
12 1 restuni ⊢ ( ( 𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ) → 𝑌 = ∪ ( 𝐽 ↾t 𝑌 ) )
13 12 sseq2d ⊢ ( ( 𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ) → ( 𝑆 ⊆ 𝑌 ↔ 𝑆 ⊆ ∪ ( 𝐽 ↾t 𝑌 ) ) )
14 13 biimp3a ⊢ ( ( 𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌 ) → 𝑆 ⊆ ∪ ( 𝐽 ↾t 𝑌 ) )
15 eqid ⊢ ∪ ( 𝐽 ↾t 𝑌 ) = ∪ ( 𝐽 ↾t 𝑌 )
16 15 ntropn ⊢ ( ( ( 𝐽 ↾t 𝑌 ) ∈ Top ∧ 𝑆 ⊆ ∪ ( 𝐽 ↾t 𝑌 ) ) → ( ( int ‘ ( 𝐽 ↾t 𝑌 ) ) ‘ 𝑆 ) ∈ ( 𝐽 ↾t 𝑌 ) )
17 11 14 16 syl2anc ⊢ ( ( 𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌 ) → ( ( int ‘ ( 𝐽 ↾t 𝑌 ) ) ‘ 𝑆 ) ∈ ( 𝐽 ↾t 𝑌 ) )
18 4 17 eqeltrid ⊢ ( ( 𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌 ) → ( ( int ‘ 𝐾 ) ‘ 𝑆 ) ∈ ( 𝐽 ↾t 𝑌 ) )
19 simp1 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌 ) → 𝐽 ∈ Top )
20 uniexg ⊢ ( 𝐽 ∈ Top → ∪ 𝐽 ∈ V )
21 1 20 eqeltrid ⊢ ( 𝐽 ∈ Top → 𝑋 ∈ V )
22 ssexg ⊢ ( ( 𝑌 ⊆ 𝑋 ∧ 𝑋 ∈ V ) → 𝑌 ∈ V )
23 21 22 sylan2 ⊢ ( ( 𝑌 ⊆ 𝑋 ∧ 𝐽 ∈ Top ) → 𝑌 ∈ V )
24 23 ancoms ⊢ ( ( 𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ) → 𝑌 ∈ V )
25 24 3adant3 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌 ) → 𝑌 ∈ V )
26 elrest ⊢ ( ( 𝐽 ∈ Top ∧ 𝑌 ∈ V ) → ( ( ( int ‘ 𝐾 ) ‘ 𝑆 ) ∈ ( 𝐽 ↾t 𝑌 ) ↔ ∃ 𝑜 ∈ 𝐽 ( ( int ‘ 𝐾 ) ‘ 𝑆 ) = ( 𝑜 ∩ 𝑌 ) ) )
27 19 25 26 syl2anc ⊢ ( ( 𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌 ) → ( ( ( int ‘ 𝐾 ) ‘ 𝑆 ) ∈ ( 𝐽 ↾t 𝑌 ) ↔ ∃ 𝑜 ∈ 𝐽 ( ( int ‘ 𝐾 ) ‘ 𝑆 ) = ( 𝑜 ∩ 𝑌 ) ) )
28 18 27 mpbid ⊢ ( ( 𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌 ) → ∃ 𝑜 ∈ 𝐽 ( ( int ‘ 𝐾 ) ‘ 𝑆 ) = ( 𝑜 ∩ 𝑌 ) )
29 1 eltopss ⊢ ( ( 𝐽 ∈ Top ∧ 𝑜 ∈ 𝐽 ) → 𝑜 ⊆ 𝑋 )
30 29 sseld ⊢ ( ( 𝐽 ∈ Top ∧ 𝑜 ∈ 𝐽 ) → ( 𝑥 ∈ 𝑜 → 𝑥 ∈ 𝑋 ) )
31 30 adantrr ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑜 ∈ 𝐽 ∧ ( ( int ‘ 𝐾 ) ‘ 𝑆 ) = ( 𝑜 ∩ 𝑌 ) ) ) → ( 𝑥 ∈ 𝑜 → 𝑥 ∈ 𝑋 ) )
32 31 3ad2antl1 ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌 ) ∧ ( 𝑜 ∈ 𝐽 ∧ ( ( int ‘ 𝐾 ) ‘ 𝑆 ) = ( 𝑜 ∩ 𝑌 ) ) ) → ( 𝑥 ∈ 𝑜 → 𝑥 ∈ 𝑋 ) )
33 eldif ⊢ ( 𝑥 ∈ ( 𝑋 ∖ 𝑌 ) ↔ ( 𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ 𝑌 ) )
34 33 simplbi2 ⊢ ( 𝑥 ∈ 𝑋 → ( ¬ 𝑥 ∈ 𝑌 → 𝑥 ∈ ( 𝑋 ∖ 𝑌 ) ) )
35 34 orrd ⊢ ( 𝑥 ∈ 𝑋 → ( 𝑥 ∈ 𝑌 ∨ 𝑥 ∈ ( 𝑋 ∖ 𝑌 ) ) )
36 32 35 syl6 ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌 ) ∧ ( 𝑜 ∈ 𝐽 ∧ ( ( int ‘ 𝐾 ) ‘ 𝑆 ) = ( 𝑜 ∩ 𝑌 ) ) ) → ( 𝑥 ∈ 𝑜 → ( 𝑥 ∈ 𝑌 ∨ 𝑥 ∈ ( 𝑋 ∖ 𝑌 ) ) ) )
37 elin ⊢ ( 𝑥 ∈ ( 𝑜 ∩ 𝑌 ) ↔ ( 𝑥 ∈ 𝑜 ∧ 𝑥 ∈ 𝑌 ) )
38 eleq2 ⊢ ( ( ( int ‘ 𝐾 ) ‘ 𝑆 ) = ( 𝑜 ∩ 𝑌 ) → ( 𝑥 ∈ ( ( int ‘ 𝐾 ) ‘ 𝑆 ) ↔ 𝑥 ∈ ( 𝑜 ∩ 𝑌 ) ) )
39 elun1 ⊢ ( 𝑥 ∈ ( ( int ‘ 𝐾 ) ‘ 𝑆 ) → 𝑥 ∈ ( ( ( int ‘ 𝐾 ) ‘ 𝑆 ) ∪ ( 𝑋 ∖ 𝑌 ) ) )
40 38 39 biimtrrdi ⊢ ( ( ( int ‘ 𝐾 ) ‘ 𝑆 ) = ( 𝑜 ∩ 𝑌 ) → ( 𝑥 ∈ ( 𝑜 ∩ 𝑌 ) → 𝑥 ∈ ( ( ( int ‘ 𝐾 ) ‘ 𝑆 ) ∪ ( 𝑋 ∖ 𝑌 ) ) ) )
41 40 ad2antll ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌 ) ∧ ( 𝑜 ∈ 𝐽 ∧ ( ( int ‘ 𝐾 ) ‘ 𝑆 ) = ( 𝑜 ∩ 𝑌 ) ) ) → ( 𝑥 ∈ ( 𝑜 ∩ 𝑌 ) → 𝑥 ∈ ( ( ( int ‘ 𝐾 ) ‘ 𝑆 ) ∪ ( 𝑋 ∖ 𝑌 ) ) ) )
42 37 41 biimtrrid ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌 ) ∧ ( 𝑜 ∈ 𝐽 ∧ ( ( int ‘ 𝐾 ) ‘ 𝑆 ) = ( 𝑜 ∩ 𝑌 ) ) ) → ( ( 𝑥 ∈ 𝑜 ∧ 𝑥 ∈ 𝑌 ) → 𝑥 ∈ ( ( ( int ‘ 𝐾 ) ‘ 𝑆 ) ∪ ( 𝑋 ∖ 𝑌 ) ) ) )
43 42 expdimp ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌 ) ∧ ( 𝑜 ∈ 𝐽 ∧ ( ( int ‘ 𝐾 ) ‘ 𝑆 ) = ( 𝑜 ∩ 𝑌 ) ) ) ∧ 𝑥 ∈ 𝑜 ) → ( 𝑥 ∈ 𝑌 → 𝑥 ∈ ( ( ( int ‘ 𝐾 ) ‘ 𝑆 ) ∪ ( 𝑋 ∖ 𝑌 ) ) ) )
44 elun2 ⊢ ( 𝑥 ∈ ( 𝑋 ∖ 𝑌 ) → 𝑥 ∈ ( ( ( int ‘ 𝐾 ) ‘ 𝑆 ) ∪ ( 𝑋 ∖ 𝑌 ) ) )
45 44 a1i ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌 ) ∧ ( 𝑜 ∈ 𝐽 ∧ ( ( int ‘ 𝐾 ) ‘ 𝑆 ) = ( 𝑜 ∩ 𝑌 ) ) ) ∧ 𝑥 ∈ 𝑜 ) → ( 𝑥 ∈ ( 𝑋 ∖ 𝑌 ) → 𝑥 ∈ ( ( ( int ‘ 𝐾 ) ‘ 𝑆 ) ∪ ( 𝑋 ∖ 𝑌 ) ) ) )
46 43 45 jaod ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌 ) ∧ ( 𝑜 ∈ 𝐽 ∧ ( ( int ‘ 𝐾 ) ‘ 𝑆 ) = ( 𝑜 ∩ 𝑌 ) ) ) ∧ 𝑥 ∈ 𝑜 ) → ( ( 𝑥 ∈ 𝑌 ∨ 𝑥 ∈ ( 𝑋 ∖ 𝑌 ) ) → 𝑥 ∈ ( ( ( int ‘ 𝐾 ) ‘ 𝑆 ) ∪ ( 𝑋 ∖ 𝑌 ) ) ) )
47 46 ex ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌 ) ∧ ( 𝑜 ∈ 𝐽 ∧ ( ( int ‘ 𝐾 ) ‘ 𝑆 ) = ( 𝑜 ∩ 𝑌 ) ) ) → ( 𝑥 ∈ 𝑜 → ( ( 𝑥 ∈ 𝑌 ∨ 𝑥 ∈ ( 𝑋 ∖ 𝑌 ) ) → 𝑥 ∈ ( ( ( int ‘ 𝐾 ) ‘ 𝑆 ) ∪ ( 𝑋 ∖ 𝑌 ) ) ) ) )
48 36 47 mpdd ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌 ) ∧ ( 𝑜 ∈ 𝐽 ∧ ( ( int ‘ 𝐾 ) ‘ 𝑆 ) = ( 𝑜 ∩ 𝑌 ) ) ) → ( 𝑥 ∈ 𝑜 → 𝑥 ∈ ( ( ( int ‘ 𝐾 ) ‘ 𝑆 ) ∪ ( 𝑋 ∖ 𝑌 ) ) ) )
49 48 ssrdv ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌 ) ∧ ( 𝑜 ∈ 𝐽 ∧ ( ( int ‘ 𝐾 ) ‘ 𝑆 ) = ( 𝑜 ∩ 𝑌 ) ) ) → 𝑜 ⊆ ( ( ( int ‘ 𝐾 ) ‘ 𝑆 ) ∪ ( 𝑋 ∖ 𝑌 ) ) )
50 11 adantr ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌 ) ∧ ( 𝑜 ∈ 𝐽 ∧ ( ( int ‘ 𝐾 ) ‘ 𝑆 ) = ( 𝑜 ∩ 𝑌 ) ) ) → ( 𝐽 ↾t 𝑌 ) ∈ Top )
51 2 50 eqeltrid ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌 ) ∧ ( 𝑜 ∈ 𝐽 ∧ ( ( int ‘ 𝐾 ) ‘ 𝑆 ) = ( 𝑜 ∩ 𝑌 ) ) ) → 𝐾 ∈ Top )
52 14 adantr ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌 ) ∧ ( 𝑜 ∈ 𝐽 ∧ ( ( int ‘ 𝐾 ) ‘ 𝑆 ) = ( 𝑜 ∩ 𝑌 ) ) ) → 𝑆 ⊆ ∪ ( 𝐽 ↾t 𝑌 ) )
53 2 unieqi ⊢ ∪ 𝐾 = ∪ ( 𝐽 ↾t 𝑌 )
54 53 eqcomi ⊢ ∪ ( 𝐽 ↾t 𝑌 ) = ∪ 𝐾
55 54 ntrss2 ⊢ ( ( 𝐾 ∈ Top ∧ 𝑆 ⊆ ∪ ( 𝐽 ↾t 𝑌 ) ) → ( ( int ‘ 𝐾 ) ‘ 𝑆 ) ⊆ 𝑆 )
56 51 52 55 syl2anc ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌 ) ∧ ( 𝑜 ∈ 𝐽 ∧ ( ( int ‘ 𝐾 ) ‘ 𝑆 ) = ( 𝑜 ∩ 𝑌 ) ) ) → ( ( int ‘ 𝐾 ) ‘ 𝑆 ) ⊆ 𝑆 )
57 unss1 ⊢ ( ( ( int ‘ 𝐾 ) ‘ 𝑆 ) ⊆ 𝑆 → ( ( ( int ‘ 𝐾 ) ‘ 𝑆 ) ∪ ( 𝑋 ∖ 𝑌 ) ) ⊆ ( 𝑆 ∪ ( 𝑋 ∖ 𝑌 ) ) )
58 56 57 syl ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌 ) ∧ ( 𝑜 ∈ 𝐽 ∧ ( ( int ‘ 𝐾 ) ‘ 𝑆 ) = ( 𝑜 ∩ 𝑌 ) ) ) → ( ( ( int ‘ 𝐾 ) ‘ 𝑆 ) ∪ ( 𝑋 ∖ 𝑌 ) ) ⊆ ( 𝑆 ∪ ( 𝑋 ∖ 𝑌 ) ) )
59 49 58 sstrd ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌 ) ∧ ( 𝑜 ∈ 𝐽 ∧ ( ( int ‘ 𝐾 ) ‘ 𝑆 ) = ( 𝑜 ∩ 𝑌 ) ) ) → 𝑜 ⊆ ( 𝑆 ∪ ( 𝑋 ∖ 𝑌 ) ) )
60 simpl1 ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌 ) ∧ ( 𝑜 ∈ 𝐽 ∧ 𝑜 ⊆ ( 𝑆 ∪ ( 𝑋 ∖ 𝑌 ) ) ) ) → 𝐽 ∈ Top )
61 sstr ⊢ ( ( 𝑆 ⊆ 𝑌 ∧ 𝑌 ⊆ 𝑋 ) → 𝑆 ⊆ 𝑋 )
62 61 ancoms ⊢ ( ( 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌 ) → 𝑆 ⊆ 𝑋 )
63 62 3adant1 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌 ) → 𝑆 ⊆ 𝑋 )
64 63 adantr ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌 ) ∧ ( 𝑜 ∈ 𝐽 ∧ 𝑜 ⊆ ( 𝑆 ∪ ( 𝑋 ∖ 𝑌 ) ) ) ) → 𝑆 ⊆ 𝑋 )
65 difss ⊢ ( 𝑋 ∖ 𝑌 ) ⊆ 𝑋
66 unss ⊢ ( ( 𝑆 ⊆ 𝑋 ∧ ( 𝑋 ∖ 𝑌 ) ⊆ 𝑋 ) ↔ ( 𝑆 ∪ ( 𝑋 ∖ 𝑌 ) ) ⊆ 𝑋 )
67 64 65 66 sylanblc ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌 ) ∧ ( 𝑜 ∈ 𝐽 ∧ 𝑜 ⊆ ( 𝑆 ∪ ( 𝑋 ∖ 𝑌 ) ) ) ) → ( 𝑆 ∪ ( 𝑋 ∖ 𝑌 ) ) ⊆ 𝑋 )
68 simprl ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌 ) ∧ ( 𝑜 ∈ 𝐽 ∧ 𝑜 ⊆ ( 𝑆 ∪ ( 𝑋 ∖ 𝑌 ) ) ) ) → 𝑜 ∈ 𝐽 )
69 simprr ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌 ) ∧ ( 𝑜 ∈ 𝐽 ∧ 𝑜 ⊆ ( 𝑆 ∪ ( 𝑋 ∖ 𝑌 ) ) ) ) → 𝑜 ⊆ ( 𝑆 ∪ ( 𝑋 ∖ 𝑌 ) ) )
70 1 ssntr ⊢ ( ( ( 𝐽 ∈ Top ∧ ( 𝑆 ∪ ( 𝑋 ∖ 𝑌 ) ) ⊆ 𝑋 ) ∧ ( 𝑜 ∈ 𝐽 ∧ 𝑜 ⊆ ( 𝑆 ∪ ( 𝑋 ∖ 𝑌 ) ) ) ) → 𝑜 ⊆ ( ( int ‘ 𝐽 ) ‘ ( 𝑆 ∪ ( 𝑋 ∖ 𝑌 ) ) ) )
71 60 67 68 69 70 syl22anc ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌 ) ∧ ( 𝑜 ∈ 𝐽 ∧ 𝑜 ⊆ ( 𝑆 ∪ ( 𝑋 ∖ 𝑌 ) ) ) ) → 𝑜 ⊆ ( ( int ‘ 𝐽 ) ‘ ( 𝑆 ∪ ( 𝑋 ∖ 𝑌 ) ) ) )
72 71 ssrind ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌 ) ∧ ( 𝑜 ∈ 𝐽 ∧ 𝑜 ⊆ ( 𝑆 ∪ ( 𝑋 ∖ 𝑌 ) ) ) ) → ( 𝑜 ∩ 𝑌 ) ⊆ ( ( ( int ‘ 𝐽 ) ‘ ( 𝑆 ∪ ( 𝑋 ∖ 𝑌 ) ) ) ∩ 𝑌 ) )
73 sseq1 ⊢ ( ( ( int ‘ 𝐾 ) ‘ 𝑆 ) = ( 𝑜 ∩ 𝑌 ) → ( ( ( int ‘ 𝐾 ) ‘ 𝑆 ) ⊆ ( ( ( int ‘ 𝐽 ) ‘ ( 𝑆 ∪ ( 𝑋 ∖ 𝑌 ) ) ) ∩ 𝑌 ) ↔ ( 𝑜 ∩ 𝑌 ) ⊆ ( ( ( int ‘ 𝐽 ) ‘ ( 𝑆 ∪ ( 𝑋 ∖ 𝑌 ) ) ) ∩ 𝑌 ) ) )
74 72 73 syl5ibrcom ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌 ) ∧ ( 𝑜 ∈ 𝐽 ∧ 𝑜 ⊆ ( 𝑆 ∪ ( 𝑋 ∖ 𝑌 ) ) ) ) → ( ( ( int ‘ 𝐾 ) ‘ 𝑆 ) = ( 𝑜 ∩ 𝑌 ) → ( ( int ‘ 𝐾 ) ‘ 𝑆 ) ⊆ ( ( ( int ‘ 𝐽 ) ‘ ( 𝑆 ∪ ( 𝑋 ∖ 𝑌 ) ) ) ∩ 𝑌 ) ) )
75 74 expr ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌 ) ∧ 𝑜 ∈ 𝐽 ) → ( 𝑜 ⊆ ( 𝑆 ∪ ( 𝑋 ∖ 𝑌 ) ) → ( ( ( int ‘ 𝐾 ) ‘ 𝑆 ) = ( 𝑜 ∩ 𝑌 ) → ( ( int ‘ 𝐾 ) ‘ 𝑆 ) ⊆ ( ( ( int ‘ 𝐽 ) ‘ ( 𝑆 ∪ ( 𝑋 ∖ 𝑌 ) ) ) ∩ 𝑌 ) ) ) )
76 75 com23 ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌 ) ∧ 𝑜 ∈ 𝐽 ) → ( ( ( int ‘ 𝐾 ) ‘ 𝑆 ) = ( 𝑜 ∩ 𝑌 ) → ( 𝑜 ⊆ ( 𝑆 ∪ ( 𝑋 ∖ 𝑌 ) ) → ( ( int ‘ 𝐾 ) ‘ 𝑆 ) ⊆ ( ( ( int ‘ 𝐽 ) ‘ ( 𝑆 ∪ ( 𝑋 ∖ 𝑌 ) ) ) ∩ 𝑌 ) ) ) )
77 76 impr ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌 ) ∧ ( 𝑜 ∈ 𝐽 ∧ ( ( int ‘ 𝐾 ) ‘ 𝑆 ) = ( 𝑜 ∩ 𝑌 ) ) ) → ( 𝑜 ⊆ ( 𝑆 ∪ ( 𝑋 ∖ 𝑌 ) ) → ( ( int ‘ 𝐾 ) ‘ 𝑆 ) ⊆ ( ( ( int ‘ 𝐽 ) ‘ ( 𝑆 ∪ ( 𝑋 ∖ 𝑌 ) ) ) ∩ 𝑌 ) ) )
78 59 77 mpd ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌 ) ∧ ( 𝑜 ∈ 𝐽 ∧ ( ( int ‘ 𝐾 ) ‘ 𝑆 ) = ( 𝑜 ∩ 𝑌 ) ) ) → ( ( int ‘ 𝐾 ) ‘ 𝑆 ) ⊆ ( ( ( int ‘ 𝐽 ) ‘ ( 𝑆 ∪ ( 𝑋 ∖ 𝑌 ) ) ) ∩ 𝑌 ) )
79 28 78 rexlimddv ⊢ ( ( 𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌 ) → ( ( int ‘ 𝐾 ) ‘ 𝑆 ) ⊆ ( ( ( int ‘ 𝐽 ) ‘ ( 𝑆 ∪ ( 𝑋 ∖ 𝑌 ) ) ) ∩ 𝑌 ) )
80 2 11 eqeltrid ⊢ ( ( 𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌 ) → 𝐾 ∈ Top )
81 8 3adant3 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌 ) → 𝑌 ∈ V )
82 63 65 66 sylanblc ⊢ ( ( 𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌 ) → ( 𝑆 ∪ ( 𝑋 ∖ 𝑌 ) ) ⊆ 𝑋 )
83 1 ntropn ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑆 ∪ ( 𝑋 ∖ 𝑌 ) ) ⊆ 𝑋 ) → ( ( int ‘ 𝐽 ) ‘ ( 𝑆 ∪ ( 𝑋 ∖ 𝑌 ) ) ) ∈ 𝐽 )
84 19 82 83 syl2anc ⊢ ( ( 𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌 ) → ( ( int ‘ 𝐽 ) ‘ ( 𝑆 ∪ ( 𝑋 ∖ 𝑌 ) ) ) ∈ 𝐽 )
85 elrestr ⊢ ( ( 𝐽 ∈ Top ∧ 𝑌 ∈ V ∧ ( ( int ‘ 𝐽 ) ‘ ( 𝑆 ∪ ( 𝑋 ∖ 𝑌 ) ) ) ∈ 𝐽 ) → ( ( ( int ‘ 𝐽 ) ‘ ( 𝑆 ∪ ( 𝑋 ∖ 𝑌 ) ) ) ∩ 𝑌 ) ∈ ( 𝐽 ↾t 𝑌 ) )
86 19 81 84 85 syl3anc ⊢ ( ( 𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌 ) → ( ( ( int ‘ 𝐽 ) ‘ ( 𝑆 ∪ ( 𝑋 ∖ 𝑌 ) ) ) ∩ 𝑌 ) ∈ ( 𝐽 ↾t 𝑌 ) )
87 86 2 eleqtrrdi ⊢ ( ( 𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌 ) → ( ( ( int ‘ 𝐽 ) ‘ ( 𝑆 ∪ ( 𝑋 ∖ 𝑌 ) ) ) ∩ 𝑌 ) ∈ 𝐾 )
88 1 ntrss2 ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑆 ∪ ( 𝑋 ∖ 𝑌 ) ) ⊆ 𝑋 ) → ( ( int ‘ 𝐽 ) ‘ ( 𝑆 ∪ ( 𝑋 ∖ 𝑌 ) ) ) ⊆ ( 𝑆 ∪ ( 𝑋 ∖ 𝑌 ) ) )
89 19 82 88 syl2anc ⊢ ( ( 𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌 ) → ( ( int ‘ 𝐽 ) ‘ ( 𝑆 ∪ ( 𝑋 ∖ 𝑌 ) ) ) ⊆ ( 𝑆 ∪ ( 𝑋 ∖ 𝑌 ) ) )
90 89 ssrind ⊢ ( ( 𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌 ) → ( ( ( int ‘ 𝐽 ) ‘ ( 𝑆 ∪ ( 𝑋 ∖ 𝑌 ) ) ) ∩ 𝑌 ) ⊆ ( ( 𝑆 ∪ ( 𝑋 ∖ 𝑌 ) ) ∩ 𝑌 ) )
91 elin ⊢ ( 𝑥 ∈ ( ( 𝑆 ∪ ( 𝑋 ∖ 𝑌 ) ) ∩ 𝑌 ) ↔ ( 𝑥 ∈ ( 𝑆 ∪ ( 𝑋 ∖ 𝑌 ) ) ∧ 𝑥 ∈ 𝑌 ) )
92 elun ⊢ ( 𝑥 ∈ ( 𝑆 ∪ ( 𝑋 ∖ 𝑌 ) ) ↔ ( 𝑥 ∈ 𝑆 ∨ 𝑥 ∈ ( 𝑋 ∖ 𝑌 ) ) )
93 orcom ⊢ ( ( 𝑥 ∈ 𝑆 ∨ 𝑥 ∈ ( 𝑋 ∖ 𝑌 ) ) ↔ ( 𝑥 ∈ ( 𝑋 ∖ 𝑌 ) ∨ 𝑥 ∈ 𝑆 ) )
94 df-or ⊢ ( ( 𝑥 ∈ ( 𝑋 ∖ 𝑌 ) ∨ 𝑥 ∈ 𝑆 ) ↔ ( ¬ 𝑥 ∈ ( 𝑋 ∖ 𝑌 ) → 𝑥 ∈ 𝑆 ) )
95 93 94 bitri ⊢ ( ( 𝑥 ∈ 𝑆 ∨ 𝑥 ∈ ( 𝑋 ∖ 𝑌 ) ) ↔ ( ¬ 𝑥 ∈ ( 𝑋 ∖ 𝑌 ) → 𝑥 ∈ 𝑆 ) )
96 92 95 bitri ⊢ ( 𝑥 ∈ ( 𝑆 ∪ ( 𝑋 ∖ 𝑌 ) ) ↔ ( ¬ 𝑥 ∈ ( 𝑋 ∖ 𝑌 ) → 𝑥 ∈ 𝑆 ) )
97 96 anbi1i ⊢ ( ( 𝑥 ∈ ( 𝑆 ∪ ( 𝑋 ∖ 𝑌 ) ) ∧ 𝑥 ∈ 𝑌 ) ↔ ( ( ¬ 𝑥 ∈ ( 𝑋 ∖ 𝑌 ) → 𝑥 ∈ 𝑆 ) ∧ 𝑥 ∈ 𝑌 ) )
98 91 97 bitri ⊢ ( 𝑥 ∈ ( ( 𝑆 ∪ ( 𝑋 ∖ 𝑌 ) ) ∩ 𝑌 ) ↔ ( ( ¬ 𝑥 ∈ ( 𝑋 ∖ 𝑌 ) → 𝑥 ∈ 𝑆 ) ∧ 𝑥 ∈ 𝑌 ) )
99 elndif ⊢ ( 𝑥 ∈ 𝑌 → ¬ 𝑥 ∈ ( 𝑋 ∖ 𝑌 ) )
100 pm2.27 ⊢ ( ¬ 𝑥 ∈ ( 𝑋 ∖ 𝑌 ) → ( ( ¬ 𝑥 ∈ ( 𝑋 ∖ 𝑌 ) → 𝑥 ∈ 𝑆 ) → 𝑥 ∈ 𝑆 ) )
101 99 100 syl ⊢ ( 𝑥 ∈ 𝑌 → ( ( ¬ 𝑥 ∈ ( 𝑋 ∖ 𝑌 ) → 𝑥 ∈ 𝑆 ) → 𝑥 ∈ 𝑆 ) )
102 101 impcom ⊢ ( ( ( ¬ 𝑥 ∈ ( 𝑋 ∖ 𝑌 ) → 𝑥 ∈ 𝑆 ) ∧ 𝑥 ∈ 𝑌 ) → 𝑥 ∈ 𝑆 )
103 102 a1i ⊢ ( ( 𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌 ) → ( ( ( ¬ 𝑥 ∈ ( 𝑋 ∖ 𝑌 ) → 𝑥 ∈ 𝑆 ) ∧ 𝑥 ∈ 𝑌 ) → 𝑥 ∈ 𝑆 ) )
104 98 103 biimtrid ⊢ ( ( 𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌 ) → ( 𝑥 ∈ ( ( 𝑆 ∪ ( 𝑋 ∖ 𝑌 ) ) ∩ 𝑌 ) → 𝑥 ∈ 𝑆 ) )
105 104 ssrdv ⊢ ( ( 𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌 ) → ( ( 𝑆 ∪ ( 𝑋 ∖ 𝑌 ) ) ∩ 𝑌 ) ⊆ 𝑆 )
106 90 105 sstrd ⊢ ( ( 𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌 ) → ( ( ( int ‘ 𝐽 ) ‘ ( 𝑆 ∪ ( 𝑋 ∖ 𝑌 ) ) ) ∩ 𝑌 ) ⊆ 𝑆 )
107 54 ssntr ⊢ ( ( ( 𝐾 ∈ Top ∧ 𝑆 ⊆ ∪ ( 𝐽 ↾t 𝑌 ) ) ∧ ( ( ( ( int ‘ 𝐽 ) ‘ ( 𝑆 ∪ ( 𝑋 ∖ 𝑌 ) ) ) ∩ 𝑌 ) ∈ 𝐾 ∧ ( ( ( int ‘ 𝐽 ) ‘ ( 𝑆 ∪ ( 𝑋 ∖ 𝑌 ) ) ) ∩ 𝑌 ) ⊆ 𝑆 ) ) → ( ( ( int ‘ 𝐽 ) ‘ ( 𝑆 ∪ ( 𝑋 ∖ 𝑌 ) ) ) ∩ 𝑌 ) ⊆ ( ( int ‘ 𝐾 ) ‘ 𝑆 ) )
108 80 14 87 106 107 syl22anc ⊢ ( ( 𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌 ) → ( ( ( int ‘ 𝐽 ) ‘ ( 𝑆 ∪ ( 𝑋 ∖ 𝑌 ) ) ) ∩ 𝑌 ) ⊆ ( ( int ‘ 𝐾 ) ‘ 𝑆 ) )
109 79 108 eqssd ⊢ ( ( 𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌 ) → ( ( int ‘ 𝐾 ) ‘ 𝑆 ) = ( ( ( int ‘ 𝐽 ) ‘ ( 𝑆 ∪ ( 𝑋 ∖ 𝑌 ) ) ) ∩ 𝑌 ) )