fconst5

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

		Ref	Expression
	Assertion	fconst5	$⊢ (F Fn A \land A \neq \emptyset) \to (F = A \times \{B\} \leftrightarrow ran F = \{B\})$

Proof

Step	Hyp	Ref	Expression
1		rneq	$⊢ F = A \times \{B\} \to ran F = ran (A \times \{B\})$
2		rnxp	$⊢ A \neq \emptyset \to ran (A \times \{B\}) = \{B\}$
3	2	eqeq2d	$⊢ A \neq \emptyset \to (ran F = ran (A \times \{B\}) \leftrightarrow ran F = \{B\})$
4	1 3	imbitrid	$⊢ A \neq \emptyset \to (F = A \times \{B\} \to ran F = \{B\})$
5	4	adantl	$⊢ (F Fn A \land A \neq \emptyset) \to (F = A \times \{B\} \to ran F = \{B\})$
6		df-fo	$⊢ F : A \underset{onto}{⟶} \{B\} \leftrightarrow (F Fn A \land ran F = \{B\})$
7		fof	$⊢ F : A \underset{onto}{⟶} \{B\} \to F : A ⟶ \{B\}$
8	6 7	sylbir	$⊢ (F Fn A \land ran F = \{B\}) \to F : A ⟶ \{B\}$
9		fconst2g	$⊢ B \in V \to (F : A ⟶ \{B\} \leftrightarrow F = A \times \{B\})$
10	8 9	imbitrid	$⊢ B \in V \to ((F Fn A \land ran F = \{B\}) \to F = A \times \{B\})$
11	10	expd	$⊢ B \in V \to (F Fn A \to (ran F = \{B\} \to F = A \times \{B\}))$
12	11	adantrd	$⊢ B \in V \to ((F Fn A \land A \neq \emptyset) \to (ran F = \{B\} \to F = A \times \{B\}))$
13		fnrel	$⊢ F Fn A \to Rel F$
14		snprc	$⊢ \neg B \in V \leftrightarrow \{B\} = \emptyset$
15		relrn0	$⊢ Rel F \to (F = \emptyset \leftrightarrow ran F = \emptyset)$
16	15	biimprd	$⊢ Rel F \to (ran F = \emptyset \to F = \emptyset)$
17	16	adantl	$⊢ (\{B\} = \emptyset \land Rel F) \to (ran F = \emptyset \to F = \emptyset)$
18		eqeq2	$⊢ \{B\} = \emptyset \to (ran F = \{B\} \leftrightarrow ran F = \emptyset)$
19	18	adantr	$⊢ (\{B\} = \emptyset \land Rel F) \to (ran F = \{B\} \leftrightarrow ran F = \emptyset)$
20		xpeq2	$⊢ \{B\} = \emptyset \to A \times \{B\} = A \times \emptyset$
21		xp0	$⊢ A \times \emptyset = \emptyset$
22	20 21	eqtrdi	$⊢ \{B\} = \emptyset \to A \times \{B\} = \emptyset$
23	22	eqeq2d	$⊢ \{B\} = \emptyset \to (F = A \times \{B\} \leftrightarrow F = \emptyset)$
24	23	adantr	$⊢ (\{B\} = \emptyset \land Rel F) \to (F = A \times \{B\} \leftrightarrow F = \emptyset)$
25	17 19 24	3imtr4d	$⊢ (\{B\} = \emptyset \land Rel F) \to (ran F = \{B\} \to F = A \times \{B\})$
26	25	ex	$⊢ \{B\} = \emptyset \to (Rel F \to (ran F = \{B\} \to F = A \times \{B\}))$
27	14 26	sylbi	$⊢ \neg B \in V \to (Rel F \to (ran F = \{B\} \to F = A \times \{B\}))$
28	13 27	syl5	$⊢ \neg B \in V \to (F Fn A \to (ran F = \{B\} \to F = A \times \{B\}))$
29	28	adantrd	$⊢ \neg B \in V \to ((F Fn A \land A \neq \emptyset) \to (ran F = \{B\} \to F = A \times \{B\}))$
30	12 29	pm2.61i	$⊢ (F Fn A \land A \neq \emptyset) \to (ran F = \{B\} \to F = A \times \{B\})$
31	5 30	impbid	$⊢ (F Fn A \land A \neq \emptyset) \to (F = A \times \{B\} \leftrightarrow ran F = \{B\})$

Metamath Proof Explorer

Theorem fconst5

Proof