Metamath Proof Explorer

Theorem llyidm

Description: Idempotence of the "locally" predicate, i.e. being "locally A " is a local property. (Contributed by Mario Carneiro, 2-Mar-2015)

Ref Expression
Assertion llyidm Locally Locally 𝐴 = Locally 𝐴

Proof

Step Hyp Ref Expression
1 llytop ⊢ ( 𝑗 ∈ Locally Locally 𝐴 → 𝑗 ∈ Top )
2 llyi ⊢ ( ( 𝑗 ∈ Locally Locally 𝐴 ∧ 𝑥 ∈ 𝑗 ∧ 𝑦 ∈ 𝑥 ) → ∃ 𝑢 ∈ 𝑗 ( 𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ Locally 𝐴 ) )
3 simprr3 ⊢ ( ( ( 𝑗 ∈ Locally Locally 𝐴 ∧ 𝑥 ∈ 𝑗 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑢 ∈ 𝑗 ∧ ( 𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ Locally 𝐴 ) ) ) → ( 𝑗 ↾t 𝑢 ) ∈ Locally 𝐴 )
4 simprl ⊢ ( ( ( 𝑗 ∈ Locally Locally 𝐴 ∧ 𝑥 ∈ 𝑗 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑢 ∈ 𝑗 ∧ ( 𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ Locally 𝐴 ) ) ) → 𝑢 ∈ 𝑗 )
5 ssidd ⊢ ( ( ( 𝑗 ∈ Locally Locally 𝐴 ∧ 𝑥 ∈ 𝑗 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑢 ∈ 𝑗 ∧ ( 𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ Locally 𝐴 ) ) ) → 𝑢 ⊆ 𝑢 )
6 1 3ad2ant1 ⊢ ( ( 𝑗 ∈ Locally Locally 𝐴 ∧ 𝑥 ∈ 𝑗 ∧ 𝑦 ∈ 𝑥 ) → 𝑗 ∈ Top )
7 6 adantr ⊢ ( ( ( 𝑗 ∈ Locally Locally 𝐴 ∧ 𝑥 ∈ 𝑗 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑢 ∈ 𝑗 ∧ ( 𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ Locally 𝐴 ) ) ) → 𝑗 ∈ Top )
8 restopn2 ⊢ ( ( 𝑗 ∈ Top ∧ 𝑢 ∈ 𝑗 ) → ( 𝑢 ∈ ( 𝑗 ↾t 𝑢 ) ↔ ( 𝑢 ∈ 𝑗 ∧ 𝑢 ⊆ 𝑢 ) ) )
9 7 4 8 syl2anc ⊢ ( ( ( 𝑗 ∈ Locally Locally 𝐴 ∧ 𝑥 ∈ 𝑗 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑢 ∈ 𝑗 ∧ ( 𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ Locally 𝐴 ) ) ) → ( 𝑢 ∈ ( 𝑗 ↾t 𝑢 ) ↔ ( 𝑢 ∈ 𝑗 ∧ 𝑢 ⊆ 𝑢 ) ) )
10 4 5 9 mpbir2and ⊢ ( ( ( 𝑗 ∈ Locally Locally 𝐴 ∧ 𝑥 ∈ 𝑗 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑢 ∈ 𝑗 ∧ ( 𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ Locally 𝐴 ) ) ) → 𝑢 ∈ ( 𝑗 ↾t 𝑢 ) )
11 simprr2 ⊢ ( ( ( 𝑗 ∈ Locally Locally 𝐴 ∧ 𝑥 ∈ 𝑗 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑢 ∈ 𝑗 ∧ ( 𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ Locally 𝐴 ) ) ) → 𝑦 ∈ 𝑢 )
12 llyi ⊢ ( ( ( 𝑗 ↾t 𝑢 ) ∈ Locally 𝐴 ∧ 𝑢 ∈ ( 𝑗 ↾t 𝑢 ) ∧ 𝑦 ∈ 𝑢 ) → ∃ 𝑣 ∈ ( 𝑗 ↾t 𝑢 ) ( 𝑣 ⊆ 𝑢 ∧ 𝑦 ∈ 𝑣 ∧ ( ( 𝑗 ↾t 𝑢 ) ↾t 𝑣 ) ∈ 𝐴 ) )
13 3 10 11 12 syl3anc ⊢ ( ( ( 𝑗 ∈ Locally Locally 𝐴 ∧ 𝑥 ∈ 𝑗 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑢 ∈ 𝑗 ∧ ( 𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ Locally 𝐴 ) ) ) → ∃ 𝑣 ∈ ( 𝑗 ↾t 𝑢 ) ( 𝑣 ⊆ 𝑢 ∧ 𝑦 ∈ 𝑣 ∧ ( ( 𝑗 ↾t 𝑢 ) ↾t 𝑣 ) ∈ 𝐴 ) )
14 restopn2 ⊢ ( ( 𝑗 ∈ Top ∧ 𝑢 ∈ 𝑗 ) → ( 𝑣 ∈ ( 𝑗 ↾t 𝑢 ) ↔ ( 𝑣 ∈ 𝑗 ∧ 𝑣 ⊆ 𝑢 ) ) )
15 7 4 14 syl2anc ⊢ ( ( ( 𝑗 ∈ Locally Locally 𝐴 ∧ 𝑥 ∈ 𝑗 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑢 ∈ 𝑗 ∧ ( 𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ Locally 𝐴 ) ) ) → ( 𝑣 ∈ ( 𝑗 ↾t 𝑢 ) ↔ ( 𝑣 ∈ 𝑗 ∧ 𝑣 ⊆ 𝑢 ) ) )
16 simpl ⊢ ( ( 𝑣 ∈ 𝑗 ∧ 𝑣 ⊆ 𝑢 ) → 𝑣 ∈ 𝑗 )
17 15 16 syl6bi ⊢ ( ( ( 𝑗 ∈ Locally Locally 𝐴 ∧ 𝑥 ∈ 𝑗 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑢 ∈ 𝑗 ∧ ( 𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ Locally 𝐴 ) ) ) → ( 𝑣 ∈ ( 𝑗 ↾t 𝑢 ) → 𝑣 ∈ 𝑗 ) )
18 simprl ⊢ ( ( ( ( 𝑗 ∈ Locally Locally 𝐴 ∧ 𝑥 ∈ 𝑗 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑢 ∈ 𝑗 ∧ ( 𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ Locally 𝐴 ) ) ) ∧ ( 𝑣 ∈ 𝑗 ∧ ( 𝑣 ⊆ 𝑢 ∧ 𝑦 ∈ 𝑣 ∧ ( ( 𝑗 ↾t 𝑢 ) ↾t 𝑣 ) ∈ 𝐴 ) ) ) → 𝑣 ∈ 𝑗 )
19 simprr1 ⊢ ( ( ( ( 𝑗 ∈ Locally Locally 𝐴 ∧ 𝑥 ∈ 𝑗 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑢 ∈ 𝑗 ∧ ( 𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ Locally 𝐴 ) ) ) ∧ ( 𝑣 ∈ 𝑗 ∧ ( 𝑣 ⊆ 𝑢 ∧ 𝑦 ∈ 𝑣 ∧ ( ( 𝑗 ↾t 𝑢 ) ↾t 𝑣 ) ∈ 𝐴 ) ) ) → 𝑣 ⊆ 𝑢 )
20 simprr1 ⊢ ( ( ( 𝑗 ∈ Locally Locally 𝐴 ∧ 𝑥 ∈ 𝑗 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑢 ∈ 𝑗 ∧ ( 𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ Locally 𝐴 ) ) ) → 𝑢 ⊆ 𝑥 )
21 20 adantr ⊢ ( ( ( ( 𝑗 ∈ Locally Locally 𝐴 ∧ 𝑥 ∈ 𝑗 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑢 ∈ 𝑗 ∧ ( 𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ Locally 𝐴 ) ) ) ∧ ( 𝑣 ∈ 𝑗 ∧ ( 𝑣 ⊆ 𝑢 ∧ 𝑦 ∈ 𝑣 ∧ ( ( 𝑗 ↾t 𝑢 ) ↾t 𝑣 ) ∈ 𝐴 ) ) ) → 𝑢 ⊆ 𝑥 )
22 19 21 sstrd ⊢ ( ( ( ( 𝑗 ∈ Locally Locally 𝐴 ∧ 𝑥 ∈ 𝑗 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑢 ∈ 𝑗 ∧ ( 𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ Locally 𝐴 ) ) ) ∧ ( 𝑣 ∈ 𝑗 ∧ ( 𝑣 ⊆ 𝑢 ∧ 𝑦 ∈ 𝑣 ∧ ( ( 𝑗 ↾t 𝑢 ) ↾t 𝑣 ) ∈ 𝐴 ) ) ) → 𝑣 ⊆ 𝑥 )
23 velpw ⊢ ( 𝑣 ∈ 𝒫 𝑥 ↔ 𝑣 ⊆ 𝑥 )
24 22 23 sylibr ⊢ ( ( ( ( 𝑗 ∈ Locally Locally 𝐴 ∧ 𝑥 ∈ 𝑗 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑢 ∈ 𝑗 ∧ ( 𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ Locally 𝐴 ) ) ) ∧ ( 𝑣 ∈ 𝑗 ∧ ( 𝑣 ⊆ 𝑢 ∧ 𝑦 ∈ 𝑣 ∧ ( ( 𝑗 ↾t 𝑢 ) ↾t 𝑣 ) ∈ 𝐴 ) ) ) → 𝑣 ∈ 𝒫 𝑥 )
25 18 24 elind ⊢ ( ( ( ( 𝑗 ∈ Locally Locally 𝐴 ∧ 𝑥 ∈ 𝑗 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑢 ∈ 𝑗 ∧ ( 𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ Locally 𝐴 ) ) ) ∧ ( 𝑣 ∈ 𝑗 ∧ ( 𝑣 ⊆ 𝑢 ∧ 𝑦 ∈ 𝑣 ∧ ( ( 𝑗 ↾t 𝑢 ) ↾t 𝑣 ) ∈ 𝐴 ) ) ) → 𝑣 ∈ ( 𝑗 ∩ 𝒫 𝑥 ) )
26 simprr2 ⊢ ( ( ( ( 𝑗 ∈ Locally Locally 𝐴 ∧ 𝑥 ∈ 𝑗 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑢 ∈ 𝑗 ∧ ( 𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ Locally 𝐴 ) ) ) ∧ ( 𝑣 ∈ 𝑗 ∧ ( 𝑣 ⊆ 𝑢 ∧ 𝑦 ∈ 𝑣 ∧ ( ( 𝑗 ↾t 𝑢 ) ↾t 𝑣 ) ∈ 𝐴 ) ) ) → 𝑦 ∈ 𝑣 )
27 7 adantr ⊢ ( ( ( ( 𝑗 ∈ Locally Locally 𝐴 ∧ 𝑥 ∈ 𝑗 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑢 ∈ 𝑗 ∧ ( 𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ Locally 𝐴 ) ) ) ∧ ( 𝑣 ∈ 𝑗 ∧ ( 𝑣 ⊆ 𝑢 ∧ 𝑦 ∈ 𝑣 ∧ ( ( 𝑗 ↾t 𝑢 ) ↾t 𝑣 ) ∈ 𝐴 ) ) ) → 𝑗 ∈ Top )
28 simplrl ⊢ ( ( ( ( 𝑗 ∈ Locally Locally 𝐴 ∧ 𝑥 ∈ 𝑗 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑢 ∈ 𝑗 ∧ ( 𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ Locally 𝐴 ) ) ) ∧ ( 𝑣 ∈ 𝑗 ∧ ( 𝑣 ⊆ 𝑢 ∧ 𝑦 ∈ 𝑣 ∧ ( ( 𝑗 ↾t 𝑢 ) ↾t 𝑣 ) ∈ 𝐴 ) ) ) → 𝑢 ∈ 𝑗 )
29 restabs ⊢ ( ( 𝑗 ∈ Top ∧ 𝑣 ⊆ 𝑢 ∧ 𝑢 ∈ 𝑗 ) → ( ( 𝑗 ↾t 𝑢 ) ↾t 𝑣 ) = ( 𝑗 ↾t 𝑣 ) )
30 27 19 28 29 syl3anc ⊢ ( ( ( ( 𝑗 ∈ Locally Locally 𝐴 ∧ 𝑥 ∈ 𝑗 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑢 ∈ 𝑗 ∧ ( 𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ Locally 𝐴 ) ) ) ∧ ( 𝑣 ∈ 𝑗 ∧ ( 𝑣 ⊆ 𝑢 ∧ 𝑦 ∈ 𝑣 ∧ ( ( 𝑗 ↾t 𝑢 ) ↾t 𝑣 ) ∈ 𝐴 ) ) ) → ( ( 𝑗 ↾t 𝑢 ) ↾t 𝑣 ) = ( 𝑗 ↾t 𝑣 ) )
31 simprr3 ⊢ ( ( ( ( 𝑗 ∈ Locally Locally 𝐴 ∧ 𝑥 ∈ 𝑗 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑢 ∈ 𝑗 ∧ ( 𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ Locally 𝐴 ) ) ) ∧ ( 𝑣 ∈ 𝑗 ∧ ( 𝑣 ⊆ 𝑢 ∧ 𝑦 ∈ 𝑣 ∧ ( ( 𝑗 ↾t 𝑢 ) ↾t 𝑣 ) ∈ 𝐴 ) ) ) → ( ( 𝑗 ↾t 𝑢 ) ↾t 𝑣 ) ∈ 𝐴 )
32 30 31 eqeltrrd ⊢ ( ( ( ( 𝑗 ∈ Locally Locally 𝐴 ∧ 𝑥 ∈ 𝑗 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑢 ∈ 𝑗 ∧ ( 𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ Locally 𝐴 ) ) ) ∧ ( 𝑣 ∈ 𝑗 ∧ ( 𝑣 ⊆ 𝑢 ∧ 𝑦 ∈ 𝑣 ∧ ( ( 𝑗 ↾t 𝑢 ) ↾t 𝑣 ) ∈ 𝐴 ) ) ) → ( 𝑗 ↾t 𝑣 ) ∈ 𝐴 )
33 25 26 32 jca32 ⊢ ( ( ( ( 𝑗 ∈ Locally Locally 𝐴 ∧ 𝑥 ∈ 𝑗 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑢 ∈ 𝑗 ∧ ( 𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ Locally 𝐴 ) ) ) ∧ ( 𝑣 ∈ 𝑗 ∧ ( 𝑣 ⊆ 𝑢 ∧ 𝑦 ∈ 𝑣 ∧ ( ( 𝑗 ↾t 𝑢 ) ↾t 𝑣 ) ∈ 𝐴 ) ) ) → ( 𝑣 ∈ ( 𝑗 ∩ 𝒫 𝑥 ) ∧ ( 𝑦 ∈ 𝑣 ∧ ( 𝑗 ↾t 𝑣 ) ∈ 𝐴 ) ) )
34 33 ex ⊢ ( ( ( 𝑗 ∈ Locally Locally 𝐴 ∧ 𝑥 ∈ 𝑗 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑢 ∈ 𝑗 ∧ ( 𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ Locally 𝐴 ) ) ) → ( ( 𝑣 ∈ 𝑗 ∧ ( 𝑣 ⊆ 𝑢 ∧ 𝑦 ∈ 𝑣 ∧ ( ( 𝑗 ↾t 𝑢 ) ↾t 𝑣 ) ∈ 𝐴 ) ) → ( 𝑣 ∈ ( 𝑗 ∩ 𝒫 𝑥 ) ∧ ( 𝑦 ∈ 𝑣 ∧ ( 𝑗 ↾t 𝑣 ) ∈ 𝐴 ) ) ) )
35 17 34 syland ⊢ ( ( ( 𝑗 ∈ Locally Locally 𝐴 ∧ 𝑥 ∈ 𝑗 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑢 ∈ 𝑗 ∧ ( 𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ Locally 𝐴 ) ) ) → ( ( 𝑣 ∈ ( 𝑗 ↾t 𝑢 ) ∧ ( 𝑣 ⊆ 𝑢 ∧ 𝑦 ∈ 𝑣 ∧ ( ( 𝑗 ↾t 𝑢 ) ↾t 𝑣 ) ∈ 𝐴 ) ) → ( 𝑣 ∈ ( 𝑗 ∩ 𝒫 𝑥 ) ∧ ( 𝑦 ∈ 𝑣 ∧ ( 𝑗 ↾t 𝑣 ) ∈ 𝐴 ) ) ) )
36 35 reximdv2 ⊢ ( ( ( 𝑗 ∈ Locally Locally 𝐴 ∧ 𝑥 ∈ 𝑗 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑢 ∈ 𝑗 ∧ ( 𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ Locally 𝐴 ) ) ) → ( ∃ 𝑣 ∈ ( 𝑗 ↾t 𝑢 ) ( 𝑣 ⊆ 𝑢 ∧ 𝑦 ∈ 𝑣 ∧ ( ( 𝑗 ↾t 𝑢 ) ↾t 𝑣 ) ∈ 𝐴 ) → ∃ 𝑣 ∈ ( 𝑗 ∩ 𝒫 𝑥 ) ( 𝑦 ∈ 𝑣 ∧ ( 𝑗 ↾t 𝑣 ) ∈ 𝐴 ) ) )
37 13 36 mpd ⊢ ( ( ( 𝑗 ∈ Locally Locally 𝐴 ∧ 𝑥 ∈ 𝑗 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑢 ∈ 𝑗 ∧ ( 𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ Locally 𝐴 ) ) ) → ∃ 𝑣 ∈ ( 𝑗 ∩ 𝒫 𝑥 ) ( 𝑦 ∈ 𝑣 ∧ ( 𝑗 ↾t 𝑣 ) ∈ 𝐴 ) )
38 2 37 rexlimddv ⊢ ( ( 𝑗 ∈ Locally Locally 𝐴 ∧ 𝑥 ∈ 𝑗 ∧ 𝑦 ∈ 𝑥 ) → ∃ 𝑣 ∈ ( 𝑗 ∩ 𝒫 𝑥 ) ( 𝑦 ∈ 𝑣 ∧ ( 𝑗 ↾t 𝑣 ) ∈ 𝐴 ) )
39 38 3expb ⊢ ( ( 𝑗 ∈ Locally Locally 𝐴 ∧ ( 𝑥 ∈ 𝑗 ∧ 𝑦 ∈ 𝑥 ) ) → ∃ 𝑣 ∈ ( 𝑗 ∩ 𝒫 𝑥 ) ( 𝑦 ∈ 𝑣 ∧ ( 𝑗 ↾t 𝑣 ) ∈ 𝐴 ) )
40 39 ralrimivva ⊢ ( 𝑗 ∈ Locally Locally 𝐴 → ∀ 𝑥 ∈ 𝑗 ∀ 𝑦 ∈ 𝑥 ∃ 𝑣 ∈ ( 𝑗 ∩ 𝒫 𝑥 ) ( 𝑦 ∈ 𝑣 ∧ ( 𝑗 ↾t 𝑣 ) ∈ 𝐴 ) )
41 islly ⊢ ( 𝑗 ∈ Locally 𝐴 ↔ ( 𝑗 ∈ Top ∧ ∀ 𝑥 ∈ 𝑗 ∀ 𝑦 ∈ 𝑥 ∃ 𝑣 ∈ ( 𝑗 ∩ 𝒫 𝑥 ) ( 𝑦 ∈ 𝑣 ∧ ( 𝑗 ↾t 𝑣 ) ∈ 𝐴 ) ) )
42 1 40 41 sylanbrc ⊢ ( 𝑗 ∈ Locally Locally 𝐴 → 𝑗 ∈ Locally 𝐴 )
43 42 ssriv ⊢ Locally Locally 𝐴 ⊆ Locally 𝐴
44 llyrest ⊢ ( ( 𝑗 ∈ Locally 𝐴 ∧ 𝑥 ∈ 𝑗 ) → ( 𝑗 ↾t 𝑥 ) ∈ Locally 𝐴 )
45 44 adantl ⊢ ( ( ⊤ ∧ ( 𝑗 ∈ Locally 𝐴 ∧ 𝑥 ∈ 𝑗 ) ) → ( 𝑗 ↾t 𝑥 ) ∈ Locally 𝐴 )
46 llytop ⊢ ( 𝑗 ∈ Locally 𝐴 → 𝑗 ∈ Top )
47 46 ssriv ⊢ Locally 𝐴 ⊆ Top
48 47 a1i ⊢ ( ⊤ → Locally 𝐴 ⊆ Top )
49 45 48 restlly ⊢ ( ⊤ → Locally 𝐴 ⊆ Locally Locally 𝐴 )
50 49 mptru ⊢ Locally 𝐴 ⊆ Locally Locally 𝐴
51 43 50 eqssi ⊢ Locally Locally 𝐴 = Locally 𝐴