Theorem ustneism

Description: For a point A in X , ( V " { A } ) is small enough in ( V o.`' V ) ` . This proposition actually does not require any axiom of the definition of uniform structures. (Contributed by Thierry Arnoux, 18-Nov-2017)

	Ref	Expression
Assertion	ustneism	⊢ ( ( 𝑉 ⊆ ( 𝑋 × 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑉 “ { 𝐴 } ) × ( 𝑉 “ { 𝐴 } ) ) ⊆ ( 𝑉 ∘ ◡ 𝑉 ) )

Proof

Step	Hyp	Ref	Expression
1		snnzg	⊢ ( 𝐴 ∈ 𝑋 → { 𝐴 } ≠ ∅ )
2	1	adantl	⊢ ( ( 𝑉 ⊆ ( 𝑋 × 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) → { 𝐴 } ≠ ∅ )
3		xpco	⊢ ( { 𝐴 } ≠ ∅ → ( ( { 𝐴 } × ( 𝑉 “ { 𝐴 } ) ) ∘ ( ( 𝑉 “ { 𝐴 } ) × { 𝐴 } ) ) = ( ( 𝑉 “ { 𝐴 } ) × ( 𝑉 “ { 𝐴 } ) ) )
4	2 3	syl	⊢ ( ( 𝑉 ⊆ ( 𝑋 × 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) → ( ( { 𝐴 } × ( 𝑉 “ { 𝐴 } ) ) ∘ ( ( 𝑉 “ { 𝐴 } ) × { 𝐴 } ) ) = ( ( 𝑉 “ { 𝐴 } ) × ( 𝑉 “ { 𝐴 } ) ) )
5		cnvxp	⊢ ◡ ( { 𝐴 } × ( 𝑉 “ { 𝐴 } ) ) = ( ( 𝑉 “ { 𝐴 } ) × { 𝐴 } )
6		ressn	⊢ ( 𝑉 ↾ { 𝐴 } ) = ( { 𝐴 } × ( 𝑉 “ { 𝐴 } ) )
7	6	cnveqi	⊢ ◡ ( 𝑉 ↾ { 𝐴 } ) = ◡ ( { 𝐴 } × ( 𝑉 “ { 𝐴 } ) )
8		resss	⊢ ( 𝑉 ↾ { 𝐴 } ) ⊆ 𝑉
9		cnvss	⊢ ( ( 𝑉 ↾ { 𝐴 } ) ⊆ 𝑉 → ◡ ( 𝑉 ↾ { 𝐴 } ) ⊆ ◡ 𝑉 )
10	8 9	ax-mp	⊢ ◡ ( 𝑉 ↾ { 𝐴 } ) ⊆ ◡ 𝑉
11	7 10	eqsstrri	⊢ ◡ ( { 𝐴 } × ( 𝑉 “ { 𝐴 } ) ) ⊆ ◡ 𝑉
12	5 11	eqsstrri	⊢ ( ( 𝑉 “ { 𝐴 } ) × { 𝐴 } ) ⊆ ◡ 𝑉
13		coss2	⊢ ( ( ( 𝑉 “ { 𝐴 } ) × { 𝐴 } ) ⊆ ◡ 𝑉 → ( ( { 𝐴 } × ( 𝑉 “ { 𝐴 } ) ) ∘ ( ( 𝑉 “ { 𝐴 } ) × { 𝐴 } ) ) ⊆ ( ( { 𝐴 } × ( 𝑉 “ { 𝐴 } ) ) ∘ ◡ 𝑉 ) )
14	12 13	mp1i	⊢ ( ( 𝑉 ⊆ ( 𝑋 × 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) → ( ( { 𝐴 } × ( 𝑉 “ { 𝐴 } ) ) ∘ ( ( 𝑉 “ { 𝐴 } ) × { 𝐴 } ) ) ⊆ ( ( { 𝐴 } × ( 𝑉 “ { 𝐴 } ) ) ∘ ◡ 𝑉 ) )
15	6 8	eqsstrri	⊢ ( { 𝐴 } × ( 𝑉 “ { 𝐴 } ) ) ⊆ 𝑉
16		coss1	⊢ ( ( { 𝐴 } × ( 𝑉 “ { 𝐴 } ) ) ⊆ 𝑉 → ( ( { 𝐴 } × ( 𝑉 “ { 𝐴 } ) ) ∘ ◡ 𝑉 ) ⊆ ( 𝑉 ∘ ◡ 𝑉 ) )
17	15 16	mp1i	⊢ ( ( 𝑉 ⊆ ( 𝑋 × 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) → ( ( { 𝐴 } × ( 𝑉 “ { 𝐴 } ) ) ∘ ◡ 𝑉 ) ⊆ ( 𝑉 ∘ ◡ 𝑉 ) )
18	14 17	sstrd	⊢ ( ( 𝑉 ⊆ ( 𝑋 × 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) → ( ( { 𝐴 } × ( 𝑉 “ { 𝐴 } ) ) ∘ ( ( 𝑉 “ { 𝐴 } ) × { 𝐴 } ) ) ⊆ ( 𝑉 ∘ ◡ 𝑉 ) )
19	4 18	eqsstrrd	⊢ ( ( 𝑉 ⊆ ( 𝑋 × 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑉 “ { 𝐴 } ) × ( 𝑉 “ { 𝐴 } ) ) ⊆ ( 𝑉 ∘ ◡ 𝑉 ) )