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→ { 𝑋 } )