Theorem brsuccf 30758

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 30688	. . 3 |- Succ = (Cup o. ( _I (x) Singleton ) )
2	1	breqi 4424	. 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 5027	. 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 4421	. . . . 5 |- ( x = <. A , { A } >. -> ( xCup B <-> <. A , { A } >.Cup B ) )
8	6, 7	ceqsexv 3096	. . . 4 |- ( E. x ( x = <. A , { A } >. /\ xCup B ) <-> <. A , { A } >.Cup B )
9		snex 4658	. . . . 5 |- { A } e. _V
10	3, 9, 4	brcup 30756	. . . 4 |- ( <. A , { A } >.Cup B <-> B = ( A u. { A } ) )
11	8, 10	bitri 257	. . 3 |- ( E. x ( x = <. A , { A } >. /\ xCup B ) <-> B = ( A u. { A } ) )
12	3	brtxp2 30698	. . . . . 6 |- ( A ( _I (x) Singleton ) x <-> E. a E. b ( x = <. a , b >. /\ A _I a /\ ASingleton b ) )
13	12	anbi1i 706	. . . . 5 |- ( ( A ( _I (x) Singleton ) x /\ xCup B ) <-> ( E. a E. b ( x = <. a , b >. /\ A _I a /\ ASingleton b ) /\ xCup B ) )
14		3anass 995	. . . . . . . . 9 |- ( ( x = <. a , b >. /\ A _I a /\ ASingleton b ) <-> ( x = <. a , b >. /\ ( A _I a /\ ASingleton b ) ) )
15	14	anbi1i 706	. . . . . . . 8 |- ( ( ( x = <. a , b >. /\ A _I a /\ ASingleton b ) /\ xCup B ) <-> ( ( x = <. a , b >. /\ ( A _I a /\ ASingleton b ) ) /\ xCup B ) )
16		an32 812	. . . . . . . 8 |- ( ( ( x = <. a , b >. /\ ( A _I a /\ ASingleton b ) ) /\ xCup B ) <-> ( ( x = <. a , b >. /\ xCup B ) /\ ( A _I a /\ ASingleton b ) ) )
17		vex 3060	. . . . . . . . . . . . 13 |- a e. _V
18	17	ideq 5009	. . . . . . . . . . . 12 |- ( A _I a <-> A = a )
19		eqcom 2469	. . . . . . . . . . . 12 |- ( A = a <-> a = A )
20	18, 19	bitri 257	. . . . . . . . . . 11 |- ( A _I a <-> a = A )
21		vex 3060	. . . . . . . . . . . 12 |- b e. _V
22	3, 21	brsingle 30734	. . . . . . . . . . 11 |- ( ASingleton b <-> b = { A } )
23	20, 22	anbi12i 708	. . . . . . . . . 10 |- ( ( A _I a /\ ASingleton b ) <-> ( a = A /\ b = { A } ) )
24	23	anbi1i 706	. . . . . . . . 9 |- ( ( ( A _I a /\ ASingleton b ) /\ ( x = <. a , b >. /\ xCup B ) ) <-> ( ( a = A /\ b = { A } ) /\ ( x = <. a , b >. /\ xCup B ) ) )
25		ancom 456	. . . . . . . . 9 |- ( ( ( x = <. a , b >. /\ xCup B ) /\ ( A _I a /\ ASingleton b ) ) <-> ( ( A _I a /\ ASingleton b ) /\ ( x = <. a , b >. /\ xCup B ) ) )
26		df-3an 993	. . . . . . . . 9 |- ( ( a = A /\ b = { A } /\ ( x = <. a , b >. /\ xCup B ) ) <-> ( ( a = A /\ b = { A } ) /\ ( x = <. a , b >. /\ xCup B ) ) )
27	24, 25, 26	3bitr4i 285	. . . . . . . 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 279	. . . . . . 7 |- ( ( ( x = <. a , b >. /\ A _I a /\ ASingleton b ) /\ xCup B ) <-> ( a = A /\ b = { A } /\ ( x = <. a , b >. /\ xCup B ) ) )
29	28	2exbii 1730	. . . . . 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 1842	. . . . . 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 4180	. . . . . . . . 9 |- ( a = A -> <. a , b >. = <. A , b >. )
32	31	eqeq2d 2472	. . . . . . . 8 |- ( a = A -> ( x = <. a , b >. <-> x = <. A , b >. ) )
33	32	anbi1d 716	. . . . . . 7 |- ( a = A -> ( ( x = <. a , b >. /\ xCup B ) <-> ( x = <. A , b >. /\ xCup B ) ) )
34		opeq2 4181	. . . . . . . . 9 |- ( b = { A } -> <. A , b >. = <. A , { A } >. )
35	34	eqeq2d 2472	. . . . . . . 8 |- ( b = { A } -> ( x = <. A , b >. <-> x = <. A , { A } >. ) )
36	35	anbi1d 716	. . . . . . 7 |- ( b = { A } -> ( ( x = <. A , b >. /\ xCup B ) <-> ( x = <. A , { A } >. /\ xCup B ) ) )
37	3, 9, 33, 36	ceqsex2v 3099	. . . . . 6 |- ( E. a E. b ( a = A /\ b = { A } /\ ( x = <. a , b >. /\ xCup B ) ) <-> ( x = <. A , { A } >. /\ xCup B ) )
38	29, 30, 37	3bitr3i 283	. . . . 5 |- ( ( E. a E. b ( x = <. a , b >. /\ A _I a /\ ASingleton b ) /\ xCup B ) <-> ( x = <. A , { A } >. /\ xCup B ) )
39	13, 38	bitri 257	. . . 4 |- ( ( A ( _I (x) Singleton ) x /\ xCup B ) <-> ( x = <. A , { A } >. /\ xCup B ) )
40	39	exbii 1729	. . 3 |- ( E. x ( A ( _I (x) Singleton ) x /\ xCup B ) <-> E. x ( x = <. A , { A } >. /\ xCup B ) )
41		df-suc 5452	. . . 4 |- suc A = ( A u. { A } )
42	41	eqeq2i 2474	. . 3 |- ( B = suc A <-> B = ( A u. { A } ) )
43	11, 40, 42	3bitr4i 285	. 2 |- ( E. x ( A ( _I (x) Singleton ) x /\ xCup B ) <-> B = suc A )
44	2, 5, 43	3bitri 279	1 |- ( ASucc B <-> B = suc A )

