Step | Hyp | Ref
| Expression |
1 | | 0ss 4295 |
. . . . . . . 8
⊢ ∅
⊆ 𝐵 |
2 | | sspsstr 4006 |
. . . . . . . 8
⊢ ((∅
⊆ 𝐵 ∧ 𝐵 ⊊ 𝐴) → ∅ ⊊ 𝐴) |
3 | 1, 2 | mpan 690 |
. . . . . . 7
⊢ (𝐵 ⊊ 𝐴 → ∅ ⊊ 𝐴) |
4 | | 0pss 4344 |
. . . . . . . 8
⊢ (∅
⊊ 𝐴 ↔ 𝐴 ≠ ∅) |
5 | | df-ne 2936 |
. . . . . . . 8
⊢ (𝐴 ≠ ∅ ↔ ¬ 𝐴 = ∅) |
6 | 4, 5 | bitri 278 |
. . . . . . 7
⊢ (∅
⊊ 𝐴 ↔ ¬
𝐴 =
∅) |
7 | 3, 6 | sylib 221 |
. . . . . 6
⊢ (𝐵 ⊊ 𝐴 → ¬ 𝐴 = ∅) |
8 | | nn0suc 7638 |
. . . . . . 7
⊢ (𝐴 ∈ ω → (𝐴 = ∅ ∨ ∃𝑥 ∈ ω 𝐴 = suc 𝑥)) |
9 | 8 | orcanai 1002 |
. . . . . 6
⊢ ((𝐴 ∈ ω ∧ ¬
𝐴 = ∅) →
∃𝑥 ∈ ω
𝐴 = suc 𝑥) |
10 | 7, 9 | sylan2 596 |
. . . . 5
⊢ ((𝐴 ∈ ω ∧ 𝐵 ⊊ 𝐴) → ∃𝑥 ∈ ω 𝐴 = suc 𝑥) |
11 | | pssnel 4370 |
. . . . . . . . . 10
⊢ (𝐵 ⊊ suc 𝑥 → ∃𝑦(𝑦 ∈ suc 𝑥 ∧ ¬ 𝑦 ∈ 𝐵)) |
12 | | pssss 3996 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐵 ⊊ suc 𝑥 → 𝐵 ⊆ suc 𝑥) |
13 | | ssdif 4040 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐵 ⊆ suc 𝑥 → (𝐵 ∖ {𝑦}) ⊆ (suc 𝑥 ∖ {𝑦})) |
14 | | disjsn 4612 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐵 ∩ {𝑦}) = ∅ ↔ ¬ 𝑦 ∈ 𝐵) |
15 | | disj3 4353 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐵 ∩ {𝑦}) = ∅ ↔ 𝐵 = (𝐵 ∖ {𝑦})) |
16 | 14, 15 | bitr3i 280 |
. . . . . . . . . . . . . . . . . . 19
⊢ (¬
𝑦 ∈ 𝐵 ↔ 𝐵 = (𝐵 ∖ {𝑦})) |
17 | | sseq1 3912 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐵 = (𝐵 ∖ {𝑦}) → (𝐵 ⊆ (suc 𝑥 ∖ {𝑦}) ↔ (𝐵 ∖ {𝑦}) ⊆ (suc 𝑥 ∖ {𝑦}))) |
18 | 16, 17 | sylbi 220 |
. . . . . . . . . . . . . . . . . 18
⊢ (¬
𝑦 ∈ 𝐵 → (𝐵 ⊆ (suc 𝑥 ∖ {𝑦}) ↔ (𝐵 ∖ {𝑦}) ⊆ (suc 𝑥 ∖ {𝑦}))) |
19 | 13, 18 | syl5ibr 249 |
. . . . . . . . . . . . . . . . 17
⊢ (¬
𝑦 ∈ 𝐵 → (𝐵 ⊆ suc 𝑥 → 𝐵 ⊆ (suc 𝑥 ∖ {𝑦}))) |
20 | | vex 3404 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝑥 ∈ V |
21 | 20 | sucex 7557 |
. . . . . . . . . . . . . . . . . . 19
⊢ suc 𝑥 ∈ V |
22 | 21 | difexi 5206 |
. . . . . . . . . . . . . . . . . 18
⊢ (suc
𝑥 ∖ {𝑦}) ∈ V |
23 | | ssdomg 8613 |
. . . . . . . . . . . . . . . . . 18
⊢ ((suc
𝑥 ∖ {𝑦}) ∈ V → (𝐵 ⊆ (suc 𝑥 ∖ {𝑦}) → 𝐵 ≼ (suc 𝑥 ∖ {𝑦}))) |
24 | 22, 23 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐵 ⊆ (suc 𝑥 ∖ {𝑦}) → 𝐵 ≼ (suc 𝑥 ∖ {𝑦})) |
25 | 12, 19, 24 | syl56 36 |
. . . . . . . . . . . . . . . 16
⊢ (¬
𝑦 ∈ 𝐵 → (𝐵 ⊊ suc 𝑥 → 𝐵 ≼ (suc 𝑥 ∖ {𝑦}))) |
26 | 25 | imp 410 |
. . . . . . . . . . . . . . 15
⊢ ((¬
𝑦 ∈ 𝐵 ∧ 𝐵 ⊊ suc 𝑥) → 𝐵 ≼ (suc 𝑥 ∖ {𝑦})) |
27 | | vex 3404 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑦 ∈ V |
28 | 20, 27 | phplem3 8760 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ suc 𝑥) → 𝑥 ≈ (suc 𝑥 ∖ {𝑦})) |
29 | 28 | ensymd 8618 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ suc 𝑥) → (suc 𝑥 ∖ {𝑦}) ≈ 𝑥) |
30 | | domentr 8626 |
. . . . . . . . . . . . . . 15
⊢ ((𝐵 ≼ (suc 𝑥 ∖ {𝑦}) ∧ (suc 𝑥 ∖ {𝑦}) ≈ 𝑥) → 𝐵 ≼ 𝑥) |
31 | 26, 29, 30 | syl2an 599 |
. . . . . . . . . . . . . 14
⊢ (((¬
𝑦 ∈ 𝐵 ∧ 𝐵 ⊊ suc 𝑥) ∧ (𝑥 ∈ ω ∧ 𝑦 ∈ suc 𝑥)) → 𝐵 ≼ 𝑥) |
32 | 31 | exp43 440 |
. . . . . . . . . . . . 13
⊢ (¬
𝑦 ∈ 𝐵 → (𝐵 ⊊ suc 𝑥 → (𝑥 ∈ ω → (𝑦 ∈ suc 𝑥 → 𝐵 ≼ 𝑥)))) |
33 | 32 | com4r 94 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ suc 𝑥 → (¬ 𝑦 ∈ 𝐵 → (𝐵 ⊊ suc 𝑥 → (𝑥 ∈ ω → 𝐵 ≼ 𝑥)))) |
34 | 33 | imp 410 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ suc 𝑥 ∧ ¬ 𝑦 ∈ 𝐵) → (𝐵 ⊊ suc 𝑥 → (𝑥 ∈ ω → 𝐵 ≼ 𝑥))) |
35 | 34 | exlimiv 1937 |
. . . . . . . . . 10
⊢
(∃𝑦(𝑦 ∈ suc 𝑥 ∧ ¬ 𝑦 ∈ 𝐵) → (𝐵 ⊊ suc 𝑥 → (𝑥 ∈ ω → 𝐵 ≼ 𝑥))) |
36 | 11, 35 | mpcom 38 |
. . . . . . . . 9
⊢ (𝐵 ⊊ suc 𝑥 → (𝑥 ∈ ω → 𝐵 ≼ 𝑥)) |
37 | | endomtr 8625 |
. . . . . . . . . . . 12
⊢ ((suc
𝑥 ≈ 𝐵 ∧ 𝐵 ≼ 𝑥) → suc 𝑥 ≼ 𝑥) |
38 | | sssucid 6259 |
. . . . . . . . . . . . 13
⊢ 𝑥 ⊆ suc 𝑥 |
39 | | ssdomg 8613 |
. . . . . . . . . . . . 13
⊢ (suc
𝑥 ∈ V → (𝑥 ⊆ suc 𝑥 → 𝑥 ≼ suc 𝑥)) |
40 | 21, 38, 39 | mp2 9 |
. . . . . . . . . . . 12
⊢ 𝑥 ≼ suc 𝑥 |
41 | | sbth 8699 |
. . . . . . . . . . . 12
⊢ ((suc
𝑥 ≼ 𝑥 ∧ 𝑥 ≼ suc 𝑥) → suc 𝑥 ≈ 𝑥) |
42 | 37, 40, 41 | sylancl 589 |
. . . . . . . . . . 11
⊢ ((suc
𝑥 ≈ 𝐵 ∧ 𝐵 ≼ 𝑥) → suc 𝑥 ≈ 𝑥) |
43 | 42 | expcom 417 |
. . . . . . . . . 10
⊢ (𝐵 ≼ 𝑥 → (suc 𝑥 ≈ 𝐵 → suc 𝑥 ≈ 𝑥)) |
44 | | peano2b 7627 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ω ↔ suc 𝑥 ∈
ω) |
45 | | nnord 7619 |
. . . . . . . . . . . . 13
⊢ (suc
𝑥 ∈ ω → Ord
suc 𝑥) |
46 | 44, 45 | sylbi 220 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ω → Ord suc
𝑥) |
47 | 20 | sucid 6261 |
. . . . . . . . . . . 12
⊢ 𝑥 ∈ suc 𝑥 |
48 | | nordeq 6201 |
. . . . . . . . . . . 12
⊢ ((Ord suc
𝑥 ∧ 𝑥 ∈ suc 𝑥) → suc 𝑥 ≠ 𝑥) |
49 | 46, 47, 48 | sylancl 589 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ω → suc 𝑥 ≠ 𝑥) |
50 | | nneneq 8762 |
. . . . . . . . . . . . . 14
⊢ ((suc
𝑥 ∈ ω ∧
𝑥 ∈ ω) →
(suc 𝑥 ≈ 𝑥 ↔ suc 𝑥 = 𝑥)) |
51 | 44, 50 | sylanb 584 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ω ∧ 𝑥 ∈ ω) → (suc
𝑥 ≈ 𝑥 ↔ suc 𝑥 = 𝑥)) |
52 | 51 | anidms 570 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ω → (suc
𝑥 ≈ 𝑥 ↔ suc 𝑥 = 𝑥)) |
53 | 52 | necon3bbid 2972 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ω → (¬
suc 𝑥 ≈ 𝑥 ↔ suc 𝑥 ≠ 𝑥)) |
54 | 49, 53 | mpbird 260 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ω → ¬ suc
𝑥 ≈ 𝑥) |
55 | 43, 54 | nsyli 160 |
. . . . . . . . 9
⊢ (𝐵 ≼ 𝑥 → (𝑥 ∈ ω → ¬ suc 𝑥 ≈ 𝐵)) |
56 | 36, 55 | syli 39 |
. . . . . . . 8
⊢ (𝐵 ⊊ suc 𝑥 → (𝑥 ∈ ω → ¬ suc 𝑥 ≈ 𝐵)) |
57 | 56 | com12 32 |
. . . . . . 7
⊢ (𝑥 ∈ ω → (𝐵 ⊊ suc 𝑥 → ¬ suc 𝑥 ≈ 𝐵)) |
58 | | psseq2 3989 |
. . . . . . . 8
⊢ (𝐴 = suc 𝑥 → (𝐵 ⊊ 𝐴 ↔ 𝐵 ⊊ suc 𝑥)) |
59 | | breq1 5043 |
. . . . . . . . 9
⊢ (𝐴 = suc 𝑥 → (𝐴 ≈ 𝐵 ↔ suc 𝑥 ≈ 𝐵)) |
60 | 59 | notbid 321 |
. . . . . . . 8
⊢ (𝐴 = suc 𝑥 → (¬ 𝐴 ≈ 𝐵 ↔ ¬ suc 𝑥 ≈ 𝐵)) |
61 | 58, 60 | imbi12d 348 |
. . . . . . 7
⊢ (𝐴 = suc 𝑥 → ((𝐵 ⊊ 𝐴 → ¬ 𝐴 ≈ 𝐵) ↔ (𝐵 ⊊ suc 𝑥 → ¬ suc 𝑥 ≈ 𝐵))) |
62 | 57, 61 | syl5ibrcom 250 |
. . . . . 6
⊢ (𝑥 ∈ ω → (𝐴 = suc 𝑥 → (𝐵 ⊊ 𝐴 → ¬ 𝐴 ≈ 𝐵))) |
63 | 62 | rexlimiv 3191 |
. . . . 5
⊢
(∃𝑥 ∈
ω 𝐴 = suc 𝑥 → (𝐵 ⊊ 𝐴 → ¬ 𝐴 ≈ 𝐵)) |
64 | 10, 63 | syl 17 |
. . . 4
⊢ ((𝐴 ∈ ω ∧ 𝐵 ⊊ 𝐴) → (𝐵 ⊊ 𝐴 → ¬ 𝐴 ≈ 𝐵)) |
65 | 64 | ex 416 |
. . 3
⊢ (𝐴 ∈ ω → (𝐵 ⊊ 𝐴 → (𝐵 ⊊ 𝐴 → ¬ 𝐴 ≈ 𝐵))) |
66 | 65 | pm2.43d 53 |
. 2
⊢ (𝐴 ∈ ω → (𝐵 ⊊ 𝐴 → ¬ 𝐴 ≈ 𝐵)) |
67 | 66 | imp 410 |
1
⊢ ((𝐴 ∈ ω ∧ 𝐵 ⊊ 𝐴) → ¬ 𝐴 ≈ 𝐵) |