Step |
Hyp |
Ref |
Expression |
1 |
|
sssucid |
⊢ 𝐵 ⊆ suc 𝐵 |
2 |
|
sstr2 |
⊢ ( 𝐴 ⊆ 𝐵 → ( 𝐵 ⊆ suc 𝐵 → 𝐴 ⊆ suc 𝐵 ) ) |
3 |
1 2
|
mpi |
⊢ ( 𝐴 ⊆ 𝐵 → 𝐴 ⊆ suc 𝐵 ) |
4 |
|
eleq1 |
⊢ ( 𝑥 = 𝐵 → ( 𝑥 ∈ 𝐴 ↔ 𝐵 ∈ 𝐴 ) ) |
5 |
4
|
biimpcd |
⊢ ( 𝑥 ∈ 𝐴 → ( 𝑥 = 𝐵 → 𝐵 ∈ 𝐴 ) ) |
6 |
|
limsuc |
⊢ ( Lim 𝐴 → ( 𝐵 ∈ 𝐴 ↔ suc 𝐵 ∈ 𝐴 ) ) |
7 |
6
|
biimpa |
⊢ ( ( Lim 𝐴 ∧ 𝐵 ∈ 𝐴 ) → suc 𝐵 ∈ 𝐴 ) |
8 |
|
limord |
⊢ ( Lim 𝐴 → Ord 𝐴 ) |
9 |
|
ordelord |
⊢ ( ( Ord 𝐴 ∧ 𝐵 ∈ 𝐴 ) → Ord 𝐵 ) |
10 |
8 9
|
sylan |
⊢ ( ( Lim 𝐴 ∧ 𝐵 ∈ 𝐴 ) → Ord 𝐵 ) |
11 |
|
ordsuc |
⊢ ( Ord 𝐵 ↔ Ord suc 𝐵 ) |
12 |
10 11
|
sylib |
⊢ ( ( Lim 𝐴 ∧ 𝐵 ∈ 𝐴 ) → Ord suc 𝐵 ) |
13 |
|
ordtri1 |
⊢ ( ( Ord 𝐴 ∧ Ord suc 𝐵 ) → ( 𝐴 ⊆ suc 𝐵 ↔ ¬ suc 𝐵 ∈ 𝐴 ) ) |
14 |
8 12 13
|
syl2an2r |
⊢ ( ( Lim 𝐴 ∧ 𝐵 ∈ 𝐴 ) → ( 𝐴 ⊆ suc 𝐵 ↔ ¬ suc 𝐵 ∈ 𝐴 ) ) |
15 |
14
|
con2bid |
⊢ ( ( Lim 𝐴 ∧ 𝐵 ∈ 𝐴 ) → ( suc 𝐵 ∈ 𝐴 ↔ ¬ 𝐴 ⊆ suc 𝐵 ) ) |
16 |
7 15
|
mpbid |
⊢ ( ( Lim 𝐴 ∧ 𝐵 ∈ 𝐴 ) → ¬ 𝐴 ⊆ suc 𝐵 ) |
17 |
16
|
ex |
⊢ ( Lim 𝐴 → ( 𝐵 ∈ 𝐴 → ¬ 𝐴 ⊆ suc 𝐵 ) ) |
18 |
5 17
|
sylan9r |
⊢ ( ( Lim 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑥 = 𝐵 → ¬ 𝐴 ⊆ suc 𝐵 ) ) |
19 |
18
|
con2d |
⊢ ( ( Lim 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐴 ⊆ suc 𝐵 → ¬ 𝑥 = 𝐵 ) ) |
20 |
19
|
ex |
⊢ ( Lim 𝐴 → ( 𝑥 ∈ 𝐴 → ( 𝐴 ⊆ suc 𝐵 → ¬ 𝑥 = 𝐵 ) ) ) |
21 |
20
|
com23 |
⊢ ( Lim 𝐴 → ( 𝐴 ⊆ suc 𝐵 → ( 𝑥 ∈ 𝐴 → ¬ 𝑥 = 𝐵 ) ) ) |
22 |
21
|
imp31 |
⊢ ( ( ( Lim 𝐴 ∧ 𝐴 ⊆ suc 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → ¬ 𝑥 = 𝐵 ) |
23 |
|
ssel2 |
⊢ ( ( 𝐴 ⊆ suc 𝐵 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ suc 𝐵 ) |
24 |
|
vex |
⊢ 𝑥 ∈ V |
25 |
24
|
elsuc |
⊢ ( 𝑥 ∈ suc 𝐵 ↔ ( 𝑥 ∈ 𝐵 ∨ 𝑥 = 𝐵 ) ) |
26 |
23 25
|
sylib |
⊢ ( ( 𝐴 ⊆ suc 𝐵 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑥 ∈ 𝐵 ∨ 𝑥 = 𝐵 ) ) |
27 |
26
|
ord |
⊢ ( ( 𝐴 ⊆ suc 𝐵 ∧ 𝑥 ∈ 𝐴 ) → ( ¬ 𝑥 ∈ 𝐵 → 𝑥 = 𝐵 ) ) |
28 |
27
|
con1d |
⊢ ( ( 𝐴 ⊆ suc 𝐵 ∧ 𝑥 ∈ 𝐴 ) → ( ¬ 𝑥 = 𝐵 → 𝑥 ∈ 𝐵 ) ) |
29 |
28
|
adantll |
⊢ ( ( ( Lim 𝐴 ∧ 𝐴 ⊆ suc 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → ( ¬ 𝑥 = 𝐵 → 𝑥 ∈ 𝐵 ) ) |
30 |
22 29
|
mpd |
⊢ ( ( ( Lim 𝐴 ∧ 𝐴 ⊆ suc 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐵 ) |
31 |
30
|
ex |
⊢ ( ( Lim 𝐴 ∧ 𝐴 ⊆ suc 𝐵 ) → ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵 ) ) |
32 |
31
|
ssrdv |
⊢ ( ( Lim 𝐴 ∧ 𝐴 ⊆ suc 𝐵 ) → 𝐴 ⊆ 𝐵 ) |
33 |
32
|
ex |
⊢ ( Lim 𝐴 → ( 𝐴 ⊆ suc 𝐵 → 𝐴 ⊆ 𝐵 ) ) |
34 |
3 33
|
impbid2 |
⊢ ( Lim 𝐴 → ( 𝐴 ⊆ 𝐵 ↔ 𝐴 ⊆ suc 𝐵 ) ) |