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 ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 +o 𝐵 ) = ( 𝐴 ∪ ran ( 𝑥 ∈ 𝐵 ↦ ( 𝐴 +o 𝑥 ) ) ) )

Proof

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