Theorem brsuccf 30700

Description: Binary relationship 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 30630	. . 3 |- Succ = (Cup o. ( _I (x) Singleton ) )
2	1	breqi 4426	. 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 5020	. 2 |- ( A (Cup o. ( _I (x) Singleton ) ) B <-> E. x ( A ( _I (x) Singleton ) x /\ xCup B ) )
6		opex 4681	. . . . 5 |- <. A , { A } >. e. _V
7		breq1 4423	. . . . 5 |- ( x = <. A , { A } >. -> ( xCup B <-> <. A , { A } >.Cup B ) )
8	6, 7	ceqsexv 3118	. . . 4 |- ( E. x ( x = <. A , { A } >. /\ xCup B ) <-> <. A , { A } >.Cup B )
9		snex 4658	. . . . 5 |- { A } e. _V
10	3, 9, 4	brcup 30698	. . . 4 |- ( <. A , { A } >.Cup B <-> B = ( A u. { A } ) )
11	8, 10	bitri 252	. . 3 |- ( E. x ( x = <. A , { A } >. /\ xCup B ) <-> B = ( A u. { A } ) )
12	3	brtxp2 30640	. . . . . 6 |- ( A ( _I (x) Singleton ) x <-> E. a E. b ( x = <. a , b >. /\ A _I a /\ ASingleton b ) )
13	12	anbi1i 699	. . . . 5 |- ( ( A ( _I (x) Singleton ) x /\ xCup B ) <-> ( E. a E. b ( x = <. a , b >. /\ A _I a /\ ASingleton b ) /\ xCup B ) )
14		3anass 986	. . . . . . . . 9 |- ( ( x = <. a , b >. /\ A _I a /\ ASingleton b ) <-> ( x = <. a , b >. /\ ( A _I a /\ ASingleton b ) ) )
15	14	anbi1i 699	. . . . . . . 8 |- ( ( ( x = <. a , b >. /\ A _I a /\ ASingleton b ) /\ xCup B ) <-> ( ( x = <. a , b >. /\ ( A _I a /\ ASingleton b ) ) /\ xCup B ) )
16		an32 805	. . . . . . . 8 |- ( ( ( x = <. a , b >. /\ ( A _I a /\ ASingleton b ) ) /\ xCup B ) <-> ( ( x = <. a , b >. /\ xCup B ) /\ ( A _I a /\ ASingleton b ) ) )
17		vex 3084	. . . . . . . . . . . . 13 |- a e. _V
18	17	ideq 5002	. . . . . . . . . . . 12 |- ( A _I a <-> A = a )
19		eqcom 2431	. . . . . . . . . . . 12 |- ( A = a <-> a = A )
20	18, 19	bitri 252	. . . . . . . . . . 11 |- ( A _I a <-> a = A )
21		vex 3084	. . . . . . . . . . . 12 |- b e. _V
22	3, 21	brsingle 30676	. . . . . . . . . . 11 |- ( ASingleton b <-> b = { A } )
23	20, 22	anbi12i 701	. . . . . . . . . 10 |- ( ( A _I a /\ ASingleton b ) <-> ( a = A /\ b = { A } ) )
24	23	anbi1i 699	. . . . . . . . 9 |- ( ( ( A _I a /\ ASingleton b ) /\ ( x = <. a , b >. /\ xCup B ) ) <-> ( ( a = A /\ b = { A } ) /\ ( x = <. a , b >. /\ xCup B ) ) )
25		ancom 451	. . . . . . . . 9 |- ( ( ( x = <. a , b >. /\ xCup B ) /\ ( A _I a /\ ASingleton b ) ) <-> ( ( A _I a /\ ASingleton b ) /\ ( x = <. a , b >. /\ xCup B ) ) )
26		df-3an 984	. . . . . . . . 9 |- ( ( a = A /\ b = { A } /\ ( x = <. a , b >. /\ xCup B ) ) <-> ( ( a = A /\ b = { A } ) /\ ( x = <. a , b >. /\ xCup B ) ) )
27	24, 25, 26	3bitr4i 280	. . . . . . . 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 274	. . . . . . 7 |- ( ( ( x = <. a , b >. /\ A _I a /\ ASingleton b ) /\ xCup B ) <-> ( a = A /\ b = { A } /\ ( x = <. a , b >. /\ xCup B ) ) )
29	28	2exbii 1713	. . . . . 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 1820	. . . . . 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 4184	. . . . . . . . 9 |- ( a = A -> <. a , b >. = <. A , b >. )
32	31	eqeq2d 2436	. . . . . . . 8 |- ( a = A -> ( x = <. a , b >. <-> x = <. A , b >. ) )
33	32	anbi1d 709	. . . . . . 7 |- ( a = A -> ( ( x = <. a , b >. /\ xCup B ) <-> ( x = <. A , b >. /\ xCup B ) ) )
34		opeq2 4185	. . . . . . . . 9 |- ( b = { A } -> <. A , b >. = <. A , { A } >. )
35	34	eqeq2d 2436	. . . . . . . 8 |- ( b = { A } -> ( x = <. A , b >. <-> x = <. A , { A } >. ) )
36	35	anbi1d 709	. . . . . . 7 |- ( b = { A } -> ( ( x = <. A , b >. /\ xCup B ) <-> ( x = <. A , { A } >. /\ xCup B ) ) )
37	3, 9, 33, 36	ceqsex2v 3120	. . . . . 6 |- ( E. a E. b ( a = A /\ b = { A } /\ ( x = <. a , b >. /\ xCup B ) ) <-> ( x = <. A , { A } >. /\ xCup B ) )
38	29, 30, 37	3bitr3i 278	. . . . 5 |- ( ( E. a E. b ( x = <. a , b >. /\ A _I a /\ ASingleton b ) /\ xCup B ) <-> ( x = <. A , { A } >. /\ xCup B ) )
39	13, 38	bitri 252	. . . 4 |- ( ( A ( _I (x) Singleton ) x /\ xCup B ) <-> ( x = <. A , { A } >. /\ xCup B ) )
40	39	exbii 1712	. . 3 |- ( E. x ( A ( _I (x) Singleton ) x /\ xCup B ) <-> E. x ( x = <. A , { A } >. /\ xCup B ) )
41		df-suc 5444	. . . 4 |- suc A = ( A u. { A } )
42	41	eqeq2i 2440	. . 3 |- ( B = suc A <-> B = ( A u. { A } ) )
43	11, 40, 42	3bitr4i 280	. 2 |- ( E. x ( A ( _I (x) Singleton ) x /\ xCup B ) <-> B = suc A )
44	2, 5, 43	3bitri 274	1 |- ( ASucc B <-> B = suc A )

