Metamath Proof Explorer

Theorem 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 syl5ibr 
 |-  ( ( 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 ) ) ) )