Theorem mapsnf1o

Description: A bijection between a set and single-point functions to it. (Contributed by Stefan O'Rear, 24-Jan-2015)

	Ref	Expression
Hypothesis	ixpsnf1o.f	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ ( { 𝐼 } × { 𝑥 } ) )
Assertion	mapsnf1o	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → 𝐹 : 𝐴 –1-1-onto→ ( 𝐴 ↑m { 𝐼 } ) )

Proof

Step	Hyp	Ref	Expression
1		ixpsnf1o.f	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ ( { 𝐼 } × { 𝑥 } ) )
2	1	ixpsnf1o	⊢ ( 𝐼 ∈ 𝑊 → 𝐹 : 𝐴 –1-1-onto→ X 𝑦 ∈ { 𝐼 } 𝐴 )
3	2	adantl	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → 𝐹 : 𝐴 –1-1-onto→ X 𝑦 ∈ { 𝐼 } 𝐴 )
4		snex	⊢ { 𝐼 } ∈ V
5		ixpconstg	⊢ ( ( { 𝐼 } ∈ V ∧ 𝐴 ∈ 𝑉 ) → X 𝑦 ∈ { 𝐼 } 𝐴 = ( 𝐴 ↑m { 𝐼 } ) )
6	5	eqcomd	⊢ ( ( { 𝐼 } ∈ V ∧ 𝐴 ∈ 𝑉 ) → ( 𝐴 ↑m { 𝐼 } ) = X 𝑦 ∈ { 𝐼 } 𝐴 )
7	4 6	mpan	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ↑m { 𝐼 } ) = X 𝑦 ∈ { 𝐼 } 𝐴 )
8	7	adantr	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → ( 𝐴 ↑m { 𝐼 } ) = X 𝑦 ∈ { 𝐼 } 𝐴 )
9	8	f1oeq3d	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → ( 𝐹 : 𝐴 –1-1-onto→ ( 𝐴 ↑m { 𝐼 } ) ↔ 𝐹 : 𝐴 –1-1-onto→ X 𝑦 ∈ { 𝐼 } 𝐴 ) )
10	3 9	mpbird	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → 𝐹 : 𝐴 –1-1-onto→ ( 𝐴 ↑m { 𝐼 } ) )