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

Metamath Proof Explorer

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 ⊢ ( ( 𝑉 ⊆ ( 𝑋 × 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑉 “ { 𝐴 } ) × ( 𝑉 “ { 𝐴 } ) ) ⊆ ( 𝑉 ∘ ◡ 𝑉 ) )