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 ⊢ E ∈ V ∧ X ∈ W → E E X : E × E ⟶ 1-1 onto X

Proof

Step Hyp Ref Expression
1 opex ⊢ E E ∈ V
2 simpr ⊢ E ∈ V ∧ X ∈ W → X ∈ W
3 f1osng ⊢ E E ∈ V ∧ X ∈ W → E E X : E E ⟶ 1-1 onto X
4 1 2 3 sylancr ⊢ E ∈ V ∧ X ∈ W → E E X : E E ⟶ 1-1 onto X
5 xpsng ⊢ E ∈ V ∧ E ∈ V → E × E = E E
6 5 anidms ⊢ E ∈ V → E × E = E E
7 6 eqcomd ⊢ E ∈ V → E E = E × E
8 7 adantr ⊢ E ∈ V ∧ X ∈ W → E E = E × E
9 8 f1oeq2d ⊢ E ∈ V ∧ X ∈ W → E E X : E E ⟶ 1-1 onto X ↔ E E X : E × E ⟶ 1-1 onto X
10 4 9 mpbid ⊢ E ∈ V ∧ X ∈ W → E E X : E × E ⟶ 1-1 onto X