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