Theorem llynlly

Description: A locally A space is n-locally A : the "n-locally" predicate is the weaker notion. (Contributed by Mario Carneiro, 2-Mar-2015)

	Ref	Expression
Assertion	llynlly	⊢ ( 𝐽 ∈ Locally 𝐴 → 𝐽 ∈ 𝑛-Locally 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		llytop	⊢ ( 𝐽 ∈ Locally 𝐴 → 𝐽 ∈ Top )
2		llyi	⊢ ( ( 𝐽 ∈ Locally 𝐴 ∧ 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) → ∃ 𝑢 ∈ 𝐽 ( 𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) )
3		simpl1	⊢ ( ( ( 𝐽 ∈ Locally 𝐴 ∧ 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑢 ∈ 𝐽 ∧ ( 𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) ) ) → 𝐽 ∈ Locally 𝐴 )
4	3 1	syl	⊢ ( ( ( 𝐽 ∈ Locally 𝐴 ∧ 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑢 ∈ 𝐽 ∧ ( 𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) ) ) → 𝐽 ∈ Top )
5		simprl	⊢ ( ( ( 𝐽 ∈ Locally 𝐴 ∧ 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑢 ∈ 𝐽 ∧ ( 𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) ) ) → 𝑢 ∈ 𝐽 )
6		simprr2	⊢ ( ( ( 𝐽 ∈ Locally 𝐴 ∧ 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑢 ∈ 𝐽 ∧ ( 𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) ) ) → 𝑦 ∈ 𝑢 )
7		opnneip	⊢ ( ( 𝐽 ∈ Top ∧ 𝑢 ∈ 𝐽 ∧ 𝑦 ∈ 𝑢 ) → 𝑢 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) )
8	4 5 6 7	syl3anc	⊢ ( ( ( 𝐽 ∈ Locally 𝐴 ∧ 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑢 ∈ 𝐽 ∧ ( 𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) ) ) → 𝑢 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) )
9		simprr1	⊢ ( ( ( 𝐽 ∈ Locally 𝐴 ∧ 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑢 ∈ 𝐽 ∧ ( 𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) ) ) → 𝑢 ⊆ 𝑥 )
10		velpw	⊢ ( 𝑢 ∈ 𝒫 𝑥 ↔ 𝑢 ⊆ 𝑥 )
11	9 10	sylibr	⊢ ( ( ( 𝐽 ∈ Locally 𝐴 ∧ 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑢 ∈ 𝐽 ∧ ( 𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) ) ) → 𝑢 ∈ 𝒫 𝑥 )
12	8 11	elind	⊢ ( ( ( 𝐽 ∈ Locally 𝐴 ∧ 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑢 ∈ 𝐽 ∧ ( 𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) ) ) → 𝑢 ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) )
13		simprr3	⊢ ( ( ( 𝐽 ∈ Locally 𝐴 ∧ 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑢 ∈ 𝐽 ∧ ( 𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) ) ) → ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 )
14	2 12 13	reximssdv	⊢ ( ( 𝐽 ∈ Locally 𝐴 ∧ 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) → ∃ 𝑢 ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 )
15	14	3expb	⊢ ( ( 𝐽 ∈ Locally 𝐴 ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ) → ∃ 𝑢 ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 )
16	15	ralrimivva	⊢ ( 𝐽 ∈ Locally 𝐴 → ∀ 𝑥 ∈ 𝐽 ∀ 𝑦 ∈ 𝑥 ∃ 𝑢 ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 )
17		isnlly	⊢ ( 𝐽 ∈ 𝑛-Locally 𝐴 ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑥 ∈ 𝐽 ∀ 𝑦 ∈ 𝑥 ∃ 𝑢 ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) )
18	1 16 17	sylanbrc	⊢ ( 𝐽 ∈ Locally 𝐴 → 𝐽 ∈ 𝑛-Locally 𝐴 )