dffrege115

Description: If from the circumstance that c is a result of an application of the procedure R to b , whatever b may be, it can be inferred that every result of an application of the procedure R to b is the same as c , then we say : "The procedure R is single-valued". Definition 115 of Frege1879 p. 77. (Contributed by RP, 7-Jul-2020)

		Ref	Expression
	Assertion	dffrege115	$⊢ \forall c \forall b (b R c \to \forall a (b R a \to a = c)) \leftrightarrow Fun {R^{-1}}^{-1}$

Proof

Step	Hyp	Ref	Expression
1		alcom	$⊢ \forall c \forall b (b R c \to \forall a (b R a \to a = c)) \leftrightarrow \forall b \forall c (b R c \to \forall a (b R a \to a = c))$
2		19.21v	$⊢ \forall a (b R c \to (b R a \to a = c)) \leftrightarrow (b R c \to \forall a (b R a \to a = c))$
3		impexp	$⊢ ((b R c \land b R a) \to a = c) \leftrightarrow (b R c \to (b R a \to a = c))$
4		vex	$⊢ b \in V$
5		vex	$⊢ c \in V$
6	4 5	brcnv	$⊢ b {R^{-1}}^{-1} c \leftrightarrow c R^{-1} b$
7		df-br	$⊢ b {R^{-1}}^{-1} c \leftrightarrow ⟨b, c⟩ \in {R^{-1}}^{-1}$
8	5 4	brcnv	$⊢ c R^{-1} b \leftrightarrow b R c$
9	6 7 8	3bitr3ri	$⊢ b R c \leftrightarrow ⟨b, c⟩ \in {R^{-1}}^{-1}$
10		vex	$⊢ a \in V$
11	4 10	brcnv	$⊢ b {R^{-1}}^{-1} a \leftrightarrow a R^{-1} b$
12		df-br	$⊢ b {R^{-1}}^{-1} a \leftrightarrow ⟨b, a⟩ \in {R^{-1}}^{-1}$
13	10 4	brcnv	$⊢ a R^{-1} b \leftrightarrow b R a$
14	11 12 13	3bitr3ri	$⊢ b R a \leftrightarrow ⟨b, a⟩ \in {R^{-1}}^{-1}$
15	9 14	anbi12ci	$⊢ (b R c \land b R a) \leftrightarrow (⟨b, a⟩ \in {R^{-1}}^{-1} \land ⟨b, c⟩ \in {R^{-1}}^{-1})$
16	15	imbi1i	$⊢ ((b R c \land b R a) \to a = c) \leftrightarrow ((⟨b, a⟩ \in {R^{-1}}^{-1} \land ⟨b, c⟩ \in {R^{-1}}^{-1}) \to a = c)$
17	3 16	bitr3i	$⊢ (b R c \to (b R a \to a = c)) \leftrightarrow ((⟨b, a⟩ \in {R^{-1}}^{-1} \land ⟨b, c⟩ \in {R^{-1}}^{-1}) \to a = c)$
18	17	albii	$⊢ \forall a (b R c \to (b R a \to a = c)) \leftrightarrow \forall a ((⟨b, a⟩ \in {R^{-1}}^{-1} \land ⟨b, c⟩ \in {R^{-1}}^{-1}) \to a = c)$
19	2 18	bitr3i	$⊢ (b R c \to \forall a (b R a \to a = c)) \leftrightarrow \forall a ((⟨b, a⟩ \in {R^{-1}}^{-1} \land ⟨b, c⟩ \in {R^{-1}}^{-1}) \to a = c)$
20	19	albii	$⊢ \forall c (b R c \to \forall a (b R a \to a = c)) \leftrightarrow \forall c \forall a ((⟨b, a⟩ \in {R^{-1}}^{-1} \land ⟨b, c⟩ \in {R^{-1}}^{-1}) \to a = c)$
21		alcom	$⊢ \forall c \forall a ((⟨b, a⟩ \in {R^{-1}}^{-1} \land ⟨b, c⟩ \in {R^{-1}}^{-1}) \to a = c) \leftrightarrow \forall a \forall c ((⟨b, a⟩ \in {R^{-1}}^{-1} \land ⟨b, c⟩ \in {R^{-1}}^{-1}) \to a = c)$
22	20 21	bitri	$⊢ \forall c (b R c \to \forall a (b R a \to a = c)) \leftrightarrow \forall a \forall c ((⟨b, a⟩ \in {R^{-1}}^{-1} \land ⟨b, c⟩ \in {R^{-1}}^{-1}) \to a = c)$
23		opeq2	$⊢ a = c \to ⟨b, a⟩ = ⟨b, c⟩$
24	23	eleq1d	$⊢ a = c \to (⟨b, a⟩ \in {R^{-1}}^{-1} \leftrightarrow ⟨b, c⟩ \in {R^{-1}}^{-1})$
25	24	mo4	$⊢ \exists^{*} a ⟨b, a⟩ \in {R^{-1}}^{-1} \leftrightarrow \forall a \forall c ((⟨b, a⟩ \in {R^{-1}}^{-1} \land ⟨b, c⟩ \in {R^{-1}}^{-1}) \to a = c)$
26		dfmo	$⊢ \exists^{*} a ⟨b, a⟩ \in {R^{-1}}^{-1} \leftrightarrow \exists c \forall a (⟨b, a⟩ \in {R^{-1}}^{-1} \to a = c)$
27	22 25 26	3bitr2i	$⊢ \forall c (b R c \to \forall a (b R a \to a = c)) \leftrightarrow \exists c \forall a (⟨b, a⟩ \in {R^{-1}}^{-1} \to a = c)$
28	27	albii	$⊢ \forall b \forall c (b R c \to \forall a (b R a \to a = c)) \leftrightarrow \forall b \exists c \forall a (⟨b, a⟩ \in {R^{-1}}^{-1} \to a = c)$
29		relcnv	$⊢ Rel {R^{-1}}^{-1}$
30	29	biantrur	$⊢ \forall b \exists c \forall a (⟨b, a⟩ \in {R^{-1}}^{-1} \to a = c) \leftrightarrow (Rel {R^{-1}}^{-1} \land \forall b \exists c \forall a (⟨b, a⟩ \in {R^{-1}}^{-1} \to a = c))$
31		dffun5	$⊢ Fun {R^{-1}}^{-1} \leftrightarrow (Rel {R^{-1}}^{-1} \land \forall b \exists c \forall a (⟨b, a⟩ \in {R^{-1}}^{-1} \to a = c))$
32	30 31	bitr4i	$⊢ \forall b \exists c \forall a (⟨b, a⟩ \in {R^{-1}}^{-1} \to a = c) \leftrightarrow Fun {R^{-1}}^{-1}$
33	1 28 32	3bitri	$⊢ \forall c \forall b (b R c \to \forall a (b R a \to a = c)) \leftrightarrow Fun {R^{-1}}^{-1}$

Metamath Proof Explorer

Theorem dffrege115

Proof