Theorem sgnsf

Description: The sign function. (Contributed by Thierry Arnoux, 9-Sep-2018)

	Ref	Expression
Hypotheses	sgnsval.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	sgnsval.0	⊢ 0 = ( 0g ‘ 𝑅 )
	sgnsval.l	⊢ < = ( lt ‘ 𝑅 )
	sgnsval.s	⊢ 𝑆 = ( sgns ‘ 𝑅 )
Assertion	sgnsf	⊢ ( 𝑅 ∈ 𝑉 → 𝑆 : 𝐵 ⟶ { - 1 , 0 , 1 } )

Proof

Step	Hyp	Ref	Expression
1		sgnsval.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		sgnsval.0	⊢ 0 = ( 0g ‘ 𝑅 )
3		sgnsval.l	⊢ < = ( lt ‘ 𝑅 )
4		sgnsval.s	⊢ 𝑆 = ( sgns ‘ 𝑅 )
5	1 2 3 4	sgnsv	⊢ ( 𝑅 ∈ 𝑉 → 𝑆 = ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 = 0 , 0 , if ( 0 < 𝑥 , 1 , - 1 ) ) ) )
6		c0ex	⊢ 0 ∈ V
7	6	tpid2	⊢ 0 ∈ { - 1 , 0 , 1 }
8		1ex	⊢ 1 ∈ V
9	8	tpid3	⊢ 1 ∈ { - 1 , 0 , 1 }
10		negex	⊢ - 1 ∈ V
11	10	tpid1	⊢ - 1 ∈ { - 1 , 0 , 1 }
12	9 11	ifcli	⊢ if ( 0 < 𝑥 , 1 , - 1 ) ∈ { - 1 , 0 , 1 }
13	7 12	ifcli	⊢ if ( 𝑥 = 0 , 0 , if ( 0 < 𝑥 , 1 , - 1 ) ) ∈ { - 1 , 0 , 1 }
14	13	a1i	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑥 ∈ 𝐵 ) → if ( 𝑥 = 0 , 0 , if ( 0 < 𝑥 , 1 , - 1 ) ) ∈ { - 1 , 0 , 1 } )
15	5 14	fmpt3d	⊢ ( 𝑅 ∈ 𝑉 → 𝑆 : 𝐵 ⟶ { - 1 , 0 , 1 } )