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

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 ‘ 𝑋 ) ∧ 𝑉 ∈ 𝑈 ∧ 𝐴 ∈ 𝑋 ) → 𝐴 ∈ ( 𝑉 “ { 𝐴 } ) )