Step | Hyp | Ref
| Expression |
1 | | oafnex 6024 |
. . 3
⊢ (𝑦 ∈ V ↦ suc 𝑦) Fn V |
2 | | rdgival 5969 |
. . 3
⊢ (((𝑦 ∈ V ↦ suc 𝑦) Fn V ∧ 𝐴 ∈ On ∧ 𝐵 ∈ On) → (rec((𝑦 ∈ V ↦ suc 𝑦), 𝐴)‘𝐵) = (𝐴 ∪ ∪
𝑥 ∈ 𝐵 ((𝑦 ∈ V ↦ suc 𝑦)‘(rec((𝑦 ∈ V ↦ suc 𝑦), 𝐴)‘𝑥)))) |
3 | 1, 2 | mp3an1 1219 |
. 2
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (rec((𝑦 ∈ V ↦ suc 𝑦), 𝐴)‘𝐵) = (𝐴 ∪ ∪
𝑥 ∈ 𝐵 ((𝑦 ∈ V ↦ suc 𝑦)‘(rec((𝑦 ∈ V ↦ suc 𝑦), 𝐴)‘𝑥)))) |
4 | | oav 6034 |
. 2
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 +𝑜 𝐵) = (rec((𝑦 ∈ V ↦ suc 𝑦), 𝐴)‘𝐵)) |
5 | | onelon 4121 |
. . . . . 6
⊢ ((𝐵 ∈ On ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ On) |
6 | | vex 2560 |
. . . . . . . . . 10
⊢ 𝑥 ∈ V |
7 | | oaexg 6028 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ V) → (𝐴 +𝑜 𝑥) ∈ V) |
8 | 6, 7 | mpan2 401 |
. . . . . . . . 9
⊢ (𝐴 ∈ On → (𝐴 +𝑜 𝑥) ∈ V) |
9 | | sucexg 4224 |
. . . . . . . . . 10
⊢ ((𝐴 +𝑜 𝑥) ∈ V → suc (𝐴 +𝑜 𝑥) ∈ V) |
10 | 8, 9 | syl 14 |
. . . . . . . . 9
⊢ (𝐴 ∈ On → suc (𝐴 +𝑜 𝑥) ∈ V) |
11 | | suceq 4139 |
. . . . . . . . . 10
⊢ (𝑦 = (𝐴 +𝑜 𝑥) → suc 𝑦 = suc (𝐴 +𝑜 𝑥)) |
12 | | eqid 2040 |
. . . . . . . . . 10
⊢ (𝑦 ∈ V ↦ suc 𝑦) = (𝑦 ∈ V ↦ suc 𝑦) |
13 | 11, 12 | fvmptg 5248 |
. . . . . . . . 9
⊢ (((𝐴 +𝑜 𝑥) ∈ V ∧ suc (𝐴 +𝑜 𝑥) ∈ V) → ((𝑦 ∈ V ↦ suc 𝑦)‘(𝐴 +𝑜 𝑥)) = suc (𝐴 +𝑜 𝑥)) |
14 | 8, 10, 13 | syl2anc 391 |
. . . . . . . 8
⊢ (𝐴 ∈ On → ((𝑦 ∈ V ↦ suc 𝑦)‘(𝐴 +𝑜 𝑥)) = suc (𝐴 +𝑜 𝑥)) |
15 | 14 | adantr 261 |
. . . . . . 7
⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ On) → ((𝑦 ∈ V ↦ suc 𝑦)‘(𝐴 +𝑜 𝑥)) = suc (𝐴 +𝑜 𝑥)) |
16 | | oav 6034 |
. . . . . . . 8
⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ On) → (𝐴 +𝑜 𝑥) = (rec((𝑦 ∈ V ↦ suc 𝑦), 𝐴)‘𝑥)) |
17 | 16 | fveq2d 5182 |
. . . . . . 7
⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ On) → ((𝑦 ∈ V ↦ suc 𝑦)‘(𝐴 +𝑜 𝑥)) = ((𝑦 ∈ V ↦ suc 𝑦)‘(rec((𝑦 ∈ V ↦ suc 𝑦), 𝐴)‘𝑥))) |
18 | 15, 17 | eqtr3d 2074 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ On) → suc (𝐴 +𝑜 𝑥) = ((𝑦 ∈ V ↦ suc 𝑦)‘(rec((𝑦 ∈ V ↦ suc 𝑦), 𝐴)‘𝑥))) |
19 | 5, 18 | sylan2 270 |
. . . . 5
⊢ ((𝐴 ∈ On ∧ (𝐵 ∈ On ∧ 𝑥 ∈ 𝐵)) → suc (𝐴 +𝑜 𝑥) = ((𝑦 ∈ V ↦ suc 𝑦)‘(rec((𝑦 ∈ V ↦ suc 𝑦), 𝐴)‘𝑥))) |
20 | 19 | anassrs 380 |
. . . 4
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑥 ∈ 𝐵) → suc (𝐴 +𝑜 𝑥) = ((𝑦 ∈ V ↦ suc 𝑦)‘(rec((𝑦 ∈ V ↦ suc 𝑦), 𝐴)‘𝑥))) |
21 | 20 | iuneq2dv 3678 |
. . 3
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ∪ 𝑥 ∈ 𝐵 suc (𝐴 +𝑜 𝑥) = ∪ 𝑥 ∈ 𝐵 ((𝑦 ∈ V ↦ suc 𝑦)‘(rec((𝑦 ∈ V ↦ suc 𝑦), 𝐴)‘𝑥))) |
22 | 21 | uneq2d 3097 |
. 2
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ∪ ∪ 𝑥 ∈ 𝐵 suc (𝐴 +𝑜 𝑥)) = (𝐴 ∪ ∪
𝑥 ∈ 𝐵 ((𝑦 ∈ V ↦ suc 𝑦)‘(rec((𝑦 ∈ V ↦ suc 𝑦), 𝐴)‘𝑥)))) |
23 | 3, 4, 22 | 3eqtr4d 2082 |
1
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 +𝑜 𝐵) = (𝐴 ∪ ∪
𝑥 ∈ 𝐵 suc (𝐴 +𝑜 𝑥))) |