Metamath Proof Explorer


Theorem ustelimasn

Description: Any point A is near enough to itself. (Contributed by Thierry Arnoux, 18-Nov-2017)

Ref Expression
Assertion ustelimasn ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉𝑈𝐴𝑋 ) → 𝐴 ∈ ( 𝑉 “ { 𝐴 } ) )

Proof

Step Hyp Ref Expression
1 simp3 ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉𝑈𝐴𝑋 ) → 𝐴𝑋 )
2 ustdiag ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉𝑈 ) → ( I ↾ 𝑋 ) ⊆ 𝑉 )
3 2 3adant3 ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉𝑈𝐴𝑋 ) → ( I ↾ 𝑋 ) ⊆ 𝑉 )
4 opelidres ( 𝐴𝑋 → ( ⟨ 𝐴 , 𝐴 ⟩ ∈ ( I ↾ 𝑋 ) ↔ 𝐴𝑋 ) )
5 4 ibir ( 𝐴𝑋 → ⟨ 𝐴 , 𝐴 ⟩ ∈ ( I ↾ 𝑋 ) )
6 5 3ad2ant3 ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉𝑈𝐴𝑋 ) → ⟨ 𝐴 , 𝐴 ⟩ ∈ ( I ↾ 𝑋 ) )
7 3 6 sseldd ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉𝑈𝐴𝑋 ) → ⟨ 𝐴 , 𝐴 ⟩ ∈ 𝑉 )
8 elimasng ( ( 𝐴𝑋𝐴𝑋 ) → ( 𝐴 ∈ ( 𝑉 “ { 𝐴 } ) ↔ ⟨ 𝐴 , 𝐴 ⟩ ∈ 𝑉 ) )
9 8 anidms ( 𝐴𝑋 → ( 𝐴 ∈ ( 𝑉 “ { 𝐴 } ) ↔ ⟨ 𝐴 , 𝐴 ⟩ ∈ 𝑉 ) )
10 9 biimpar ( ( 𝐴𝑋 ∧ ⟨ 𝐴 , 𝐴 ⟩ ∈ 𝑉 ) → 𝐴 ∈ ( 𝑉 “ { 𝐴 } ) )
11 1 7 10 syl2anc ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉𝑈𝐴𝑋 ) → 𝐴 ∈ ( 𝑉 “ { 𝐴 } ) )