| Step | Hyp | Ref
| Expression |
| 1 | | peano2 7912 |
. . . . . 6
⊢ (𝐴 ∈ ω → suc 𝐴 ∈
ω) |
| 2 | | nnawordex 8675 |
. . . . . 6
⊢ ((suc
𝐴 ∈ ω ∧
𝐵 ∈ ω) →
(suc 𝐴 ⊆ 𝐵 ↔ ∃𝑦 ∈ ω (suc 𝐴 +o 𝑦) = 𝐵)) |
| 3 | 1, 2 | sylan 580 |
. . . . 5
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (suc
𝐴 ⊆ 𝐵 ↔ ∃𝑦 ∈ ω (suc 𝐴 +o 𝑦) = 𝐵)) |
| 4 | | nnacl 8649 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ω ∧ 𝑦 ∈ ω) → (𝐴 +o 𝑦) ∈
ω) |
| 5 | | nnaword1 8667 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ω ∧ 𝑦 ∈ ω) → 𝐴 ⊆ (𝐴 +o 𝑦)) |
| 6 | | nnasuc 8644 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ω ∧ 𝐴 ∈ ω) → (𝑦 +o suc 𝐴) = suc (𝑦 +o 𝐴)) |
| 7 | 6 | ancoms 458 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ω ∧ 𝑦 ∈ ω) → (𝑦 +o suc 𝐴) = suc (𝑦 +o 𝐴)) |
| 8 | | nnacom 8655 |
. . . . . . . . . . 11
⊢ ((suc
𝐴 ∈ ω ∧
𝑦 ∈ ω) →
(suc 𝐴 +o 𝑦) = (𝑦 +o suc 𝐴)) |
| 9 | 1, 8 | sylan 580 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ω ∧ 𝑦 ∈ ω) → (suc
𝐴 +o 𝑦) = (𝑦 +o suc 𝐴)) |
| 10 | | nnacom 8655 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ω ∧ 𝑦 ∈ ω) → (𝐴 +o 𝑦) = (𝑦 +o 𝐴)) |
| 11 | | suceq 6450 |
. . . . . . . . . . 11
⊢ ((𝐴 +o 𝑦) = (𝑦 +o 𝐴) → suc (𝐴 +o 𝑦) = suc (𝑦 +o 𝐴)) |
| 12 | 10, 11 | syl 17 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ω ∧ 𝑦 ∈ ω) → suc
(𝐴 +o 𝑦) = suc (𝑦 +o 𝐴)) |
| 13 | 7, 9, 12 | 3eqtr4d 2787 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ω ∧ 𝑦 ∈ ω) → (suc
𝐴 +o 𝑦) = suc (𝐴 +o 𝑦)) |
| 14 | | sseq2 4010 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝐴 +o 𝑦) → (𝐴 ⊆ 𝑥 ↔ 𝐴 ⊆ (𝐴 +o 𝑦))) |
| 15 | | suceq 6450 |
. . . . . . . . . . . 12
⊢ (𝑥 = (𝐴 +o 𝑦) → suc 𝑥 = suc (𝐴 +o 𝑦)) |
| 16 | 15 | eqeq2d 2748 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝐴 +o 𝑦) → ((suc 𝐴 +o 𝑦) = suc 𝑥 ↔ (suc 𝐴 +o 𝑦) = suc (𝐴 +o 𝑦))) |
| 17 | 14, 16 | anbi12d 632 |
. . . . . . . . . 10
⊢ (𝑥 = (𝐴 +o 𝑦) → ((𝐴 ⊆ 𝑥 ∧ (suc 𝐴 +o 𝑦) = suc 𝑥) ↔ (𝐴 ⊆ (𝐴 +o 𝑦) ∧ (suc 𝐴 +o 𝑦) = suc (𝐴 +o 𝑦)))) |
| 18 | 17 | rspcev 3622 |
. . . . . . . . 9
⊢ (((𝐴 +o 𝑦) ∈ ω ∧ (𝐴 ⊆ (𝐴 +o 𝑦) ∧ (suc 𝐴 +o 𝑦) = suc (𝐴 +o 𝑦))) → ∃𝑥 ∈ ω (𝐴 ⊆ 𝑥 ∧ (suc 𝐴 +o 𝑦) = suc 𝑥)) |
| 19 | 4, 5, 13, 18 | syl12anc 837 |
. . . . . . . 8
⊢ ((𝐴 ∈ ω ∧ 𝑦 ∈ ω) →
∃𝑥 ∈ ω
(𝐴 ⊆ 𝑥 ∧ (suc 𝐴 +o 𝑦) = suc 𝑥)) |
| 20 | | eqeq1 2741 |
. . . . . . . . . 10
⊢ ((suc
𝐴 +o 𝑦) = 𝐵 → ((suc 𝐴 +o 𝑦) = suc 𝑥 ↔ 𝐵 = suc 𝑥)) |
| 21 | 20 | anbi2d 630 |
. . . . . . . . 9
⊢ ((suc
𝐴 +o 𝑦) = 𝐵 → ((𝐴 ⊆ 𝑥 ∧ (suc 𝐴 +o 𝑦) = suc 𝑥) ↔ (𝐴 ⊆ 𝑥 ∧ 𝐵 = suc 𝑥))) |
| 22 | 21 | rexbidv 3179 |
. . . . . . . 8
⊢ ((suc
𝐴 +o 𝑦) = 𝐵 → (∃𝑥 ∈ ω (𝐴 ⊆ 𝑥 ∧ (suc 𝐴 +o 𝑦) = suc 𝑥) ↔ ∃𝑥 ∈ ω (𝐴 ⊆ 𝑥 ∧ 𝐵 = suc 𝑥))) |
| 23 | 19, 22 | syl5ibcom 245 |
. . . . . . 7
⊢ ((𝐴 ∈ ω ∧ 𝑦 ∈ ω) → ((suc
𝐴 +o 𝑦) = 𝐵 → ∃𝑥 ∈ ω (𝐴 ⊆ 𝑥 ∧ 𝐵 = suc 𝑥))) |
| 24 | 23 | rexlimdva 3155 |
. . . . . 6
⊢ (𝐴 ∈ ω →
(∃𝑦 ∈ ω
(suc 𝐴 +o 𝑦) = 𝐵 → ∃𝑥 ∈ ω (𝐴 ⊆ 𝑥 ∧ 𝐵 = suc 𝑥))) |
| 25 | 24 | adantr 480 |
. . . . 5
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) →
(∃𝑦 ∈ ω
(suc 𝐴 +o 𝑦) = 𝐵 → ∃𝑥 ∈ ω (𝐴 ⊆ 𝑥 ∧ 𝐵 = suc 𝑥))) |
| 26 | 3, 25 | sylbid 240 |
. . . 4
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (suc
𝐴 ⊆ 𝐵 → ∃𝑥 ∈ ω (𝐴 ⊆ 𝑥 ∧ 𝐵 = suc 𝑥))) |
| 27 | 26 | expimpd 453 |
. . 3
⊢ (𝐴 ∈ ω → ((𝐵 ∈ ω ∧ suc 𝐴 ⊆ 𝐵) → ∃𝑥 ∈ ω (𝐴 ⊆ 𝑥 ∧ 𝐵 = suc 𝑥))) |
| 28 | | peano2 7912 |
. . . . . . . 8
⊢ (𝑥 ∈ ω → suc 𝑥 ∈
ω) |
| 29 | 28 | ad2antlr 727 |
. . . . . . 7
⊢ (((𝐴 ∈ ω ∧ 𝑥 ∈ ω) ∧ 𝐴 ⊆ 𝑥) → suc 𝑥 ∈ ω) |
| 30 | | nnord 7895 |
. . . . . . . . 9
⊢ (𝐴 ∈ ω → Ord 𝐴) |
| 31 | | nnord 7895 |
. . . . . . . . 9
⊢ (𝑥 ∈ ω → Ord 𝑥) |
| 32 | | ordsucsssuc 7843 |
. . . . . . . . 9
⊢ ((Ord
𝐴 ∧ Ord 𝑥) → (𝐴 ⊆ 𝑥 ↔ suc 𝐴 ⊆ suc 𝑥)) |
| 33 | 30, 31, 32 | syl2an 596 |
. . . . . . . 8
⊢ ((𝐴 ∈ ω ∧ 𝑥 ∈ ω) → (𝐴 ⊆ 𝑥 ↔ suc 𝐴 ⊆ suc 𝑥)) |
| 34 | 33 | biimpa 476 |
. . . . . . 7
⊢ (((𝐴 ∈ ω ∧ 𝑥 ∈ ω) ∧ 𝐴 ⊆ 𝑥) → suc 𝐴 ⊆ suc 𝑥) |
| 35 | 29, 34 | jca 511 |
. . . . . 6
⊢ (((𝐴 ∈ ω ∧ 𝑥 ∈ ω) ∧ 𝐴 ⊆ 𝑥) → (suc 𝑥 ∈ ω ∧ suc 𝐴 ⊆ suc 𝑥)) |
| 36 | | eleq1 2829 |
. . . . . . 7
⊢ (𝐵 = suc 𝑥 → (𝐵 ∈ ω ↔ suc 𝑥 ∈
ω)) |
| 37 | | sseq2 4010 |
. . . . . . 7
⊢ (𝐵 = suc 𝑥 → (suc 𝐴 ⊆ 𝐵 ↔ suc 𝐴 ⊆ suc 𝑥)) |
| 38 | 36, 37 | anbi12d 632 |
. . . . . 6
⊢ (𝐵 = suc 𝑥 → ((𝐵 ∈ ω ∧ suc 𝐴 ⊆ 𝐵) ↔ (suc 𝑥 ∈ ω ∧ suc 𝐴 ⊆ suc 𝑥))) |
| 39 | 35, 38 | syl5ibrcom 247 |
. . . . 5
⊢ (((𝐴 ∈ ω ∧ 𝑥 ∈ ω) ∧ 𝐴 ⊆ 𝑥) → (𝐵 = suc 𝑥 → (𝐵 ∈ ω ∧ suc 𝐴 ⊆ 𝐵))) |
| 40 | 39 | expimpd 453 |
. . . 4
⊢ ((𝐴 ∈ ω ∧ 𝑥 ∈ ω) → ((𝐴 ⊆ 𝑥 ∧ 𝐵 = suc 𝑥) → (𝐵 ∈ ω ∧ suc 𝐴 ⊆ 𝐵))) |
| 41 | 40 | rexlimdva 3155 |
. . 3
⊢ (𝐴 ∈ ω →
(∃𝑥 ∈ ω
(𝐴 ⊆ 𝑥 ∧ 𝐵 = suc 𝑥) → (𝐵 ∈ ω ∧ suc 𝐴 ⊆ 𝐵))) |
| 42 | 27, 41 | impbid 212 |
. 2
⊢ (𝐴 ∈ ω → ((𝐵 ∈ ω ∧ suc 𝐴 ⊆ 𝐵) ↔ ∃𝑥 ∈ ω (𝐴 ⊆ 𝑥 ∧ 𝐵 = suc 𝑥))) |
| 43 | | eldif 3961 |
. . 3
⊢ (𝐵 ∈ (ω ∖ suc
𝐴) ↔ (𝐵 ∈ ω ∧ ¬
𝐵 ∈ suc 𝐴)) |
| 44 | | nnord 7895 |
. . . . . 6
⊢ (suc
𝐴 ∈ ω → Ord
suc 𝐴) |
| 45 | 1, 44 | syl 17 |
. . . . 5
⊢ (𝐴 ∈ ω → Ord suc
𝐴) |
| 46 | | nnord 7895 |
. . . . 5
⊢ (𝐵 ∈ ω → Ord 𝐵) |
| 47 | | ordtri1 6417 |
. . . . 5
⊢ ((Ord suc
𝐴 ∧ Ord 𝐵) → (suc 𝐴 ⊆ 𝐵 ↔ ¬ 𝐵 ∈ suc 𝐴)) |
| 48 | 45, 46, 47 | syl2an 596 |
. . . 4
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (suc
𝐴 ⊆ 𝐵 ↔ ¬ 𝐵 ∈ suc 𝐴)) |
| 49 | 48 | pm5.32da 579 |
. . 3
⊢ (𝐴 ∈ ω → ((𝐵 ∈ ω ∧ suc 𝐴 ⊆ 𝐵) ↔ (𝐵 ∈ ω ∧ ¬ 𝐵 ∈ suc 𝐴))) |
| 50 | 43, 49 | bitr4id 290 |
. 2
⊢ (𝐴 ∈ ω → (𝐵 ∈ (ω ∖ suc
𝐴) ↔ (𝐵 ∈ ω ∧ suc 𝐴 ⊆ 𝐵))) |
| 51 | | eldif 3961 |
. . . . . 6
⊢ (𝑥 ∈ (ω ∖ 𝐴) ↔ (𝑥 ∈ ω ∧ ¬ 𝑥 ∈ 𝐴)) |
| 52 | 51 | anbi1i 624 |
. . . . 5
⊢ ((𝑥 ∈ (ω ∖ 𝐴) ∧ 𝐵 = suc 𝑥) ↔ ((𝑥 ∈ ω ∧ ¬ 𝑥 ∈ 𝐴) ∧ 𝐵 = suc 𝑥)) |
| 53 | | anass 468 |
. . . . 5
⊢ (((𝑥 ∈ ω ∧ ¬
𝑥 ∈ 𝐴) ∧ 𝐵 = suc 𝑥) ↔ (𝑥 ∈ ω ∧ (¬ 𝑥 ∈ 𝐴 ∧ 𝐵 = suc 𝑥))) |
| 54 | 52, 53 | bitri 275 |
. . . 4
⊢ ((𝑥 ∈ (ω ∖ 𝐴) ∧ 𝐵 = suc 𝑥) ↔ (𝑥 ∈ ω ∧ (¬ 𝑥 ∈ 𝐴 ∧ 𝐵 = suc 𝑥))) |
| 55 | 54 | rexbii2 3090 |
. . 3
⊢
(∃𝑥 ∈
(ω ∖ 𝐴)𝐵 = suc 𝑥 ↔ ∃𝑥 ∈ ω (¬ 𝑥 ∈ 𝐴 ∧ 𝐵 = suc 𝑥)) |
| 56 | | ordtri1 6417 |
. . . . . 6
⊢ ((Ord
𝐴 ∧ Ord 𝑥) → (𝐴 ⊆ 𝑥 ↔ ¬ 𝑥 ∈ 𝐴)) |
| 57 | 30, 31, 56 | syl2an 596 |
. . . . 5
⊢ ((𝐴 ∈ ω ∧ 𝑥 ∈ ω) → (𝐴 ⊆ 𝑥 ↔ ¬ 𝑥 ∈ 𝐴)) |
| 58 | 57 | anbi1d 631 |
. . . 4
⊢ ((𝐴 ∈ ω ∧ 𝑥 ∈ ω) → ((𝐴 ⊆ 𝑥 ∧ 𝐵 = suc 𝑥) ↔ (¬ 𝑥 ∈ 𝐴 ∧ 𝐵 = suc 𝑥))) |
| 59 | 58 | rexbidva 3177 |
. . 3
⊢ (𝐴 ∈ ω →
(∃𝑥 ∈ ω
(𝐴 ⊆ 𝑥 ∧ 𝐵 = suc 𝑥) ↔ ∃𝑥 ∈ ω (¬ 𝑥 ∈ 𝐴 ∧ 𝐵 = suc 𝑥))) |
| 60 | 55, 59 | bitr4id 290 |
. 2
⊢ (𝐴 ∈ ω →
(∃𝑥 ∈ (ω
∖ 𝐴)𝐵 = suc 𝑥 ↔ ∃𝑥 ∈ ω (𝐴 ⊆ 𝑥 ∧ 𝐵 = suc 𝑥))) |
| 61 | 42, 50, 60 | 3bitr4d 311 |
1
⊢ (𝐴 ∈ ω → (𝐵 ∈ (ω ∖ suc
𝐴) ↔ ∃𝑥 ∈ (ω ∖ 𝐴)𝐵 = suc 𝑥)) |