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∈On∧B∈On→A+𝑜B=A∪ran⁡x∈B⟼A+𝑜x

Proof

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