Theorem 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	⊢ ( ∀ 𝑐 ∀ 𝑏 ( 𝑏 𝑅 𝑐 → ∀ 𝑎 ( 𝑏 𝑅 𝑎 → 𝑎 = 𝑐 ) ) ↔ Fun ◡ ◡ 𝑅 )

Proof

Step	Hyp	Ref	Expression
1		alcom	⊢ ( ∀ 𝑐 ∀ 𝑏 ( 𝑏 𝑅 𝑐 → ∀ 𝑎 ( 𝑏 𝑅 𝑎 → 𝑎 = 𝑐 ) ) ↔ ∀ 𝑏 ∀ 𝑐 ( 𝑏 𝑅 𝑐 → ∀ 𝑎 ( 𝑏 𝑅 𝑎 → 𝑎 = 𝑐 ) ) )
2		19.21v	⊢ ( ∀ 𝑎 ( 𝑏 𝑅 𝑐 → ( 𝑏 𝑅 𝑎 → 𝑎 = 𝑐 ) ) ↔ ( 𝑏 𝑅 𝑐 → ∀ 𝑎 ( 𝑏 𝑅 𝑎 → 𝑎 = 𝑐 ) ) )
3		impexp	⊢ ( ( ( 𝑏 𝑅 𝑐 ∧ 𝑏 𝑅 𝑎 ) → 𝑎 = 𝑐 ) ↔ ( 𝑏 𝑅 𝑐 → ( 𝑏 𝑅 𝑎 → 𝑎 = 𝑐 ) ) )
4		vex	⊢ 𝑏 ∈ V
5		vex	⊢ 𝑐 ∈ V
6	4 5	brcnv	⊢ ( 𝑏 ◡ ◡ 𝑅 𝑐 ↔ 𝑐 ◡ 𝑅 𝑏 )
7		df-br	⊢ ( 𝑏 ◡ ◡ 𝑅 𝑐 ↔ ⟨ 𝑏 , 𝑐 ⟩ ∈ ◡ ◡ 𝑅 )
8	5 4	brcnv	⊢ ( 𝑐 ◡ 𝑅 𝑏 ↔ 𝑏 𝑅 𝑐 )
9	6 7 8	3bitr3ri	⊢ ( 𝑏 𝑅 𝑐 ↔ ⟨ 𝑏 , 𝑐 ⟩ ∈ ◡ ◡ 𝑅 )
10		vex	⊢ 𝑎 ∈ V
11	4 10	brcnv	⊢ ( 𝑏 ◡ ◡ 𝑅 𝑎 ↔ 𝑎 ◡ 𝑅 𝑏 )
12		df-br	⊢ ( 𝑏 ◡ ◡ 𝑅 𝑎 ↔ ⟨ 𝑏 , 𝑎 ⟩ ∈ ◡ ◡ 𝑅 )
13	10 4	brcnv	⊢ ( 𝑎 ◡ 𝑅 𝑏 ↔ 𝑏 𝑅 𝑎 )
14	11 12 13	3bitr3ri	⊢ ( 𝑏 𝑅 𝑎 ↔ ⟨ 𝑏 , 𝑎 ⟩ ∈ ◡ ◡ 𝑅 )
15	9 14	anbi12ci	⊢ ( ( 𝑏 𝑅 𝑐 ∧ 𝑏 𝑅 𝑎 ) ↔ ( ⟨ 𝑏 , 𝑎 ⟩ ∈ ◡ ◡ 𝑅 ∧ ⟨ 𝑏 , 𝑐 ⟩ ∈ ◡ ◡ 𝑅 ) )
16	15	imbi1i	⊢ ( ( ( 𝑏 𝑅 𝑐 ∧ 𝑏 𝑅 𝑎 ) → 𝑎 = 𝑐 ) ↔ ( ( ⟨ 𝑏 , 𝑎 ⟩ ∈ ◡ ◡ 𝑅 ∧ ⟨ 𝑏 , 𝑐 ⟩ ∈ ◡ ◡ 𝑅 ) → 𝑎 = 𝑐 ) )
17	3 16	bitr3i	⊢ ( ( 𝑏 𝑅 𝑐 → ( 𝑏 𝑅 𝑎 → 𝑎 = 𝑐 ) ) ↔ ( ( ⟨ 𝑏 , 𝑎 ⟩ ∈ ◡ ◡ 𝑅 ∧ ⟨ 𝑏 , 𝑐 ⟩ ∈ ◡ ◡ 𝑅 ) → 𝑎 = 𝑐 ) )
18	17	albii	⊢ ( ∀ 𝑎 ( 𝑏 𝑅 𝑐 → ( 𝑏 𝑅 𝑎 → 𝑎 = 𝑐 ) ) ↔ ∀ 𝑎 ( ( ⟨ 𝑏 , 𝑎 ⟩ ∈ ◡ ◡ 𝑅 ∧ ⟨ 𝑏 , 𝑐 ⟩ ∈ ◡ ◡ 𝑅 ) → 𝑎 = 𝑐 ) )
19	2 18	bitr3i	⊢ ( ( 𝑏 𝑅 𝑐 → ∀ 𝑎 ( 𝑏 𝑅 𝑎 → 𝑎 = 𝑐 ) ) ↔ ∀ 𝑎 ( ( ⟨ 𝑏 , 𝑎 ⟩ ∈ ◡ ◡ 𝑅 ∧ ⟨ 𝑏 , 𝑐 ⟩ ∈ ◡ ◡ 𝑅 ) → 𝑎 = 𝑐 ) )
20	19	albii	⊢ ( ∀ 𝑐 ( 𝑏 𝑅 𝑐 → ∀ 𝑎 ( 𝑏 𝑅 𝑎 → 𝑎 = 𝑐 ) ) ↔ ∀ 𝑐 ∀ 𝑎 ( ( ⟨ 𝑏 , 𝑎 ⟩ ∈ ◡ ◡ 𝑅 ∧ ⟨ 𝑏 , 𝑐 ⟩ ∈ ◡ ◡ 𝑅 ) → 𝑎 = 𝑐 ) )
21		alcom	⊢ ( ∀ 𝑐 ∀ 𝑎 ( ( ⟨ 𝑏 , 𝑎 ⟩ ∈ ◡ ◡ 𝑅 ∧ ⟨ 𝑏 , 𝑐 ⟩ ∈ ◡ ◡ 𝑅 ) → 𝑎 = 𝑐 ) ↔ ∀ 𝑎 ∀ 𝑐 ( ( ⟨ 𝑏 , 𝑎 ⟩ ∈ ◡ ◡ 𝑅 ∧ ⟨ 𝑏 , 𝑐 ⟩ ∈ ◡ ◡ 𝑅 ) → 𝑎 = 𝑐 ) )
22	20 21	bitri	⊢ ( ∀ 𝑐 ( 𝑏 𝑅 𝑐 → ∀ 𝑎 ( 𝑏 𝑅 𝑎 → 𝑎 = 𝑐 ) ) ↔ ∀ 𝑎 ∀ 𝑐 ( ( ⟨ 𝑏 , 𝑎 ⟩ ∈ ◡ ◡ 𝑅 ∧ ⟨ 𝑏 , 𝑐 ⟩ ∈ ◡ ◡ 𝑅 ) → 𝑎 = 𝑐 ) )
23		opeq2	⊢ ( 𝑎 = 𝑐 → ⟨ 𝑏 , 𝑎 ⟩ = ⟨ 𝑏 , 𝑐 ⟩ )
24	23	eleq1d	⊢ ( 𝑎 = 𝑐 → ( ⟨ 𝑏 , 𝑎 ⟩ ∈ ◡ ◡ 𝑅 ↔ ⟨ 𝑏 , 𝑐 ⟩ ∈ ◡ ◡ 𝑅 ) )
25	24	mo4	⊢ ( ∃* 𝑎 ⟨ 𝑏 , 𝑎 ⟩ ∈ ◡ ◡ 𝑅 ↔ ∀ 𝑎 ∀ 𝑐 ( ( ⟨ 𝑏 , 𝑎 ⟩ ∈ ◡ ◡ 𝑅 ∧ ⟨ 𝑏 , 𝑐 ⟩ ∈ ◡ ◡ 𝑅 ) → 𝑎 = 𝑐 ) )
26		dfmo	⊢ ( ∃* 𝑎 ⟨ 𝑏 , 𝑎 ⟩ ∈ ◡ ◡ 𝑅 ↔ ∃ 𝑐 ∀ 𝑎 ( ⟨ 𝑏 , 𝑎 ⟩ ∈ ◡ ◡ 𝑅 → 𝑎 = 𝑐 ) )
27	22 25 26	3bitr2i	⊢ ( ∀ 𝑐 ( 𝑏 𝑅 𝑐 → ∀ 𝑎 ( 𝑏 𝑅 𝑎 → 𝑎 = 𝑐 ) ) ↔ ∃ 𝑐 ∀ 𝑎 ( ⟨ 𝑏 , 𝑎 ⟩ ∈ ◡ ◡ 𝑅 → 𝑎 = 𝑐 ) )
28	27	albii	⊢ ( ∀ 𝑏 ∀ 𝑐 ( 𝑏 𝑅 𝑐 → ∀ 𝑎 ( 𝑏 𝑅 𝑎 → 𝑎 = 𝑐 ) ) ↔ ∀ 𝑏 ∃ 𝑐 ∀ 𝑎 ( ⟨ 𝑏 , 𝑎 ⟩ ∈ ◡ ◡ 𝑅 → 𝑎 = 𝑐 ) )
29		relcnv	⊢ Rel ◡ ◡ 𝑅
30	29	biantrur	⊢ ( ∀ 𝑏 ∃ 𝑐 ∀ 𝑎 ( ⟨ 𝑏 , 𝑎 ⟩ ∈ ◡ ◡ 𝑅 → 𝑎 = 𝑐 ) ↔ ( Rel ◡ ◡ 𝑅 ∧ ∀ 𝑏 ∃ 𝑐 ∀ 𝑎 ( ⟨ 𝑏 , 𝑎 ⟩ ∈ ◡ ◡ 𝑅 → 𝑎 = 𝑐 ) ) )
31		dffun5	⊢ ( Fun ◡ ◡ 𝑅 ↔ ( Rel ◡ ◡ 𝑅 ∧ ∀ 𝑏 ∃ 𝑐 ∀ 𝑎 ( ⟨ 𝑏 , 𝑎 ⟩ ∈ ◡ ◡ 𝑅 → 𝑎 = 𝑐 ) ) )
32	30 31	bitr4i	⊢ ( ∀ 𝑏 ∃ 𝑐 ∀ 𝑎 ( ⟨ 𝑏 , 𝑎 ⟩ ∈ ◡ ◡ 𝑅 → 𝑎 = 𝑐 ) ↔ Fun ◡ ◡ 𝑅 )
33	1 28 32	3bitri	⊢ ( ∀ 𝑐 ∀ 𝑏 ( 𝑏 𝑅 𝑐 → ∀ 𝑎 ( 𝑏 𝑅 𝑎 → 𝑎 = 𝑐 ) ) ↔ Fun ◡ ◡ 𝑅 )