Syntax hints:   <-> wb 187   /\ wa 370   /\ w3a 982   = wceq 1437   E.wex 1659   e. wcel 1868   _Vcvv 3081   u. cun 3434   {csn 3996   <.cop 4002   class class class wbr 4420   _I cid 4759   o. ccom 4853   suc csuc 5440   (x) ctxp 30588  Singletoncsingle 30596  Cupccup 30604  Succcsuccf 30606

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-8 1870  ax-9 1872  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-sep 4543  ax-nul 4551  ax-pow 4598  ax-pr 4656  ax-un 6593

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-mo 2270  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-ral 2780  df-rex 2781  df-rab 2784  df-v 3083  df-sbc 3300  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-symdif 3693  df-nul 3762  df-if 3910  df-sn 3997  df-pr 3999  df-op 4003  df-uni 4217  df-br 4421  df-opab 4480  df-mpt 4481  df-eprel 4760  df-id 4764  df-xp 4855  df-rel 4856  df-cnv 4857  df-co 4858  df-dm 4859  df-rn 4860  df-res 4861  df-suc 5444  df-iota 5561  df-fun 5599  df-fn 5600  df-f 5601  df-fo 5603  df-fv 5605  df-1st 6803  df-2nd 6804  df-txp 30612  df-singleton 30620  df-cup 30627  df-succf 30630

This theorem is referenced by:  dfrdg4  30710