Theorem mapsnop

Description: A singleton of an ordered pair as an element of the mapping operation. (Contributed by AV, 12-Apr-2019)

	Ref	Expression
Hypothesis	mapsnop.f	⊢ 𝐹 = { ⟨ 𝑋 , 𝑌 ⟩ }
Assertion	mapsnop	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑅 ∧ 𝑅 ∈ 𝑊 ) → 𝐹 ∈ ( 𝑅 ↑m { 𝑋 } ) )

Proof

Step	Hyp	Ref	Expression
1		mapsnop.f	⊢ 𝐹 = { ⟨ 𝑋 , 𝑌 ⟩ }
2		fsng	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑅 ) → ( 𝐹 : { 𝑋 } ⟶ { 𝑌 } ↔ 𝐹 = { ⟨ 𝑋 , 𝑌 ⟩ } ) )
3	2	3adant3	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑅 ∧ 𝑅 ∈ 𝑊 ) → ( 𝐹 : { 𝑋 } ⟶ { 𝑌 } ↔ 𝐹 = { ⟨ 𝑋 , 𝑌 ⟩ } ) )
4	1 3	mpbiri	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑅 ∧ 𝑅 ∈ 𝑊 ) → 𝐹 : { 𝑋 } ⟶ { 𝑌 } )
5		snssi	⊢ ( 𝑌 ∈ 𝑅 → { 𝑌 } ⊆ 𝑅 )
6	5	3ad2ant2	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑅 ∧ 𝑅 ∈ 𝑊 ) → { 𝑌 } ⊆ 𝑅 )
7	4 6	fssd	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑅 ∧ 𝑅 ∈ 𝑊 ) → 𝐹 : { 𝑋 } ⟶ 𝑅 )
8		simp3	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑅 ∧ 𝑅 ∈ 𝑊 ) → 𝑅 ∈ 𝑊 )
9		snex	⊢ { 𝑋 } ∈ V
10		elmapg	⊢ ( ( 𝑅 ∈ 𝑊 ∧ { 𝑋 } ∈ V ) → ( 𝐹 ∈ ( 𝑅 ↑m { 𝑋 } ) ↔ 𝐹 : { 𝑋 } ⟶ 𝑅 ) )
11	8 9 10	sylancl	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑅 ∧ 𝑅 ∈ 𝑊 ) → ( 𝐹 ∈ ( 𝑅 ↑m { 𝑋 } ) ↔ 𝐹 : { 𝑋 } ⟶ 𝑅 ) )
12	7 11	mpbird	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑅 ∧ 𝑅 ∈ 𝑊 ) → 𝐹 ∈ ( 𝑅 ↑m { 𝑋 } ) )