Theorem fconst5

Description: Two ways to express that a function is constant. (Contributed by NM, 27-Nov-2007)

	Ref	Expression
Assertion	fconst5	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐴 ≠ ∅ ) → ( 𝐹 = ( 𝐴 × { 𝐵 } ) ↔ ran 𝐹 = { 𝐵 } ) )

Proof

Step	Hyp	Ref	Expression
1		rneq	⊢ ( 𝐹 = ( 𝐴 × { 𝐵 } ) → ran 𝐹 = ran ( 𝐴 × { 𝐵 } ) )
2		rnxp	⊢ ( 𝐴 ≠ ∅ → ran ( 𝐴 × { 𝐵 } ) = { 𝐵 } )
3	2	eqeq2d	⊢ ( 𝐴 ≠ ∅ → ( ran 𝐹 = ran ( 𝐴 × { 𝐵 } ) ↔ ran 𝐹 = { 𝐵 } ) )
4	1 3	imbitrid	⊢ ( 𝐴 ≠ ∅ → ( 𝐹 = ( 𝐴 × { 𝐵 } ) → ran 𝐹 = { 𝐵 } ) )
5	4	adantl	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐴 ≠ ∅ ) → ( 𝐹 = ( 𝐴 × { 𝐵 } ) → ran 𝐹 = { 𝐵 } ) )
6		df-fo	⊢ ( 𝐹 : 𝐴 –onto→ { 𝐵 } ↔ ( 𝐹 Fn 𝐴 ∧ ran 𝐹 = { 𝐵 } ) )
7		fof	⊢ ( 𝐹 : 𝐴 –onto→ { 𝐵 } → 𝐹 : 𝐴 ⟶ { 𝐵 } )
8	6 7	sylbir	⊢ ( ( 𝐹 Fn 𝐴 ∧ ran 𝐹 = { 𝐵 } ) → 𝐹 : 𝐴 ⟶ { 𝐵 } )
9		fconst2g	⊢ ( 𝐵 ∈ V → ( 𝐹 : 𝐴 ⟶ { 𝐵 } ↔ 𝐹 = ( 𝐴 × { 𝐵 } ) ) )
10	8 9	imbitrid	⊢ ( 𝐵 ∈ V → ( ( 𝐹 Fn 𝐴 ∧ ran 𝐹 = { 𝐵 } ) → 𝐹 = ( 𝐴 × { 𝐵 } ) ) )
11	10	expd	⊢ ( 𝐵 ∈ V → ( 𝐹 Fn 𝐴 → ( ran 𝐹 = { 𝐵 } → 𝐹 = ( 𝐴 × { 𝐵 } ) ) ) )
12	11	adantrd	⊢ ( 𝐵 ∈ V → ( ( 𝐹 Fn 𝐴 ∧ 𝐴 ≠ ∅ ) → ( ran 𝐹 = { 𝐵 } → 𝐹 = ( 𝐴 × { 𝐵 } ) ) ) )
13		fnrel	⊢ ( 𝐹 Fn 𝐴 → Rel 𝐹 )
14		snprc	⊢ ( ¬ 𝐵 ∈ V ↔ { 𝐵 } = ∅ )
15		relrn0	⊢ ( Rel 𝐹 → ( 𝐹 = ∅ ↔ ran 𝐹 = ∅ ) )
16	15	biimprd	⊢ ( Rel 𝐹 → ( ran 𝐹 = ∅ → 𝐹 = ∅ ) )
17	16	adantl	⊢ ( ( { 𝐵 } = ∅ ∧ Rel 𝐹 ) → ( ran 𝐹 = ∅ → 𝐹 = ∅ ) )
18		eqeq2	⊢ ( { 𝐵 } = ∅ → ( ran 𝐹 = { 𝐵 } ↔ ran 𝐹 = ∅ ) )
19	18	adantr	⊢ ( ( { 𝐵 } = ∅ ∧ Rel 𝐹 ) → ( ran 𝐹 = { 𝐵 } ↔ ran 𝐹 = ∅ ) )
20		xpeq2	⊢ ( { 𝐵 } = ∅ → ( 𝐴 × { 𝐵 } ) = ( 𝐴 × ∅ ) )
21		xp0	⊢ ( 𝐴 × ∅ ) = ∅
22	20 21	eqtrdi	⊢ ( { 𝐵 } = ∅ → ( 𝐴 × { 𝐵 } ) = ∅ )
23	22	eqeq2d	⊢ ( { 𝐵 } = ∅ → ( 𝐹 = ( 𝐴 × { 𝐵 } ) ↔ 𝐹 = ∅ ) )
24	23	adantr	⊢ ( ( { 𝐵 } = ∅ ∧ Rel 𝐹 ) → ( 𝐹 = ( 𝐴 × { 𝐵 } ) ↔ 𝐹 = ∅ ) )
25	17 19 24	3imtr4d	⊢ ( ( { 𝐵 } = ∅ ∧ Rel 𝐹 ) → ( ran 𝐹 = { 𝐵 } → 𝐹 = ( 𝐴 × { 𝐵 } ) ) )
26	25	ex	⊢ ( { 𝐵 } = ∅ → ( Rel 𝐹 → ( ran 𝐹 = { 𝐵 } → 𝐹 = ( 𝐴 × { 𝐵 } ) ) ) )
27	14 26	sylbi	⊢ ( ¬ 𝐵 ∈ V → ( Rel 𝐹 → ( ran 𝐹 = { 𝐵 } → 𝐹 = ( 𝐴 × { 𝐵 } ) ) ) )
28	13 27	syl5	⊢ ( ¬ 𝐵 ∈ V → ( 𝐹 Fn 𝐴 → ( ran 𝐹 = { 𝐵 } → 𝐹 = ( 𝐴 × { 𝐵 } ) ) ) )
29	28	adantrd	⊢ ( ¬ 𝐵 ∈ V → ( ( 𝐹 Fn 𝐴 ∧ 𝐴 ≠ ∅ ) → ( ran 𝐹 = { 𝐵 } → 𝐹 = ( 𝐴 × { 𝐵 } ) ) ) )
30	12 29	pm2.61i	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐴 ≠ ∅ ) → ( ran 𝐹 = { 𝐵 } → 𝐹 = ( 𝐴 × { 𝐵 } ) ) )
31	5 30	impbid	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐴 ≠ ∅ ) → ( 𝐹 = ( 𝐴 × { 𝐵 } ) ↔ ran 𝐹 = { 𝐵 } ) )