| Step | Hyp | Ref
| Expression |
| 1 | | sssucid 6464 |
. . 3
⊢ 𝐵 ⊆ suc 𝐵 |
| 2 | | sstr2 3990 |
. . 3
⊢ (𝐴 ⊆ 𝐵 → (𝐵 ⊆ suc 𝐵 → 𝐴 ⊆ suc 𝐵)) |
| 3 | 1, 2 | mpi 20 |
. 2
⊢ (𝐴 ⊆ 𝐵 → 𝐴 ⊆ suc 𝐵) |
| 4 | | eleq1 2829 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝐵 → (𝑥 ∈ 𝐴 ↔ 𝐵 ∈ 𝐴)) |
| 5 | 4 | biimpcd 249 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝐴 → (𝑥 = 𝐵 → 𝐵 ∈ 𝐴)) |
| 6 | | limsuc 7870 |
. . . . . . . . . . . . . 14
⊢ (Lim
𝐴 → (𝐵 ∈ 𝐴 ↔ suc 𝐵 ∈ 𝐴)) |
| 7 | 6 | biimpa 476 |
. . . . . . . . . . . . 13
⊢ ((Lim
𝐴 ∧ 𝐵 ∈ 𝐴) → suc 𝐵 ∈ 𝐴) |
| 8 | | limord 6444 |
. . . . . . . . . . . . . . 15
⊢ (Lim
𝐴 → Ord 𝐴) |
| 9 | | ordelord 6406 |
. . . . . . . . . . . . . . . . 17
⊢ ((Ord
𝐴 ∧ 𝐵 ∈ 𝐴) → Ord 𝐵) |
| 10 | 8, 9 | sylan 580 |
. . . . . . . . . . . . . . . 16
⊢ ((Lim
𝐴 ∧ 𝐵 ∈ 𝐴) → Ord 𝐵) |
| 11 | | ordsuc 7833 |
. . . . . . . . . . . . . . . 16
⊢ (Ord
𝐵 ↔ Ord suc 𝐵) |
| 12 | 10, 11 | sylib 218 |
. . . . . . . . . . . . . . 15
⊢ ((Lim
𝐴 ∧ 𝐵 ∈ 𝐴) → Ord suc 𝐵) |
| 13 | | ordtri1 6417 |
. . . . . . . . . . . . . . 15
⊢ ((Ord
𝐴 ∧ Ord suc 𝐵) → (𝐴 ⊆ suc 𝐵 ↔ ¬ suc 𝐵 ∈ 𝐴)) |
| 14 | 8, 12, 13 | syl2an2r 685 |
. . . . . . . . . . . . . 14
⊢ ((Lim
𝐴 ∧ 𝐵 ∈ 𝐴) → (𝐴 ⊆ suc 𝐵 ↔ ¬ suc 𝐵 ∈ 𝐴)) |
| 15 | 14 | con2bid 354 |
. . . . . . . . . . . . 13
⊢ ((Lim
𝐴 ∧ 𝐵 ∈ 𝐴) → (suc 𝐵 ∈ 𝐴 ↔ ¬ 𝐴 ⊆ suc 𝐵)) |
| 16 | 7, 15 | mpbid 232 |
. . . . . . . . . . . 12
⊢ ((Lim
𝐴 ∧ 𝐵 ∈ 𝐴) → ¬ 𝐴 ⊆ suc 𝐵) |
| 17 | 16 | ex 412 |
. . . . . . . . . . 11
⊢ (Lim
𝐴 → (𝐵 ∈ 𝐴 → ¬ 𝐴 ⊆ suc 𝐵)) |
| 18 | 5, 17 | sylan9r 508 |
. . . . . . . . . 10
⊢ ((Lim
𝐴 ∧ 𝑥 ∈ 𝐴) → (𝑥 = 𝐵 → ¬ 𝐴 ⊆ suc 𝐵)) |
| 19 | 18 | con2d 134 |
. . . . . . . . 9
⊢ ((Lim
𝐴 ∧ 𝑥 ∈ 𝐴) → (𝐴 ⊆ suc 𝐵 → ¬ 𝑥 = 𝐵)) |
| 20 | 19 | ex 412 |
. . . . . . . 8
⊢ (Lim
𝐴 → (𝑥 ∈ 𝐴 → (𝐴 ⊆ suc 𝐵 → ¬ 𝑥 = 𝐵))) |
| 21 | 20 | com23 86 |
. . . . . . 7
⊢ (Lim
𝐴 → (𝐴 ⊆ suc 𝐵 → (𝑥 ∈ 𝐴 → ¬ 𝑥 = 𝐵))) |
| 22 | 21 | imp31 417 |
. . . . . 6
⊢ (((Lim
𝐴 ∧ 𝐴 ⊆ suc 𝐵) ∧ 𝑥 ∈ 𝐴) → ¬ 𝑥 = 𝐵) |
| 23 | | ssel2 3978 |
. . . . . . . . . 10
⊢ ((𝐴 ⊆ suc 𝐵 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ suc 𝐵) |
| 24 | | vex 3484 |
. . . . . . . . . . 11
⊢ 𝑥 ∈ V |
| 25 | 24 | elsuc 6454 |
. . . . . . . . . 10
⊢ (𝑥 ∈ suc 𝐵 ↔ (𝑥 ∈ 𝐵 ∨ 𝑥 = 𝐵)) |
| 26 | 23, 25 | sylib 218 |
. . . . . . . . 9
⊢ ((𝐴 ⊆ suc 𝐵 ∧ 𝑥 ∈ 𝐴) → (𝑥 ∈ 𝐵 ∨ 𝑥 = 𝐵)) |
| 27 | 26 | ord 865 |
. . . . . . . 8
⊢ ((𝐴 ⊆ suc 𝐵 ∧ 𝑥 ∈ 𝐴) → (¬ 𝑥 ∈ 𝐵 → 𝑥 = 𝐵)) |
| 28 | 27 | con1d 145 |
. . . . . . 7
⊢ ((𝐴 ⊆ suc 𝐵 ∧ 𝑥 ∈ 𝐴) → (¬ 𝑥 = 𝐵 → 𝑥 ∈ 𝐵)) |
| 29 | 28 | adantll 714 |
. . . . . 6
⊢ (((Lim
𝐴 ∧ 𝐴 ⊆ suc 𝐵) ∧ 𝑥 ∈ 𝐴) → (¬ 𝑥 = 𝐵 → 𝑥 ∈ 𝐵)) |
| 30 | 22, 29 | mpd 15 |
. . . . 5
⊢ (((Lim
𝐴 ∧ 𝐴 ⊆ suc 𝐵) ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐵) |
| 31 | 30 | ex 412 |
. . . 4
⊢ ((Lim
𝐴 ∧ 𝐴 ⊆ suc 𝐵) → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)) |
| 32 | 31 | ssrdv 3989 |
. . 3
⊢ ((Lim
𝐴 ∧ 𝐴 ⊆ suc 𝐵) → 𝐴 ⊆ 𝐵) |
| 33 | 32 | ex 412 |
. 2
⊢ (Lim
𝐴 → (𝐴 ⊆ suc 𝐵 → 𝐴 ⊆ 𝐵)) |
| 34 | 3, 33 | impbid2 226 |
1
⊢ (Lim
𝐴 → (𝐴 ⊆ 𝐵 ↔ 𝐴 ⊆ suc 𝐵)) |