Syntax hints:   <-> wb 189   /\ wa 375   /\ w3a 991   = wceq 1455   E.wex 1674   e. wcel 1898   _Vcvv 3057   u. cun 3414   {csn 3980   <.cop 3986   class class class wbr 4418   _I cid 4766   o. ccom 4860   suc csuc 5448   (x) ctxp 30646  Singletoncsingle 30654  Cupccup 30662  Succcsuccf 30664

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-8 1900  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-sep 4541  ax-nul 4550  ax-pow 4598  ax-pr 4656  ax-un 6615

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-ral 2754  df-rex 2755  df-rab 2758  df-v 3059  df-sbc 3280  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-symdif 3675  df-nul 3744  df-if 3894  df-sn 3981  df-pr 3983  df-op 3987  df-uni 4213  df-br 4419  df-opab 4478  df-mpt 4479  df-eprel 4767  df-id 4771  df-xp 4862  df-rel 4863  df-cnv 4864  df-co 4865  df-dm 4866  df-rn 4867  df-res 4868  df-suc 5452  df-iota 5569  df-fun 5607  df-fn 5608  df-f 5609  df-fo 5611  df-fv 5613  df-1st 6825  df-2nd 6826  df-txp 30670  df-singleton 30678  df-cup 30685  df-succf 30688

This theorem is referenced by:  dfrdg4  30768