Step | Hyp | Ref
| Expression |
1 | | sssucid 5802 |
. . 3
⊢ 𝐵 ⊆ suc 𝐵 |
2 | | sstr2 3610 |
. . 3
⊢ (𝐴 ⊆ 𝐵 → (𝐵 ⊆ suc 𝐵 → 𝐴 ⊆ suc 𝐵)) |
3 | 1, 2 | mpi 20 |
. 2
⊢ (𝐴 ⊆ 𝐵 → 𝐴 ⊆ suc 𝐵) |
4 | | eleq1 2689 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝐵 → (𝑥 ∈ 𝐴 ↔ 𝐵 ∈ 𝐴)) |
5 | 4 | biimpcd 239 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝐴 → (𝑥 = 𝐵 → 𝐵 ∈ 𝐴)) |
6 | | limsuc 7049 |
. . . . . . . . . . . . . 14
⊢ (Lim
𝐴 → (𝐵 ∈ 𝐴 ↔ suc 𝐵 ∈ 𝐴)) |
7 | 6 | biimpa 501 |
. . . . . . . . . . . . 13
⊢ ((Lim
𝐴 ∧ 𝐵 ∈ 𝐴) → suc 𝐵 ∈ 𝐴) |
8 | | limord 5784 |
. . . . . . . . . . . . . . . 16
⊢ (Lim
𝐴 → Ord 𝐴) |
9 | 8 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((Lim
𝐴 ∧ 𝐵 ∈ 𝐴) → Ord 𝐴) |
10 | | ordelord 5745 |
. . . . . . . . . . . . . . . . 17
⊢ ((Ord
𝐴 ∧ 𝐵 ∈ 𝐴) → Ord 𝐵) |
11 | 8, 10 | sylan 488 |
. . . . . . . . . . . . . . . 16
⊢ ((Lim
𝐴 ∧ 𝐵 ∈ 𝐴) → Ord 𝐵) |
12 | | ordsuc 7014 |
. . . . . . . . . . . . . . . 16
⊢ (Ord
𝐵 ↔ Ord suc 𝐵) |
13 | 11, 12 | sylib 208 |
. . . . . . . . . . . . . . 15
⊢ ((Lim
𝐴 ∧ 𝐵 ∈ 𝐴) → Ord suc 𝐵) |
14 | | ordtri1 5756 |
. . . . . . . . . . . . . . 15
⊢ ((Ord
𝐴 ∧ Ord suc 𝐵) → (𝐴 ⊆ suc 𝐵 ↔ ¬ suc 𝐵 ∈ 𝐴)) |
15 | 9, 13, 14 | syl2anc 693 |
. . . . . . . . . . . . . 14
⊢ ((Lim
𝐴 ∧ 𝐵 ∈ 𝐴) → (𝐴 ⊆ suc 𝐵 ↔ ¬ suc 𝐵 ∈ 𝐴)) |
16 | 15 | con2bid 344 |
. . . . . . . . . . . . 13
⊢ ((Lim
𝐴 ∧ 𝐵 ∈ 𝐴) → (suc 𝐵 ∈ 𝐴 ↔ ¬ 𝐴 ⊆ suc 𝐵)) |
17 | 7, 16 | mpbid 222 |
. . . . . . . . . . . 12
⊢ ((Lim
𝐴 ∧ 𝐵 ∈ 𝐴) → ¬ 𝐴 ⊆ suc 𝐵) |
18 | 17 | ex 450 |
. . . . . . . . . . 11
⊢ (Lim
𝐴 → (𝐵 ∈ 𝐴 → ¬ 𝐴 ⊆ suc 𝐵)) |
19 | 5, 18 | sylan9r 690 |
. . . . . . . . . 10
⊢ ((Lim
𝐴 ∧ 𝑥 ∈ 𝐴) → (𝑥 = 𝐵 → ¬ 𝐴 ⊆ suc 𝐵)) |
20 | 19 | con2d 129 |
. . . . . . . . 9
⊢ ((Lim
𝐴 ∧ 𝑥 ∈ 𝐴) → (𝐴 ⊆ suc 𝐵 → ¬ 𝑥 = 𝐵)) |
21 | 20 | ex 450 |
. . . . . . . 8
⊢ (Lim
𝐴 → (𝑥 ∈ 𝐴 → (𝐴 ⊆ suc 𝐵 → ¬ 𝑥 = 𝐵))) |
22 | 21 | com23 86 |
. . . . . . 7
⊢ (Lim
𝐴 → (𝐴 ⊆ suc 𝐵 → (𝑥 ∈ 𝐴 → ¬ 𝑥 = 𝐵))) |
23 | 22 | imp31 448 |
. . . . . 6
⊢ (((Lim
𝐴 ∧ 𝐴 ⊆ suc 𝐵) ∧ 𝑥 ∈ 𝐴) → ¬ 𝑥 = 𝐵) |
24 | | ssel2 3598 |
. . . . . . . . . 10
⊢ ((𝐴 ⊆ suc 𝐵 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ suc 𝐵) |
25 | | vex 3203 |
. . . . . . . . . . 11
⊢ 𝑥 ∈ V |
26 | 25 | elsuc 5794 |
. . . . . . . . . 10
⊢ (𝑥 ∈ suc 𝐵 ↔ (𝑥 ∈ 𝐵 ∨ 𝑥 = 𝐵)) |
27 | 24, 26 | sylib 208 |
. . . . . . . . 9
⊢ ((𝐴 ⊆ suc 𝐵 ∧ 𝑥 ∈ 𝐴) → (𝑥 ∈ 𝐵 ∨ 𝑥 = 𝐵)) |
28 | 27 | ord 392 |
. . . . . . . 8
⊢ ((𝐴 ⊆ suc 𝐵 ∧ 𝑥 ∈ 𝐴) → (¬ 𝑥 ∈ 𝐵 → 𝑥 = 𝐵)) |
29 | 28 | con1d 139 |
. . . . . . 7
⊢ ((𝐴 ⊆ suc 𝐵 ∧ 𝑥 ∈ 𝐴) → (¬ 𝑥 = 𝐵 → 𝑥 ∈ 𝐵)) |
30 | 29 | adantll 750 |
. . . . . 6
⊢ (((Lim
𝐴 ∧ 𝐴 ⊆ suc 𝐵) ∧ 𝑥 ∈ 𝐴) → (¬ 𝑥 = 𝐵 → 𝑥 ∈ 𝐵)) |
31 | 23, 30 | mpd 15 |
. . . . 5
⊢ (((Lim
𝐴 ∧ 𝐴 ⊆ suc 𝐵) ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐵) |
32 | 31 | ex 450 |
. . . 4
⊢ ((Lim
𝐴 ∧ 𝐴 ⊆ suc 𝐵) → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)) |
33 | 32 | ssrdv 3609 |
. . 3
⊢ ((Lim
𝐴 ∧ 𝐴 ⊆ suc 𝐵) → 𝐴 ⊆ 𝐵) |
34 | 33 | ex 450 |
. 2
⊢ (Lim
𝐴 → (𝐴 ⊆ suc 𝐵 → 𝐴 ⊆ 𝐵)) |
35 | 3, 34 | impbid2 216 |
1
⊢ (Lim
𝐴 → (𝐴 ⊆ 𝐵 ↔ 𝐴 ⊆ suc 𝐵)) |