Metamath Proof Explorer

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 
|- ( A. c A. b ( b R c -> A. a ( b R a -> a = c ) ) <-> Fun `' `' R )

Proof

Step Hyp Ref Expression
1 alcom 
 |-  ( A. c A. b ( b R c -> A. a ( b R a -> a = c ) ) <-> A. b A. c ( b R c -> A. a ( b R a -> a = c ) ) )
2 19.21v 
 |-  ( A. a ( b R c -> ( b R a -> a = c ) ) <-> ( b R c -> A. a ( b R a -> a = c ) ) )
3 impexp 
 |-  ( ( ( b R c /\ b R a ) -> a = c ) <-> ( b R c -> ( b R a -> a = c ) ) )
4 vex 
 |-  b e. _V
5 vex 
 |-  c e. _V
6 4 5 brcnv 
 |-  ( b `' `' R c <-> c `' R b )
7 df-br 
 |-  ( b `' `' R c <-> <. b , c >. e. `' `' R )
8 5 4 brcnv 
 |-  ( c `' R b <-> b R c )
9 6 7 8 3bitr3ri 
 |-  ( b R c <-> <. b , c >. e. `' `' R )
10 vex 
 |-  a e. _V
11 4 10 brcnv 
 |-  ( b `' `' R a <-> a `' R b )
12 df-br 
 |-  ( b `' `' R a <-> <. b , a >. e. `' `' R )
13 10 4 brcnv 
 |-  ( a `' R b <-> b R a )
14 11 12 13 3bitr3ri 
 |-  ( b R a <-> <. b , a >. e. `' `' R )
15 9 14 anbi12ci 
 |-  ( ( b R c /\ b R a ) <-> ( <. b , a >. e. `' `' R /\ <. b , c >. e. `' `' R ) )
16 15 imbi1i 
 |-  ( ( ( b R c /\ b R a ) -> a = c ) <-> ( ( <. b , a >. e. `' `' R /\ <. b , c >. e. `' `' R ) -> a = c ) )
17 3 16 bitr3i 
 |-  ( ( b R c -> ( b R a -> a = c ) ) <-> ( ( <. b , a >. e. `' `' R /\ <. b , c >. e. `' `' R ) -> a = c ) )
18 17 albii 
 |-  ( A. a ( b R c -> ( b R a -> a = c ) ) <-> A. a ( ( <. b , a >. e. `' `' R /\ <. b , c >. e. `' `' R ) -> a = c ) )
19 2 18 bitr3i 
 |-  ( ( b R c -> A. a ( b R a -> a = c ) ) <-> A. a ( ( <. b , a >. e. `' `' R /\ <. b , c >. e. `' `' R ) -> a = c ) )
20 19 albii 
 |-  ( A. c ( b R c -> A. a ( b R a -> a = c ) ) <-> A. c A. a ( ( <. b , a >. e. `' `' R /\ <. b , c >. e. `' `' R ) -> a = c ) )
21 alcom 
 |-  ( A. c A. a ( ( <. b , a >. e. `' `' R /\ <. b , c >. e. `' `' R ) -> a = c ) <-> A. a A. c ( ( <. b , a >. e. `' `' R /\ <. b , c >. e. `' `' R ) -> a = c ) )
22 20 21 bitri 
 |-  ( A. c ( b R c -> A. a ( b R a -> a = c ) ) <-> A. a A. c ( ( <. b , a >. e. `' `' R /\ <. b , c >. e. `' `' R ) -> a = c ) )
23 opeq2 
 |-  ( a = c -> <. b , a >. = <. b , c >. )
24 23 eleq1d 
 |-  ( a = c -> ( <. b , a >. e. `' `' R <-> <. b , c >. e. `' `' R ) )
25 24 mo4 
 |-  ( E* a <. b , a >. e. `' `' R <-> A. a A. c ( ( <. b , a >. e. `' `' R /\ <. b , c >. e. `' `' R ) -> a = c ) )
26 df-mo 
 |-  ( E* a <. b , a >. e. `' `' R <-> E. c A. a ( <. b , a >. e. `' `' R -> a = c ) )
27 22 25 26 3bitr2i 
 |-  ( A. c ( b R c -> A. a ( b R a -> a = c ) ) <-> E. c A. a ( <. b , a >. e. `' `' R -> a = c ) )
28 27 albii 
 |-  ( A. b A. c ( b R c -> A. a ( b R a -> a = c ) ) <-> A. b E. c A. a ( <. b , a >. e. `' `' R -> a = c ) )
29 relcnv 
 |-  Rel `' `' R
30 29 biantrur 
 |-  ( A. b E. c A. a ( <. b , a >. e. `' `' R -> a = c ) <-> ( Rel `' `' R /\ A. b E. c A. a ( <. b , a >. e. `' `' R -> a = c ) ) )
31 dffun5 
 |-  ( Fun `' `' R <-> ( Rel `' `' R /\ A. b E. c A. a ( <. b , a >. e. `' `' R -> a = c ) ) )
32 30 31 bitr4i 
 |-  ( A. b E. c A. a ( <. b , a >. e. `' `' R -> a = c ) <-> Fun `' `' R )
33 1 28 32 3bitri 
 |-  ( A. c A. b ( b R c -> A. a ( b R a -> a = c ) ) <-> Fun `' `' R )