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

Metamath Proof Explorer

Theorem f1o2sn

Description: A singleton consisting in a nested ordered pair is a one-to-one function from the cartesian product of two singletons onto a singleton (case where the two singletons are equal). (Contributed by AV, 15-Aug-2019)

Ref Expression
Assertion f1o2sn ( ( 𝐸 ∈ 𝑉 ∧ 𝑋 ∈ 𝑊 ) → { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , 𝑋 ⟩ } : ( { 𝐸 } × { 𝐸 } ) –1-1-onto→ { 𝑋 } )

Proof

Step Hyp Ref Expression
1 opex ⊢ ⟨ 𝐸 , 𝐸 ⟩ ∈ V
2 simpr ⊢ ( ( 𝐸 ∈ 𝑉 ∧ 𝑋 ∈ 𝑊 ) → 𝑋 ∈ 𝑊 )
3 f1osng ⊢ ( ( ⟨ 𝐸 , 𝐸 ⟩ ∈ V ∧ 𝑋 ∈ 𝑊 ) → { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , 𝑋 ⟩ } : { ⟨ 𝐸 , 𝐸 ⟩ } –1-1-onto→ { 𝑋 } )
4 1 2 3 sylancr ⊢ ( ( 𝐸 ∈ 𝑉 ∧ 𝑋 ∈ 𝑊 ) → { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , 𝑋 ⟩ } : { ⟨ 𝐸 , 𝐸 ⟩ } –1-1-onto→ { 𝑋 } )
5 xpsng ⊢ ( ( 𝐸 ∈ 𝑉 ∧ 𝐸 ∈ 𝑉 ) → ( { 𝐸 } × { 𝐸 } ) = { ⟨ 𝐸 , 𝐸 ⟩ } )
6 5 anidms ⊢ ( 𝐸 ∈ 𝑉 → ( { 𝐸 } × { 𝐸 } ) = { ⟨ 𝐸 , 𝐸 ⟩ } )
7 6 eqcomd ⊢ ( 𝐸 ∈ 𝑉 → { ⟨ 𝐸 , 𝐸 ⟩ } = ( { 𝐸 } × { 𝐸 } ) )
8 7 adantr ⊢ ( ( 𝐸 ∈ 𝑉 ∧ 𝑋 ∈ 𝑊 ) → { ⟨ 𝐸 , 𝐸 ⟩ } = ( { 𝐸 } × { 𝐸 } ) )
9 8 f1oeq2d ⊢ ( ( 𝐸 ∈ 𝑉 ∧ 𝑋 ∈ 𝑊 ) → ( { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , 𝑋 ⟩ } : { ⟨ 𝐸 , 𝐸 ⟩ } –1-1-onto→ { 𝑋 } ↔ { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , 𝑋 ⟩ } : ( { 𝐸 } × { 𝐸 } ) –1-1-onto→ { 𝑋 } ) )
10 4 9 mpbid ⊢ ( ( 𝐸 ∈ 𝑉 ∧ 𝑋 ∈ 𝑊 ) → { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , 𝑋 ⟩ } : ( { 𝐸 } × { 𝐸 } ) –1-1-onto→ { 𝑋 } )