Theorem utopsnnei

Description: Images of singletons by entourages V are neighborhoods of those singletons. (Contributed by Thierry Arnoux, 13-Jan-2018)

	Ref	Expression
Hypothesis	utoptop.1	⊢ 𝐽 = ( unifTop ‘ 𝑈 )
Assertion	utopsnnei	⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉 ∈ 𝑈 ∧ 𝑃 ∈ 𝑋 ) → ( 𝑉 “ { 𝑃 } ) ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) )

Proof

Step	Hyp	Ref	Expression
1		utoptop.1	⊢ 𝐽 = ( unifTop ‘ 𝑈 )
2		eqid	⊢ ( 𝑉 “ { 𝑃 } ) = ( 𝑉 “ { 𝑃 } )
3		imaeq1	⊢ ( 𝑣 = 𝑉 → ( 𝑣 “ { 𝑃 } ) = ( 𝑉 “ { 𝑃 } ) )
4	3	rspceeqv	⊢ ( ( 𝑉 ∈ 𝑈 ∧ ( 𝑉 “ { 𝑃 } ) = ( 𝑉 “ { 𝑃 } ) ) → ∃ 𝑣 ∈ 𝑈 ( 𝑉 “ { 𝑃 } ) = ( 𝑣 “ { 𝑃 } ) )
5	2 4	mpan2	⊢ ( 𝑉 ∈ 𝑈 → ∃ 𝑣 ∈ 𝑈 ( 𝑉 “ { 𝑃 } ) = ( 𝑣 “ { 𝑃 } ) )
6	5	3ad2ant2	⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉 ∈ 𝑈 ∧ 𝑃 ∈ 𝑋 ) → ∃ 𝑣 ∈ 𝑈 ( 𝑉 “ { 𝑃 } ) = ( 𝑣 “ { 𝑃 } ) )
7	1	utopsnneip	⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) → ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) = ran ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑃 } ) ) )
8	7	3adant2	⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉 ∈ 𝑈 ∧ 𝑃 ∈ 𝑋 ) → ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) = ran ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑃 } ) ) )
9	8	eleq2d	⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉 ∈ 𝑈 ∧ 𝑃 ∈ 𝑋 ) → ( ( 𝑉 “ { 𝑃 } ) ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ↔ ( 𝑉 “ { 𝑃 } ) ∈ ran ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑃 } ) ) ) )
10		imaexg	⊢ ( 𝑉 ∈ 𝑈 → ( 𝑉 “ { 𝑃 } ) ∈ V )
11		eqid	⊢ ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑃 } ) ) = ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑃 } ) )
12	11	elrnmpt	⊢ ( ( 𝑉 “ { 𝑃 } ) ∈ V → ( ( 𝑉 “ { 𝑃 } ) ∈ ran ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑃 } ) ) ↔ ∃ 𝑣 ∈ 𝑈 ( 𝑉 “ { 𝑃 } ) = ( 𝑣 “ { 𝑃 } ) ) )
13	10 12	syl	⊢ ( 𝑉 ∈ 𝑈 → ( ( 𝑉 “ { 𝑃 } ) ∈ ran ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑃 } ) ) ↔ ∃ 𝑣 ∈ 𝑈 ( 𝑉 “ { 𝑃 } ) = ( 𝑣 “ { 𝑃 } ) ) )
14	13	3ad2ant2	⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉 ∈ 𝑈 ∧ 𝑃 ∈ 𝑋 ) → ( ( 𝑉 “ { 𝑃 } ) ∈ ran ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑃 } ) ) ↔ ∃ 𝑣 ∈ 𝑈 ( 𝑉 “ { 𝑃 } ) = ( 𝑣 “ { 𝑃 } ) ) )
15	9 14	bitrd	⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉 ∈ 𝑈 ∧ 𝑃 ∈ 𝑋 ) → ( ( 𝑉 “ { 𝑃 } ) ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ↔ ∃ 𝑣 ∈ 𝑈 ( 𝑉 “ { 𝑃 } ) = ( 𝑣 “ { 𝑃 } ) ) )
16	6 15	mpbird	⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉 ∈ 𝑈 ∧ 𝑃 ∈ 𝑋 ) → ( 𝑉 “ { 𝑃 } ) ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) )