Metamath Proof Explorer

Theorem brsuccf

Description: Binary relation form of the Succ function. (Contributed by Scott Fenton, 14-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Hypotheses brsuccf.1 
|- A e. _V
brsuccf.2 
|- B e. _V
Assertion brsuccf 
|- ( A Succ B <-> B = suc A )

Proof

Step Hyp Ref Expression
1 brsuccf.1 
 |-  A e. _V
2 brsuccf.2 
 |-  B e. _V
3 df-succf 
 |-  Succ = ( Cup o. ( _I (x) Singleton ) )
4 3 breqi 
 |-  ( A Succ B <-> A ( Cup o. ( _I (x) Singleton ) ) B )
5 1 2 brco 
 |-  ( A ( Cup o. ( _I (x) Singleton ) ) B <-> E. x ( A ( _I (x) Singleton ) x /\ x Cup B ) )
6 opex 
 |-  <. A , { A } >. e. _V
7 breq1 
 |-  ( x = <. A , { A } >. -> ( x Cup B <-> <. A , { A } >. Cup B ) )
8 6 7 ceqsexv 
 |-  ( E. x ( x = <. A , { A } >. /\ x Cup B ) <-> <. A , { A } >. Cup B )
9 snex 
 |-  { A } e. _V
10 1 9 2 brcup 
 |-  ( <. A , { A } >. Cup B <-> B = ( A u. { A } ) )
11 8 10 bitri 
 |-  ( E. x ( x = <. A , { A } >. /\ x Cup B ) <-> B = ( A u. { A } ) )
12 1 brtxp2 
 |-  ( A ( _I (x) Singleton ) x <-> E. a E. b ( x = <. a , b >. /\ A _I a /\ A Singleton b ) )
13 12 anbi1i 
 |-  ( ( A ( _I (x) Singleton ) x /\ x Cup B ) <-> ( E. a E. b ( x = <. a , b >. /\ A _I a /\ A Singleton b ) /\ x Cup B ) )
14 3anass 
 |-  ( ( x = <. a , b >. /\ A _I a /\ A Singleton b ) <-> ( x = <. a , b >. /\ ( A _I a /\ A Singleton b ) ) )
15 14 anbi1i 
 |-  ( ( ( x = <. a , b >. /\ A _I a /\ A Singleton b ) /\ x Cup B ) <-> ( ( x = <. a , b >. /\ ( A _I a /\ A Singleton b ) ) /\ x Cup B ) )
16 an32 
 |-  ( ( ( x = <. a , b >. /\ ( A _I a /\ A Singleton b ) ) /\ x Cup B ) <-> ( ( x = <. a , b >. /\ x Cup B ) /\ ( A _I a /\ A Singleton b ) ) )
17 vex 
 |-  a e. _V
18 17 ideq 
 |-  ( A _I a <-> A = a )
19 eqcom 
 |-  ( A = a <-> a = A )
20 18 19 bitri 
 |-  ( A _I a <-> a = A )
21 vex 
 |-  b e. _V
22 1 21 brsingle 
 |-  ( A Singleton b <-> b = { A } )
23 20 22 anbi12i 
 |-  ( ( A _I a /\ A Singleton b ) <-> ( a = A /\ b = { A } ) )
24 23 anbi1i 
 |-  ( ( ( A _I a /\ A Singleton b ) /\ ( x = <. a , b >. /\ x Cup B ) ) <-> ( ( a = A /\ b = { A } ) /\ ( x = <. a , b >. /\ x Cup B ) ) )
25 ancom 
 |-  ( ( ( x = <. a , b >. /\ x Cup B ) /\ ( A _I a /\ A Singleton b ) ) <-> ( ( A _I a /\ A Singleton b ) /\ ( x = <. a , b >. /\ x Cup B ) ) )
26 df-3an 
 |-  ( ( a = A /\ b = { A } /\ ( x = <. a , b >. /\ x Cup B ) ) <-> ( ( a = A /\ b = { A } ) /\ ( x = <. a , b >. /\ x Cup B ) ) )
27 24 25 26 3bitr4i 
 |-  ( ( ( x = <. a , b >. /\ x Cup B ) /\ ( A _I a /\ A Singleton b ) ) <-> ( a = A /\ b = { A } /\ ( x = <. a , b >. /\ x Cup B ) ) )
28 15 16 27 3bitri 
 |-  ( ( ( x = <. a , b >. /\ A _I a /\ A Singleton b ) /\ x Cup B ) <-> ( a = A /\ b = { A } /\ ( x = <. a , b >. /\ x Cup B ) ) )
29 28 2exbii 
 |-  ( E. a E. b ( ( x = <. a , b >. /\ A _I a /\ A Singleton b ) /\ x Cup B ) <-> E. a E. b ( a = A /\ b = { A } /\ ( x = <. a , b >. /\ x Cup B ) ) )
30 19.41vv 
 |-  ( E. a E. b ( ( x = <. a , b >. /\ A _I a /\ A Singleton b ) /\ x Cup B ) <-> ( E. a E. b ( x = <. a , b >. /\ A _I a /\ A Singleton b ) /\ x Cup B ) )
31 opeq1 
 |-  ( a = A -> <. a , b >. = <. A , b >. )
32 31 eqeq2d 
 |-  ( a = A -> ( x = <. a , b >. <-> x = <. A , b >. ) )
33 32 anbi1d 
 |-  ( a = A -> ( ( x = <. a , b >. /\ x Cup B ) <-> ( x = <. A , b >. /\ x Cup B ) ) )
34 opeq2 
 |-  ( b = { A } -> <. A , b >. = <. A , { A } >. )
35 34 eqeq2d 
 |-  ( b = { A } -> ( x = <. A , b >. <-> x = <. A , { A } >. ) )
36 35 anbi1d 
 |-  ( b = { A } -> ( ( x = <. A , b >. /\ x Cup B ) <-> ( x = <. A , { A } >. /\ x Cup B ) ) )
37 1 9 33 36 ceqsex2v 
 |-  ( E. a E. b ( a = A /\ b = { A } /\ ( x = <. a , b >. /\ x Cup B ) ) <-> ( x = <. A , { A } >. /\ x Cup B ) )
38 29 30 37 3bitr3i 
 |-  ( ( E. a E. b ( x = <. a , b >. /\ A _I a /\ A Singleton b ) /\ x Cup B ) <-> ( x = <. A , { A } >. /\ x Cup B ) )
39 13 38 bitri 
 |-  ( ( A ( _I (x) Singleton ) x /\ x Cup B ) <-> ( x = <. A , { A } >. /\ x Cup B ) )
40 39 exbii 
 |-  ( E. x ( A ( _I (x) Singleton ) x /\ x Cup B ) <-> E. x ( x = <. A , { A } >. /\ x Cup B ) )
41 df-suc 
 |-  suc A = ( A u. { A } )
42 41 eqeq2i 
 |-  ( B = suc A <-> B = ( A u. { A } ) )
43 11 40 42 3bitr4i 
 |-  ( E. x ( A ( _I (x) Singleton ) x /\ x Cup B ) <-> B = suc A )
44 4 5 43 3bitri 
 |-  ( A Succ B <-> B = suc A )