Step | Hyp | Ref
| Expression |
1 | | oveq1 6556 |
. . . 4
⊢ (𝐴 = if(𝐴 ∈ ω, 𝐴, ∅) → (𝐴 +𝑜 𝐵) = (if(𝐴 ∈ ω, 𝐴, ∅) +𝑜 𝐵)) |
2 | | id 22 |
. . . 4
⊢ (𝐴 = if(𝐴 ∈ ω, 𝐴, ∅) → 𝐴 = if(𝐴 ∈ ω, 𝐴, ∅)) |
3 | 1, 2 | difeq12d 3691 |
. . 3
⊢ (𝐴 = if(𝐴 ∈ ω, 𝐴, ∅) → ((𝐴 +𝑜 𝐵) ∖ 𝐴) = ((if(𝐴 ∈ ω, 𝐴, ∅) +𝑜 𝐵) ∖ if(𝐴 ∈ ω, 𝐴, ∅))) |
4 | 3 | breq2d 4595 |
. 2
⊢ (𝐴 = if(𝐴 ∈ ω, 𝐴, ∅) → (𝐵 ≈ ((𝐴 +𝑜 𝐵) ∖ 𝐴) ↔ 𝐵 ≈ ((if(𝐴 ∈ ω, 𝐴, ∅) +𝑜 𝐵) ∖ if(𝐴 ∈ ω, 𝐴, ∅)))) |
5 | | id 22 |
. . 3
⊢ (𝐵 = if(𝐵 ∈ ω, 𝐵, ∅) → 𝐵 = if(𝐵 ∈ ω, 𝐵, ∅)) |
6 | | oveq2 6557 |
. . . 4
⊢ (𝐵 = if(𝐵 ∈ ω, 𝐵, ∅) → (if(𝐴 ∈ ω, 𝐴, ∅) +𝑜 𝐵) = (if(𝐴 ∈ ω, 𝐴, ∅) +𝑜 if(𝐵 ∈ ω, 𝐵, ∅))) |
7 | 6 | difeq1d 3689 |
. . 3
⊢ (𝐵 = if(𝐵 ∈ ω, 𝐵, ∅) → ((if(𝐴 ∈ ω, 𝐴, ∅) +𝑜 𝐵) ∖ if(𝐴 ∈ ω, 𝐴, ∅)) = ((if(𝐴 ∈ ω, 𝐴, ∅) +𝑜 if(𝐵 ∈ ω, 𝐵, ∅)) ∖ if(𝐴 ∈ ω, 𝐴, ∅))) |
8 | 5, 7 | breq12d 4596 |
. 2
⊢ (𝐵 = if(𝐵 ∈ ω, 𝐵, ∅) → (𝐵 ≈ ((if(𝐴 ∈ ω, 𝐴, ∅) +𝑜 𝐵) ∖ if(𝐴 ∈ ω, 𝐴, ∅)) ↔ if(𝐵 ∈ ω, 𝐵, ∅) ≈ ((if(𝐴 ∈ ω, 𝐴, ∅) +𝑜 if(𝐵 ∈ ω, 𝐵, ∅)) ∖ if(𝐴 ∈ ω, 𝐴, ∅)))) |
9 | | peano1 6977 |
. . . 4
⊢ ∅
∈ ω |
10 | 9 | elimel 4100 |
. . 3
⊢ if(𝐵 ∈ ω, 𝐵, ∅) ∈
ω |
11 | | ovex 6577 |
. . . 4
⊢ (if(𝐴 ∈ ω, 𝐴, ∅) +𝑜
if(𝐵 ∈ ω, 𝐵, ∅)) ∈
V |
12 | | difexg 4735 |
. . . 4
⊢
((if(𝐴 ∈
ω, 𝐴, ∅)
+𝑜 if(𝐵
∈ ω, 𝐵,
∅)) ∈ V → ((if(𝐴 ∈ ω, 𝐴, ∅) +𝑜 if(𝐵 ∈ ω, 𝐵, ∅)) ∖ if(𝐴 ∈ ω, 𝐴, ∅)) ∈
V) |
13 | 11, 12 | ax-mp 5 |
. . 3
⊢
((if(𝐴 ∈
ω, 𝐴, ∅)
+𝑜 if(𝐵
∈ ω, 𝐵,
∅)) ∖ if(𝐴
∈ ω, 𝐴,
∅)) ∈ V |
14 | 9 | elimel 4100 |
. . . 4
⊢ if(𝐴 ∈ ω, 𝐴, ∅) ∈
ω |
15 | | eqid 2610 |
. . . 4
⊢ (𝑥 ∈ if(𝐵 ∈ ω, 𝐵, ∅) ↦ (if(𝐴 ∈ ω, 𝐴, ∅) +𝑜 𝑥)) = (𝑥 ∈ if(𝐵 ∈ ω, 𝐵, ∅) ↦ (if(𝐴 ∈ ω, 𝐴, ∅) +𝑜 𝑥)) |
16 | 14, 10, 15 | unfilem2 8110 |
. . 3
⊢ (𝑥 ∈ if(𝐵 ∈ ω, 𝐵, ∅) ↦ (if(𝐴 ∈ ω, 𝐴, ∅) +𝑜 𝑥)):if(𝐵 ∈ ω, 𝐵, ∅)–1-1-onto→((if(𝐴 ∈ ω, 𝐴, ∅) +𝑜 if(𝐵 ∈ ω, 𝐵, ∅)) ∖ if(𝐴 ∈ ω, 𝐴, ∅)) |
17 | | f1oen2g 7858 |
. . 3
⊢
((if(𝐵 ∈
ω, 𝐵, ∅) ∈
ω ∧ ((if(𝐴 ∈
ω, 𝐴, ∅)
+𝑜 if(𝐵
∈ ω, 𝐵,
∅)) ∖ if(𝐴
∈ ω, 𝐴,
∅)) ∈ V ∧ (𝑥
∈ if(𝐵 ∈ ω,
𝐵, ∅) ↦
(if(𝐴 ∈ ω, 𝐴, ∅) +𝑜
𝑥)):if(𝐵 ∈ ω, 𝐵, ∅)–1-1-onto→((if(𝐴 ∈ ω, 𝐴, ∅) +𝑜 if(𝐵 ∈ ω, 𝐵, ∅)) ∖ if(𝐴 ∈ ω, 𝐴, ∅))) → if(𝐵 ∈ ω, 𝐵, ∅) ≈ ((if(𝐴 ∈ ω, 𝐴, ∅) +𝑜
if(𝐵 ∈ ω, 𝐵, ∅)) ∖ if(𝐴 ∈ ω, 𝐴, ∅))) |
18 | 10, 13, 16, 17 | mp3an 1416 |
. 2
⊢ if(𝐵 ∈ ω, 𝐵, ∅) ≈ ((if(𝐴 ∈ ω, 𝐴, ∅) +𝑜
if(𝐵 ∈ ω, 𝐵, ∅)) ∖ if(𝐴 ∈ ω, 𝐴, ∅)) |
19 | 4, 8, 18 | dedth2h 4090 |
1
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → 𝐵 ≈ ((𝐴 +𝑜 𝐵) ∖ 𝐴)) |