Theorem brsuccf 32048

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

Hypotheses

Ref	Expression
brsuccf.1	|- A e. _V
brsuccf.2	|- B e. _V

Assertion

Ref	Expression
brsuccf	|- ( ASucc B <-> B = suc A )

Proof of Theorem brsuccf

Dummy variables a b x are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-succf 31979	. . 3 |- Succ = (Cup o. ( _I (x) Singleton ) )
2	1	breqi 4659	. 2 |- ( ASucc B <-> A (Cup o. ( _I (x) Singleton ) ) B )
3		brsuccf.1	. . 3 |- A e. _V
4		brsuccf.2	. . 3 |- B e. _V
5	3, 4	brco 5292	. 2 |- ( A (Cup o. ( _I (x) Singleton ) ) B <-> E. x ( A ( _I (x) Singleton ) x /\ xCup B ) )
6		opex 4932	. . . . 5 |- <. A , { A } >. e. _V
7		breq1 4656	. . . . 5 |- ( x = <. A , { A } >. -> ( xCup B <-> <. A , { A } >.Cup B ) )
8	6, 7	ceqsexv 3242	. . . 4 |- ( E. x ( x = <. A , { A } >. /\ xCup B ) <-> <. A , { A } >.Cup B )
9		snex 4908	. . . . 5 |- { A } e. _V
10	3, 9, 4	brcup 32046	. . . 4 |- ( <. A , { A } >.Cup B <-> B = ( A u. { A } ) )
11	8, 10	bitri 264	. . 3 |- ( E. x ( x = <. A , { A } >. /\ xCup B ) <-> B = ( A u. { A } ) )
12	3	brtxp2 31988	. . . . . 6 |- ( A ( _I (x) Singleton ) x <-> E. a E. b ( x = <. a , b >. /\ A _I a /\ ASingleton b ) )
13	12	anbi1i 731	. . . . 5 |- ( ( A ( _I (x) Singleton ) x /\ xCup B ) <-> ( E. a E. b ( x = <. a , b >. /\ A _I a /\ ASingleton b ) /\ xCup B ) )
14		3anass 1042	. . . . . . . . 9 |- ( ( x = <. a , b >. /\ A _I a /\ ASingleton b ) <-> ( x = <. a , b >. /\ ( A _I a /\ ASingleton b ) ) )
15	14	anbi1i 731	. . . . . . . 8 |- ( ( ( x = <. a , b >. /\ A _I a /\ ASingleton b ) /\ xCup B ) <-> ( ( x = <. a , b >. /\ ( A _I a /\ ASingleton b ) ) /\ xCup B ) )
16		an32 839	. . . . . . . 8 |- ( ( ( x = <. a , b >. /\ ( A _I a /\ ASingleton b ) ) /\ xCup B ) <-> ( ( x = <. a , b >. /\ xCup B ) /\ ( A _I a /\ ASingleton b ) ) )
17		vex 3203	. . . . . . . . . . . . 13 |- a e. _V
18	17	ideq 5274	. . . . . . . . . . . 12 |- ( A _I a <-> A = a )
19		eqcom 2629	. . . . . . . . . . . 12 |- ( A = a <-> a = A )
20	18, 19	bitri 264	. . . . . . . . . . 11 |- ( A _I a <-> a = A )
21		vex 3203	. . . . . . . . . . . 12 |- b e. _V
22	3, 21	brsingle 32024	. . . . . . . . . . 11 |- ( ASingleton b <-> b = { A } )
23	20, 22	anbi12i 733	. . . . . . . . . 10 |- ( ( A _I a /\ ASingleton b ) <-> ( a = A /\ b = { A } ) )
24	23	anbi1i 731	. . . . . . . . 9 |- ( ( ( A _I a /\ ASingleton b ) /\ ( x = <. a , b >. /\ xCup B ) ) <-> ( ( a = A /\ b = { A } ) /\ ( x = <. a , b >. /\ xCup B ) ) )
25		ancom 466	. . . . . . . . 9 |- ( ( ( x = <. a , b >. /\ xCup B ) /\ ( A _I a /\ ASingleton b ) ) <-> ( ( A _I a /\ ASingleton b ) /\ ( x = <. a , b >. /\ xCup B ) ) )
26		df-3an 1039	. . . . . . . . 9 |- ( ( a = A /\ b = { A } /\ ( x = <. a , b >. /\ xCup B ) ) <-> ( ( a = A /\ b = { A } ) /\ ( x = <. a , b >. /\ xCup B ) ) )
27	24, 25, 26	3bitr4i 292	. . . . . . . 8 |- ( ( ( x = <. a , b >. /\ xCup B ) /\ ( A _I a /\ ASingleton b ) ) <-> ( a = A /\ b = { A } /\ ( x = <. a , b >. /\ xCup B ) ) )
28	15, 16, 27	3bitri 286	. . . . . . 7 |- ( ( ( x = <. a , b >. /\ A _I a /\ ASingleton b ) /\ xCup B ) <-> ( a = A /\ b = { A } /\ ( x = <. a , b >. /\ xCup B ) ) )
29	28	2exbii 1775	. . . . . 6 |- ( E. a E. b ( ( x = <. a , b >. /\ A _I a /\ ASingleton b ) /\ xCup B ) <-> E. a E. b ( a = A /\ b = { A } /\ ( x = <. a , b >. /\ xCup B ) ) )
30		19.41vv 1915	. . . . . 6 |- ( E. a E. b ( ( x = <. a , b >. /\ A _I a /\ ASingleton b ) /\ xCup B ) <-> ( E. a E. b ( x = <. a , b >. /\ A _I a /\ ASingleton b ) /\ xCup B ) )
31		opeq1 4402	. . . . . . . . 9 |- ( a = A -> <. a , b >. = <. A , b >. )
32	31	eqeq2d 2632	. . . . . . . 8 |- ( a = A -> ( x = <. a , b >. <-> x = <. A , b >. ) )
33	32	anbi1d 741	. . . . . . 7 |- ( a = A -> ( ( x = <. a , b >. /\ xCup B ) <-> ( x = <. A , b >. /\ xCup B ) ) )
34		opeq2 4403	. . . . . . . . 9 |- ( b = { A } -> <. A , b >. = <. A , { A } >. )
35	34	eqeq2d 2632	. . . . . . . 8 |- ( b = { A } -> ( x = <. A , b >. <-> x = <. A , { A } >. ) )
36	35	anbi1d 741	. . . . . . 7 |- ( b = { A } -> ( ( x = <. A , b >. /\ xCup B ) <-> ( x = <. A , { A } >. /\ xCup B ) ) )
37	3, 9, 33, 36	ceqsex2v 3245	. . . . . 6 |- ( E. a E. b ( a = A /\ b = { A } /\ ( x = <. a , b >. /\ xCup B ) ) <-> ( x = <. A , { A } >. /\ xCup B ) )
38	29, 30, 37	3bitr3i 290	. . . . 5 |- ( ( E. a E. b ( x = <. a , b >. /\ A _I a /\ ASingleton b ) /\ xCup B ) <-> ( x = <. A , { A } >. /\ xCup B ) )
39	13, 38	bitri 264	. . . 4 |- ( ( A ( _I (x) Singleton ) x /\ xCup B ) <-> ( x = <. A , { A } >. /\ xCup B ) )
40	39	exbii 1774	. . 3 |- ( E. x ( A ( _I (x) Singleton ) x /\ xCup B ) <-> E. x ( x = <. A , { A } >. /\ xCup B ) )
41		df-suc 5729	. . . 4 |- suc A = ( A u. { A } )
42	41	eqeq2i 2634	. . 3 |- ( B = suc A <-> B = ( A u. { A } ) )
43	11, 40, 42	3bitr4i 292	. 2 |- ( E. x ( A ( _I (x) Singleton ) x /\ xCup B ) <-> B = suc A )
44	2, 5, 43	3bitri 286	1 |- ( ASucc B <-> B = suc A )

Syntax hints:   <-> wb 196   /\ wa 384   /\ w3a 1037   = wceq 1483   E.wex 1704   e. wcel 1990   _Vcvv 3200   u. cun 3572   {csn 4177   <.cop 4183   class class class wbr 4653   _I cid 5023   o. ccom 5118   suc csuc 5725   (x) ctxp 31937  Singletoncsingle 31945  Cupccup 31953  Succcsuccf 31955

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-symdif 3844  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-mpt 4730  df-id 5024  df-eprel 5029  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-fo 5894  df-fv 5896  df-1st 7168  df-2nd 7169  df-txp 31961  df-singleton 31969  df-cup 31976  df-succf 31979

This theorem is referenced by:  dfrdg4  32058