Theorem rnmptcOLD

Description: Obsolete version of rnmptc as of 17-Apr-2024. (Contributed by Glauco Siliprandi, 11-Dec-2019) (New usage is discouraged.) (Proof modification is discouraged.)

	Ref	Expression
Hypotheses	rnmptcOLD.f	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
	rnmptcOLD.b	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝐶 )
	rnmptcOLD.a	⊢ ( 𝜑 → 𝐴 ≠ ∅ )
Assertion	rnmptcOLD	⊢ ( 𝜑 → ran 𝐹 = { 𝐵 } )

Proof

Step	Hyp	Ref	Expression
1		rnmptcOLD.f	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
2		rnmptcOLD.b	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝐶 )
3		rnmptcOLD.a	⊢ ( 𝜑 → 𝐴 ≠ ∅ )
4		fconstmpt	⊢ ( 𝐴 × { 𝐵 } ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
5	1 4	eqtr4i	⊢ 𝐹 = ( 𝐴 × { 𝐵 } )
6	2 1	fmptd	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐶 )
7	6	ffnd	⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
8		fconst5	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐴 ≠ ∅ ) → ( 𝐹 = ( 𝐴 × { 𝐵 } ) ↔ ran 𝐹 = { 𝐵 } ) )
9	7 3 8	syl2anc	⊢ ( 𝜑 → ( 𝐹 = ( 𝐴 × { 𝐵 } ) ↔ ran 𝐹 = { 𝐵 } ) )
10	5 9	mpbii	⊢ ( 𝜑 → ran 𝐹 = { 𝐵 } )