| Step | Hyp | Ref
| Expression |
| 1 | | nnaordex 8676 |
. 2
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ∈ 𝐵 ↔ ∃𝑦 ∈ ω (∅ ∈ 𝑦 ∧ (𝐴 +o 𝑦) = 𝐵))) |
| 2 | | nn0suc 7916 |
. . . . . . 7
⊢ (𝑦 ∈ ω → (𝑦 = ∅ ∨ ∃𝑥 ∈ ω 𝑦 = suc 𝑥)) |
| 3 | 2 | ad2antrl 728 |
. . . . . 6
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ (𝑦 ∈ ω ∧ (∅
∈ 𝑦 ∧ (𝐴 +o 𝑦) = 𝐵))) → (𝑦 = ∅ ∨ ∃𝑥 ∈ ω 𝑦 = suc 𝑥)) |
| 4 | | simprrl 781 |
. . . . . . 7
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ (𝑦 ∈ ω ∧ (∅
∈ 𝑦 ∧ (𝐴 +o 𝑦) = 𝐵))) → ∅ ∈ 𝑦) |
| 5 | | n0i 4340 |
. . . . . . 7
⊢ (∅
∈ 𝑦 → ¬ 𝑦 = ∅) |
| 6 | 4, 5 | syl 17 |
. . . . . 6
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ (𝑦 ∈ ω ∧ (∅
∈ 𝑦 ∧ (𝐴 +o 𝑦) = 𝐵))) → ¬ 𝑦 = ∅) |
| 7 | 3, 6 | orcnd 879 |
. . . . 5
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ (𝑦 ∈ ω ∧ (∅
∈ 𝑦 ∧ (𝐴 +o 𝑦) = 𝐵))) → ∃𝑥 ∈ ω 𝑦 = suc 𝑥) |
| 8 | | simprrr 782 |
. . . . . . 7
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ (𝑦 ∈ ω ∧ (∅
∈ 𝑦 ∧ (𝐴 +o 𝑦) = 𝐵))) → (𝐴 +o 𝑦) = 𝐵) |
| 9 | | oveq2 7439 |
. . . . . . . 8
⊢ (𝑦 = suc 𝑥 → (𝐴 +o 𝑦) = (𝐴 +o suc 𝑥)) |
| 10 | 9 | eqeq1d 2739 |
. . . . . . 7
⊢ (𝑦 = suc 𝑥 → ((𝐴 +o 𝑦) = 𝐵 ↔ (𝐴 +o suc 𝑥) = 𝐵)) |
| 11 | 8, 10 | syl5ibcom 245 |
. . . . . 6
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ (𝑦 ∈ ω ∧ (∅
∈ 𝑦 ∧ (𝐴 +o 𝑦) = 𝐵))) → (𝑦 = suc 𝑥 → (𝐴 +o suc 𝑥) = 𝐵)) |
| 12 | 11 | reximdv 3170 |
. . . . 5
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ (𝑦 ∈ ω ∧ (∅
∈ 𝑦 ∧ (𝐴 +o 𝑦) = 𝐵))) → (∃𝑥 ∈ ω 𝑦 = suc 𝑥 → ∃𝑥 ∈ ω (𝐴 +o suc 𝑥) = 𝐵)) |
| 13 | 7, 12 | mpd 15 |
. . . 4
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ (𝑦 ∈ ω ∧ (∅
∈ 𝑦 ∧ (𝐴 +o 𝑦) = 𝐵))) → ∃𝑥 ∈ ω (𝐴 +o suc 𝑥) = 𝐵) |
| 14 | 13 | rexlimdvaa 3156 |
. . 3
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) →
(∃𝑦 ∈ ω
(∅ ∈ 𝑦 ∧
(𝐴 +o 𝑦) = 𝐵) → ∃𝑥 ∈ ω (𝐴 +o suc 𝑥) = 𝐵)) |
| 15 | | peano2 7912 |
. . . . . 6
⊢ (𝑥 ∈ ω → suc 𝑥 ∈
ω) |
| 16 | 15 | ad2antrl 728 |
. . . . 5
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ (𝑥 ∈ ω ∧ (𝐴 +o suc 𝑥) = 𝐵)) → suc 𝑥 ∈ ω) |
| 17 | | nnord 7895 |
. . . . . . 7
⊢ (𝑥 ∈ ω → Ord 𝑥) |
| 18 | 17 | ad2antrl 728 |
. . . . . 6
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ (𝑥 ∈ ω ∧ (𝐴 +o suc 𝑥) = 𝐵)) → Ord 𝑥) |
| 19 | | 0elsuc 7855 |
. . . . . 6
⊢ (Ord
𝑥 → ∅ ∈ suc
𝑥) |
| 20 | 18, 19 | syl 17 |
. . . . 5
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ (𝑥 ∈ ω ∧ (𝐴 +o suc 𝑥) = 𝐵)) → ∅ ∈ suc 𝑥) |
| 21 | | simprr 773 |
. . . . 5
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ (𝑥 ∈ ω ∧ (𝐴 +o suc 𝑥) = 𝐵)) → (𝐴 +o suc 𝑥) = 𝐵) |
| 22 | | eleq2 2830 |
. . . . . . 7
⊢ (𝑦 = suc 𝑥 → (∅ ∈ 𝑦 ↔ ∅ ∈ suc 𝑥)) |
| 23 | 22, 10 | anbi12d 632 |
. . . . . 6
⊢ (𝑦 = suc 𝑥 → ((∅ ∈ 𝑦 ∧ (𝐴 +o 𝑦) = 𝐵) ↔ (∅ ∈ suc 𝑥 ∧ (𝐴 +o suc 𝑥) = 𝐵))) |
| 24 | 23 | rspcev 3622 |
. . . . 5
⊢ ((suc
𝑥 ∈ ω ∧
(∅ ∈ suc 𝑥 ∧
(𝐴 +o suc 𝑥) = 𝐵)) → ∃𝑦 ∈ ω (∅ ∈ 𝑦 ∧ (𝐴 +o 𝑦) = 𝐵)) |
| 25 | 16, 20, 21, 24 | syl12anc 837 |
. . . 4
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ (𝑥 ∈ ω ∧ (𝐴 +o suc 𝑥) = 𝐵)) → ∃𝑦 ∈ ω (∅ ∈ 𝑦 ∧ (𝐴 +o 𝑦) = 𝐵)) |
| 26 | 25 | rexlimdvaa 3156 |
. . 3
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) →
(∃𝑥 ∈ ω
(𝐴 +o suc 𝑥) = 𝐵 → ∃𝑦 ∈ ω (∅ ∈ 𝑦 ∧ (𝐴 +o 𝑦) = 𝐵))) |
| 27 | 14, 26 | impbid 212 |
. 2
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) →
(∃𝑦 ∈ ω
(∅ ∈ 𝑦 ∧
(𝐴 +o 𝑦) = 𝐵) ↔ ∃𝑥 ∈ ω (𝐴 +o suc 𝑥) = 𝐵)) |
| 28 | 1, 27 | bitrd 279 |
1
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ∈ 𝐵 ↔ ∃𝑥 ∈ ω (𝐴 +o suc 𝑥) = 𝐵)) |