oarec

Description: Recursive definition of ordinal addition. Exercise 25 of Enderton p. 240. (Contributed by NM, 26-Dec-2004) (Revised by Mario Carneiro, 30-May-2015)

		Ref	Expression
	Assertion	oarec	\|- ( ( A e. On /\ B e. On ) -> ( A +o B ) = ( A u. ran ( x e. B \|-> ( A +o x ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		oveq2	\|- ( z = (/) -> ( A +o z ) = ( A +o (/) ) )
2		mpteq1	\|- ( z = (/) -> ( x e. z \|-> ( A +o x ) ) = ( x e. (/) \|-> ( A +o x ) ) )
3		mpt0	\|- ( x e. (/) \|-> ( A +o x ) ) = (/)
4	2 3	eqtrdi	\|- ( z = (/) -> ( x e. z \|-> ( A +o x ) ) = (/) )
5	4	rneqd	\|- ( z = (/) -> ran ( x e. z \|-> ( A +o x ) ) = ran (/) )
6		rn0	\|- ran (/) = (/)
7	5 6	eqtrdi	\|- ( z = (/) -> ran ( x e. z \|-> ( A +o x ) ) = (/) )
8	7	uneq2d	\|- ( z = (/) -> ( A u. ran ( x e. z \|-> ( A +o x ) ) ) = ( A u. (/) ) )
9	1 8	eqeq12d	\|- ( z = (/) -> ( ( A +o z ) = ( A u. ran ( x e. z \|-> ( A +o x ) ) ) <-> ( A +o (/) ) = ( A u. (/) ) ) )
10		oveq2	\|- ( z = w -> ( A +o z ) = ( A +o w ) )
11		mpteq1	\|- ( z = w -> ( x e. z \|-> ( A +o x ) ) = ( x e. w \|-> ( A +o x ) ) )
12	11	rneqd	\|- ( z = w -> ran ( x e. z \|-> ( A +o x ) ) = ran ( x e. w \|-> ( A +o x ) ) )
13	12	uneq2d	\|- ( z = w -> ( A u. ran ( x e. z \|-> ( A +o x ) ) ) = ( A u. ran ( x e. w \|-> ( A +o x ) ) ) )
14	10 13	eqeq12d	\|- ( z = w -> ( ( A +o z ) = ( A u. ran ( x e. z \|-> ( A +o x ) ) ) <-> ( A +o w ) = ( A u. ran ( x e. w \|-> ( A +o x ) ) ) ) )
15		oveq2	\|- ( z = suc w -> ( A +o z ) = ( A +o suc w ) )
16		mpteq1	\|- ( z = suc w -> ( x e. z \|-> ( A +o x ) ) = ( x e. suc w \|-> ( A +o x ) ) )
17	16	rneqd	\|- ( z = suc w -> ran ( x e. z \|-> ( A +o x ) ) = ran ( x e. suc w \|-> ( A +o x ) ) )
18	17	uneq2d	\|- ( z = suc w -> ( A u. ran ( x e. z \|-> ( A +o x ) ) ) = ( A u. ran ( x e. suc w \|-> ( A +o x ) ) ) )
19	15 18	eqeq12d	\|- ( z = suc w -> ( ( A +o z ) = ( A u. ran ( x e. z \|-> ( A +o x ) ) ) <-> ( A +o suc w ) = ( A u. ran ( x e. suc w \|-> ( A +o x ) ) ) ) )
20		oveq2	\|- ( z = B -> ( A +o z ) = ( A +o B ) )
21		mpteq1	\|- ( z = B -> ( x e. z \|-> ( A +o x ) ) = ( x e. B \|-> ( A +o x ) ) )
22	21	rneqd	\|- ( z = B -> ran ( x e. z \|-> ( A +o x ) ) = ran ( x e. B \|-> ( A +o x ) ) )
23	22	uneq2d	\|- ( z = B -> ( A u. ran ( x e. z \|-> ( A +o x ) ) ) = ( A u. ran ( x e. B \|-> ( A +o x ) ) ) )
24	20 23	eqeq12d	\|- ( z = B -> ( ( A +o z ) = ( A u. ran ( x e. z \|-> ( A +o x ) ) ) <-> ( A +o B ) = ( A u. ran ( x e. B \|-> ( A +o x ) ) ) ) )
25		oa0	\|- ( A e. On -> ( A +o (/) ) = A )
26		un0	\|- ( A u. (/) ) = A
27	25 26	eqtr4di	\|- ( A e. On -> ( A +o (/) ) = ( A u. (/) ) )
28		uneq1	\|- ( ( A +o w ) = ( A u. ran ( x e. w \|-> ( A +o x ) ) ) -> ( ( A +o w ) u. { ( A +o w ) } ) = ( ( A u. ran ( x e. w \|-> ( A +o x ) ) ) u. { ( A +o w ) } ) )
29		unass	\|- ( ( A u. ran ( x e. w \|-> ( A +o x ) ) ) u. { ( A +o w ) } ) = ( A u. ( ran ( x e. w \|-> ( A +o x ) ) u. { ( A +o w ) } ) )
30		rexun	\|- ( E. x e. ( w u. { w } ) y = ( A +o x ) <-> ( E. x e. w y = ( A +o x ) \/ E. x e. { w } y = ( A +o x ) ) )
31		df-suc	\|- suc w = ( w u. { w } )
32	31	rexeqi	\|- ( E. x e. suc w y = ( A +o x ) <-> E. x e. ( w u. { w } ) y = ( A +o x ) )
33		eqid	\|- ( x e. w \|-> ( A +o x ) ) = ( x e. w \|-> ( A +o x ) )
34	33	elrnmpt	\|- ( y e. _V -> ( y e. ran ( x e. w \|-> ( A +o x ) ) <-> E. x e. w y = ( A +o x ) ) )
35	34	elv	\|- ( y e. ran ( x e. w \|-> ( A +o x ) ) <-> E. x e. w y = ( A +o x ) )
36		velsn	\|- ( y e. { ( A +o w ) } <-> y = ( A +o w ) )
37		vex	\|- w e. _V
38		oveq2	\|- ( x = w -> ( A +o x ) = ( A +o w ) )
39	38	eqeq2d	\|- ( x = w -> ( y = ( A +o x ) <-> y = ( A +o w ) ) )
40	37 39	rexsn	\|- ( E. x e. { w } y = ( A +o x ) <-> y = ( A +o w ) )
41	36 40	bitr4i	\|- ( y e. { ( A +o w ) } <-> E. x e. { w } y = ( A +o x ) )
42	35 41	orbi12i	\|- ( ( y e. ran ( x e. w \|-> ( A +o x ) ) \/ y e. { ( A +o w ) } ) <-> ( E. x e. w y = ( A +o x ) \/ E. x e. { w } y = ( A +o x ) ) )
43	30 32 42	3bitr4i	\|- ( E. x e. suc w y = ( A +o x ) <-> ( y e. ran ( x e. w \|-> ( A +o x ) ) \/ y e. { ( A +o w ) } ) )
44		eqid	\|- ( x e. suc w \|-> ( A +o x ) ) = ( x e. suc w \|-> ( A +o x ) )
45		ovex	\|- ( A +o x ) e. _V
46	44 45	elrnmpti	\|- ( y e. ran ( x e. suc w \|-> ( A +o x ) ) <-> E. x e. suc w y = ( A +o x ) )
47		elun	\|- ( y e. ( ran ( x e. w \|-> ( A +o x ) ) u. { ( A +o w ) } ) <-> ( y e. ran ( x e. w \|-> ( A +o x ) ) \/ y e. { ( A +o w ) } ) )
48	43 46 47	3bitr4i	\|- ( y e. ran ( x e. suc w \|-> ( A +o x ) ) <-> y e. ( ran ( x e. w \|-> ( A +o x ) ) u. { ( A +o w ) } ) )
49	48	eqriv	\|- ran ( x e. suc w \|-> ( A +o x ) ) = ( ran ( x e. w \|-> ( A +o x ) ) u. { ( A +o w ) } )
50	49	uneq2i	\|- ( A u. ran ( x e. suc w \|-> ( A +o x ) ) ) = ( A u. ( ran ( x e. w \|-> ( A +o x ) ) u. { ( A +o w ) } ) )
51	29 50	eqtr4i	\|- ( ( A u. ran ( x e. w \|-> ( A +o x ) ) ) u. { ( A +o w ) } ) = ( A u. ran ( x e. suc w \|-> ( A +o x ) ) )
52	28 51	eqtrdi	\|- ( ( A +o w ) = ( A u. ran ( x e. w \|-> ( A +o x ) ) ) -> ( ( A +o w ) u. { ( A +o w ) } ) = ( A u. ran ( x e. suc w \|-> ( A +o x ) ) ) )
53		oasuc	\|- ( ( A e. On /\ w e. On ) -> ( A +o suc w ) = suc ( A +o w ) )
54		df-suc	\|- suc ( A +o w ) = ( ( A +o w ) u. { ( A +o w ) } )
55	53 54	eqtrdi	\|- ( ( A e. On /\ w e. On ) -> ( A +o suc w ) = ( ( A +o w ) u. { ( A +o w ) } ) )
56	55	eqeq1d	\|- ( ( A e. On /\ w e. On ) -> ( ( A +o suc w ) = ( A u. ran ( x e. suc w \|-> ( A +o x ) ) ) <-> ( ( A +o w ) u. { ( A +o w ) } ) = ( A u. ran ( x e. suc w \|-> ( A +o x ) ) ) ) )
57	52 56	imbitrrid	\|- ( ( A e. On /\ w e. On ) -> ( ( A +o w ) = ( A u. ran ( x e. w \|-> ( A +o x ) ) ) -> ( A +o suc w ) = ( A u. ran ( x e. suc w \|-> ( A +o x ) ) ) ) )
58	57	expcom	\|- ( w e. On -> ( A e. On -> ( ( A +o w ) = ( A u. ran ( x e. w \|-> ( A +o x ) ) ) -> ( A +o suc w ) = ( A u. ran ( x e. suc w \|-> ( A +o x ) ) ) ) ) )
59		vex	\|- z e. _V
60		oalim	\|- ( ( A e. On /\ ( z e. _V /\ Lim z ) ) -> ( A +o z ) = U_ w e. z ( A +o w ) )
61	59 60	mpanr1	\|- ( ( A e. On /\ Lim z ) -> ( A +o z ) = U_ w e. z ( A +o w ) )
62	61	ancoms	\|- ( ( Lim z /\ A e. On ) -> ( A +o z ) = U_ w e. z ( A +o w ) )
63	62	adantr	\|- ( ( ( Lim z /\ A e. On ) /\ A. w e. z ( A +o w ) = ( A u. ran ( x e. w \|-> ( A +o x ) ) ) ) -> ( A +o z ) = U_ w e. z ( A +o w ) )
64		iuneq2	\|- ( A. w e. z ( A +o w ) = ( A u. ran ( x e. w \|-> ( A +o x ) ) ) -> U_ w e. z ( A +o w ) = U_ w e. z ( A u. ran ( x e. w \|-> ( A +o x ) ) ) )
65	64	adantl	\|- ( ( ( Lim z /\ A e. On ) /\ A. w e. z ( A +o w ) = ( A u. ran ( x e. w \|-> ( A +o x ) ) ) ) -> U_ w e. z ( A +o w ) = U_ w e. z ( A u. ran ( x e. w \|-> ( A +o x ) ) ) )
66		iunun	\|- U_ w e. z ( A u. ran ( x e. w \|-> ( A +o x ) ) ) = ( U_ w e. z A u. U_ w e. z ran ( x e. w \|-> ( A +o x ) ) )
67		0ellim	\|- ( Lim z -> (/) e. z )
68		ne0i	\|- ( (/) e. z -> z =/= (/) )
69		iunconst	\|- ( z =/= (/) -> U_ w e. z A = A )
70	67 68 69	3syl	\|- ( Lim z -> U_ w e. z A = A )
71		df-rex	\|- ( E. x e. w y = ( A +o x ) <-> E. x ( x e. w /\ y = ( A +o x ) ) )
72	35 71	bitri	\|- ( y e. ran ( x e. w \|-> ( A +o x ) ) <-> E. x ( x e. w /\ y = ( A +o x ) ) )
73	72	rexbii	\|- ( E. w e. z y e. ran ( x e. w \|-> ( A +o x ) ) <-> E. w e. z E. x ( x e. w /\ y = ( A +o x ) ) )
74		eluni2	\|- ( x e. U. z <-> E. w e. z x e. w )
75	74	anbi1i	\|- ( ( x e. U. z /\ y = ( A +o x ) ) <-> ( E. w e. z x e. w /\ y = ( A +o x ) ) )
76		r19.41v	\|- ( E. w e. z ( x e. w /\ y = ( A +o x ) ) <-> ( E. w e. z x e. w /\ y = ( A +o x ) ) )
77	75 76	bitr4i	\|- ( ( x e. U. z /\ y = ( A +o x ) ) <-> E. w e. z ( x e. w /\ y = ( A +o x ) ) )
78	77	exbii	\|- ( E. x ( x e. U. z /\ y = ( A +o x ) ) <-> E. x E. w e. z ( x e. w /\ y = ( A +o x ) ) )
79		df-rex	\|- ( E. x e. U. z y = ( A +o x ) <-> E. x ( x e. U. z /\ y = ( A +o x ) ) )
80		rexcom4	\|- ( E. w e. z E. x ( x e. w /\ y = ( A +o x ) ) <-> E. x E. w e. z ( x e. w /\ y = ( A +o x ) ) )
81	78 79 80	3bitr4i	\|- ( E. x e. U. z y = ( A +o x ) <-> E. w e. z E. x ( x e. w /\ y = ( A +o x ) ) )
82	73 81	bitr4i	\|- ( E. w e. z y e. ran ( x e. w \|-> ( A +o x ) ) <-> E. x e. U. z y = ( A +o x ) )
83		limuni	\|- ( Lim z -> z = U. z )
84	83	rexeqdv	\|- ( Lim z -> ( E. x e. z y = ( A +o x ) <-> E. x e. U. z y = ( A +o x ) ) )
85	82 84	bitr4id	\|- ( Lim z -> ( E. w e. z y e. ran ( x e. w \|-> ( A +o x ) ) <-> E. x e. z y = ( A +o x ) ) )
86		eliun	\|- ( y e. U_ w e. z ran ( x e. w \|-> ( A +o x ) ) <-> E. w e. z y e. ran ( x e. w \|-> ( A +o x ) ) )
87		eqid	\|- ( x e. z \|-> ( A +o x ) ) = ( x e. z \|-> ( A +o x ) )
88	87 45	elrnmpti	\|- ( y e. ran ( x e. z \|-> ( A +o x ) ) <-> E. x e. z y = ( A +o x ) )
89	85 86 88	3bitr4g	\|- ( Lim z -> ( y e. U_ w e. z ran ( x e. w \|-> ( A +o x ) ) <-> y e. ran ( x e. z \|-> ( A +o x ) ) ) )
90	89	eqrdv	\|- ( Lim z -> U_ w e. z ran ( x e. w \|-> ( A +o x ) ) = ran ( x e. z \|-> ( A +o x ) ) )
91	70 90	uneq12d	\|- ( Lim z -> ( U_ w e. z A u. U_ w e. z ran ( x e. w \|-> ( A +o x ) ) ) = ( A u. ran ( x e. z \|-> ( A +o x ) ) ) )
92	66 91	eqtrid	\|- ( Lim z -> U_ w e. z ( A u. ran ( x e. w \|-> ( A +o x ) ) ) = ( A u. ran ( x e. z \|-> ( A +o x ) ) ) )
93	92	ad2antrr	\|- ( ( ( Lim z /\ A e. On ) /\ A. w e. z ( A +o w ) = ( A u. ran ( x e. w \|-> ( A +o x ) ) ) ) -> U_ w e. z ( A u. ran ( x e. w \|-> ( A +o x ) ) ) = ( A u. ran ( x e. z \|-> ( A +o x ) ) ) )
94	63 65 93	3eqtrd	\|- ( ( ( Lim z /\ A e. On ) /\ A. w e. z ( A +o w ) = ( A u. ran ( x e. w \|-> ( A +o x ) ) ) ) -> ( A +o z ) = ( A u. ran ( x e. z \|-> ( A +o x ) ) ) )
95	94	exp31	\|- ( Lim z -> ( A e. On -> ( A. w e. z ( A +o w ) = ( A u. ran ( x e. w \|-> ( A +o x ) ) ) -> ( A +o z ) = ( A u. ran ( x e. z \|-> ( A +o x ) ) ) ) ) )
96	9 14 19 24 27 58 95	tfinds3	\|- ( B e. On -> ( A e. On -> ( A +o B ) = ( A u. ran ( x e. B \|-> ( A +o x ) ) ) ) )
97	96	impcom	\|- ( ( A e. On /\ B e. On ) -> ( A +o B ) = ( A u. ran ( x e. B \|-> ( A +o x ) ) ) )

Metamath Proof Explorer

Theorem oarec

Proof