Metamath Proof Explorer

Theorem lemsuccf

Description: Lemma for unfolding different forms 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 lemsuccf 
|- ( E. x ( A ( _I (x) Singleton ) x /\ x Cup B ) <-> B = suc A )

Proof

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