Step | Hyp | Ref
| Expression |
1 | | 0ss 4419 |
. . . . . 6
⊢ ∅
⊆ 𝐵 |
2 | | sspsstr 4125 |
. . . . . 6
⊢ ((∅
⊆ 𝐵 ∧ 𝐵 ⊊ 𝐴) → ∅ ⊊ 𝐴) |
3 | 1, 2 | mpan 689 |
. . . . 5
⊢ (𝐵 ⊊ 𝐴 → ∅ ⊊ 𝐴) |
4 | | 0pss 4466 |
. . . . . 6
⊢ (∅
⊊ 𝐴 ↔ 𝐴 ≠ ∅) |
5 | | df-ne 2943 |
. . . . . 6
⊢ (𝐴 ≠ ∅ ↔ ¬ 𝐴 = ∅) |
6 | 4, 5 | bitri 275 |
. . . . 5
⊢ (∅
⊊ 𝐴 ↔ ¬
𝐴 =
∅) |
7 | 3, 6 | sylib 218 |
. . . 4
⊢ (𝐵 ⊊ 𝐴 → ¬ 𝐴 = ∅) |
8 | | nn0suc 7930 |
. . . . 5
⊢ (𝐴 ∈ ω → (𝐴 = ∅ ∨ ∃𝑥 ∈ ω 𝐴 = suc 𝑥)) |
9 | 8 | orcanai 1003 |
. . . 4
⊢ ((𝐴 ∈ ω ∧ ¬
𝐴 = ∅) →
∃𝑥 ∈ ω
𝐴 = suc 𝑥) |
10 | 7, 9 | sylan2 592 |
. . 3
⊢ ((𝐴 ∈ ω ∧ 𝐵 ⊊ 𝐴) → ∃𝑥 ∈ ω 𝐴 = suc 𝑥) |
11 | | pssnel 4490 |
. . . . . . . 8
⊢ (𝐵 ⊊ suc 𝑥 → ∃𝑦(𝑦 ∈ suc 𝑥 ∧ ¬ 𝑦 ∈ 𝐵)) |
12 | | pssss 4115 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐵 ⊊ suc 𝑥 → 𝐵 ⊆ suc 𝑥) |
13 | | ssdif 4161 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐵 ⊆ suc 𝑥 → (𝐵 ∖ {𝑦}) ⊆ (suc 𝑥 ∖ {𝑦})) |
14 | | disjsn 4736 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐵 ∩ {𝑦}) = ∅ ↔ ¬ 𝑦 ∈ 𝐵) |
15 | | disj3 4473 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐵 ∩ {𝑦}) = ∅ ↔ 𝐵 = (𝐵 ∖ {𝑦})) |
16 | 14, 15 | bitr3i 277 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (¬
𝑦 ∈ 𝐵 ↔ 𝐵 = (𝐵 ∖ {𝑦})) |
17 | | sseq1 4028 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐵 = (𝐵 ∖ {𝑦}) → (𝐵 ⊆ (suc 𝑥 ∖ {𝑦}) ↔ (𝐵 ∖ {𝑦}) ⊆ (suc 𝑥 ∖ {𝑦}))) |
18 | 16, 17 | sylbi 217 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (¬
𝑦 ∈ 𝐵 → (𝐵 ⊆ (suc 𝑥 ∖ {𝑦}) ↔ (𝐵 ∖ {𝑦}) ⊆ (suc 𝑥 ∖ {𝑦}))) |
19 | 13, 18 | imbitrrid 246 |
. . . . . . . . . . . . . . . . . . 19
⊢ (¬
𝑦 ∈ 𝐵 → (𝐵 ⊆ suc 𝑥 → 𝐵 ⊆ (suc 𝑥 ∖ {𝑦}))) |
20 | 12, 19 | syl5 34 |
. . . . . . . . . . . . . . . . . 18
⊢ (¬
𝑦 ∈ 𝐵 → (𝐵 ⊊ suc 𝑥 → 𝐵 ⊆ (suc 𝑥 ∖ {𝑦}))) |
21 | | peano2 7925 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ ω → suc 𝑥 ∈
ω) |
22 | | nnfi 9229 |
. . . . . . . . . . . . . . . . . . 19
⊢ (suc
𝑥 ∈ ω → suc
𝑥 ∈
Fin) |
23 | | diffi 9238 |
. . . . . . . . . . . . . . . . . . 19
⊢ (suc
𝑥 ∈ Fin → (suc
𝑥 ∖ {𝑦}) ∈ Fin) |
24 | | ssdomfi 9258 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((suc
𝑥 ∖ {𝑦}) ∈ Fin → (𝐵 ⊆ (suc 𝑥 ∖ {𝑦}) → 𝐵 ≼ (suc 𝑥 ∖ {𝑦}))) |
25 | 21, 22, 23, 24 | 4syl 19 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ ω → (𝐵 ⊆ (suc 𝑥 ∖ {𝑦}) → 𝐵 ≼ (suc 𝑥 ∖ {𝑦}))) |
26 | 20, 25 | sylan9 507 |
. . . . . . . . . . . . . . . . 17
⊢ ((¬
𝑦 ∈ 𝐵 ∧ 𝑥 ∈ ω) → (𝐵 ⊊ suc 𝑥 → 𝐵 ≼ (suc 𝑥 ∖ {𝑦}))) |
27 | 26 | 3impia 1117 |
. . . . . . . . . . . . . . . 16
⊢ ((¬
𝑦 ∈ 𝐵 ∧ 𝑥 ∈ ω ∧ 𝐵 ⊊ suc 𝑥) → 𝐵 ≼ (suc 𝑥 ∖ {𝑦})) |
28 | 27 | 3com23 1126 |
. . . . . . . . . . . . . . 15
⊢ ((¬
𝑦 ∈ 𝐵 ∧ 𝐵 ⊊ suc 𝑥 ∧ 𝑥 ∈ ω) → 𝐵 ≼ (suc 𝑥 ∖ {𝑦})) |
29 | 28 | 3expa 1118 |
. . . . . . . . . . . . . 14
⊢ (((¬
𝑦 ∈ 𝐵 ∧ 𝐵 ⊊ suc 𝑥) ∧ 𝑥 ∈ ω) → 𝐵 ≼ (suc 𝑥 ∖ {𝑦})) |
30 | 29 | adantrr 716 |
. . . . . . . . . . . . 13
⊢ (((¬
𝑦 ∈ 𝐵 ∧ 𝐵 ⊊ suc 𝑥) ∧ (𝑥 ∈ ω ∧ 𝑦 ∈ suc 𝑥)) → 𝐵 ≼ (suc 𝑥 ∖ {𝑦})) |
31 | | nnfi 9229 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ω → 𝑥 ∈ Fin) |
32 | 31 | ad2antrl 727 |
. . . . . . . . . . . . . 14
⊢ ((𝐵 ≼ (suc 𝑥 ∖ {𝑦}) ∧ (𝑥 ∈ ω ∧ 𝑦 ∈ suc 𝑥)) → 𝑥 ∈ Fin) |
33 | | simpl 482 |
. . . . . . . . . . . . . 14
⊢ ((𝐵 ≼ (suc 𝑥 ∖ {𝑦}) ∧ (𝑥 ∈ ω ∧ 𝑦 ∈ suc 𝑥)) → 𝐵 ≼ (suc 𝑥 ∖ {𝑦})) |
34 | | simpr 484 |
. . . . . . . . . . . . . 14
⊢ ((𝐵 ≼ (suc 𝑥 ∖ {𝑦}) ∧ (𝑥 ∈ ω ∧ 𝑦 ∈ suc 𝑥)) → (𝑥 ∈ ω ∧ 𝑦 ∈ suc 𝑥)) |
35 | | phplem1 9266 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ suc 𝑥) → 𝑥 ≈ (suc 𝑥 ∖ {𝑦})) |
36 | | ensymfib 9246 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ Fin → (𝑥 ≈ (suc 𝑥 ∖ {𝑦}) ↔ (suc 𝑥 ∖ {𝑦}) ≈ 𝑥)) |
37 | 31, 36 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ ω → (𝑥 ≈ (suc 𝑥 ∖ {𝑦}) ↔ (suc 𝑥 ∖ {𝑦}) ≈ 𝑥)) |
38 | 37 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ suc 𝑥) → (𝑥 ≈ (suc 𝑥 ∖ {𝑦}) ↔ (suc 𝑥 ∖ {𝑦}) ≈ 𝑥)) |
39 | 35, 38 | mpbid 232 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ suc 𝑥) → (suc 𝑥 ∖ {𝑦}) ≈ 𝑥) |
40 | | endom 9035 |
. . . . . . . . . . . . . . . 16
⊢ ((suc
𝑥 ∖ {𝑦}) ≈ 𝑥 → (suc 𝑥 ∖ {𝑦}) ≼ 𝑥) |
41 | 39, 40 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ suc 𝑥) → (suc 𝑥 ∖ {𝑦}) ≼ 𝑥) |
42 | | domtrfir 9256 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ Fin ∧ 𝐵 ≼ (suc 𝑥 ∖ {𝑦}) ∧ (suc 𝑥 ∖ {𝑦}) ≼ 𝑥) → 𝐵 ≼ 𝑥) |
43 | 41, 42 | syl3an3 1165 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ Fin ∧ 𝐵 ≼ (suc 𝑥 ∖ {𝑦}) ∧ (𝑥 ∈ ω ∧ 𝑦 ∈ suc 𝑥)) → 𝐵 ≼ 𝑥) |
44 | 32, 33, 34, 43 | syl3anc 1371 |
. . . . . . . . . . . . 13
⊢ ((𝐵 ≼ (suc 𝑥 ∖ {𝑦}) ∧ (𝑥 ∈ ω ∧ 𝑦 ∈ suc 𝑥)) → 𝐵 ≼ 𝑥) |
45 | 30, 44 | sylancom 587 |
. . . . . . . . . . . 12
⊢ (((¬
𝑦 ∈ 𝐵 ∧ 𝐵 ⊊ suc 𝑥) ∧ (𝑥 ∈ ω ∧ 𝑦 ∈ suc 𝑥)) → 𝐵 ≼ 𝑥) |
46 | 45 | exp43 436 |
. . . . . . . . . . 11
⊢ (¬
𝑦 ∈ 𝐵 → (𝐵 ⊊ suc 𝑥 → (𝑥 ∈ ω → (𝑦 ∈ suc 𝑥 → 𝐵 ≼ 𝑥)))) |
47 | 46 | com4r 94 |
. . . . . . . . . 10
⊢ (𝑦 ∈ suc 𝑥 → (¬ 𝑦 ∈ 𝐵 → (𝐵 ⊊ suc 𝑥 → (𝑥 ∈ ω → 𝐵 ≼ 𝑥)))) |
48 | 47 | imp 406 |
. . . . . . . . 9
⊢ ((𝑦 ∈ suc 𝑥 ∧ ¬ 𝑦 ∈ 𝐵) → (𝐵 ⊊ suc 𝑥 → (𝑥 ∈ ω → 𝐵 ≼ 𝑥))) |
49 | 48 | exlimiv 1929 |
. . . . . . . 8
⊢
(∃𝑦(𝑦 ∈ suc 𝑥 ∧ ¬ 𝑦 ∈ 𝐵) → (𝐵 ⊊ suc 𝑥 → (𝑥 ∈ ω → 𝐵 ≼ 𝑥))) |
50 | 11, 49 | mpcom 38 |
. . . . . . 7
⊢ (𝐵 ⊊ suc 𝑥 → (𝑥 ∈ ω → 𝐵 ≼ 𝑥)) |
51 | | simp1 1136 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ω ∧ suc 𝑥 ≈ 𝐵 ∧ 𝐵 ≼ 𝑥) → 𝑥 ∈ ω) |
52 | | endom 9035 |
. . . . . . . . . . . . . . 15
⊢ (suc
𝑥 ≈ 𝐵 → suc 𝑥 ≼ 𝐵) |
53 | | domtrfir 9256 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ Fin ∧ suc 𝑥 ≼ 𝐵 ∧ 𝐵 ≼ 𝑥) → suc 𝑥 ≼ 𝑥) |
54 | 52, 53 | syl3an2 1164 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ Fin ∧ suc 𝑥 ≈ 𝐵 ∧ 𝐵 ≼ 𝑥) → suc 𝑥 ≼ 𝑥) |
55 | 31, 54 | syl3an1 1163 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ω ∧ suc 𝑥 ≈ 𝐵 ∧ 𝐵 ≼ 𝑥) → suc 𝑥 ≼ 𝑥) |
56 | | sssucid 6474 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑥 ⊆ suc 𝑥 |
57 | | ssdomfi 9258 |
. . . . . . . . . . . . . . . . 17
⊢ (suc
𝑥 ∈ Fin → (𝑥 ⊆ suc 𝑥 → 𝑥 ≼ suc 𝑥)) |
58 | 22, 56, 57 | mpisyl 21 |
. . . . . . . . . . . . . . . 16
⊢ (suc
𝑥 ∈ ω →
𝑥 ≼ suc 𝑥) |
59 | 21, 58 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ω → 𝑥 ≼ suc 𝑥) |
60 | 59 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ω ∧ suc 𝑥 ≼ 𝑥) → 𝑥 ≼ suc 𝑥) |
61 | | sbthfi 9261 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ Fin ∧ suc 𝑥 ≼ 𝑥 ∧ 𝑥 ≼ suc 𝑥) → suc 𝑥 ≈ 𝑥) |
62 | 31, 61 | syl3an1 1163 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ω ∧ suc 𝑥 ≼ 𝑥 ∧ 𝑥 ≼ suc 𝑥) → suc 𝑥 ≈ 𝑥) |
63 | 60, 62 | mpd3an3 1462 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ω ∧ suc 𝑥 ≼ 𝑥) → suc 𝑥 ≈ 𝑥) |
64 | 51, 55, 63 | syl2anc 583 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ω ∧ suc 𝑥 ≈ 𝐵 ∧ 𝐵 ≼ 𝑥) → suc 𝑥 ≈ 𝑥) |
65 | 64 | 3com23 1126 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ω ∧ 𝐵 ≼ 𝑥 ∧ suc 𝑥 ≈ 𝐵) → suc 𝑥 ≈ 𝑥) |
66 | 65 | 3expia 1121 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ω ∧ 𝐵 ≼ 𝑥) → (suc 𝑥 ≈ 𝐵 → suc 𝑥 ≈ 𝑥)) |
67 | | peano2b 7916 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ω ↔ suc 𝑥 ∈
ω) |
68 | | nnord 7907 |
. . . . . . . . . . . . 13
⊢ (suc
𝑥 ∈ ω → Ord
suc 𝑥) |
69 | 67, 68 | sylbi 217 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ω → Ord suc
𝑥) |
70 | | vex 3486 |
. . . . . . . . . . . . 13
⊢ 𝑥 ∈ V |
71 | 70 | sucid 6476 |
. . . . . . . . . . . 12
⊢ 𝑥 ∈ suc 𝑥 |
72 | | nordeq 6413 |
. . . . . . . . . . . 12
⊢ ((Ord suc
𝑥 ∧ 𝑥 ∈ suc 𝑥) → suc 𝑥 ≠ 𝑥) |
73 | 69, 71, 72 | sylancl 585 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ω → suc 𝑥 ≠ 𝑥) |
74 | | nneneq 9268 |
. . . . . . . . . . . . . 14
⊢ ((suc
𝑥 ∈ ω ∧
𝑥 ∈ ω) →
(suc 𝑥 ≈ 𝑥 ↔ suc 𝑥 = 𝑥)) |
75 | 67, 74 | sylanb 580 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ω ∧ 𝑥 ∈ ω) → (suc
𝑥 ≈ 𝑥 ↔ suc 𝑥 = 𝑥)) |
76 | 75 | anidms 566 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ω → (suc
𝑥 ≈ 𝑥 ↔ suc 𝑥 = 𝑥)) |
77 | 76 | necon3bbid 2980 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ω → (¬
suc 𝑥 ≈ 𝑥 ↔ suc 𝑥 ≠ 𝑥)) |
78 | 73, 77 | mpbird 257 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ω → ¬ suc
𝑥 ≈ 𝑥) |
79 | 66, 78 | nsyli 157 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ω ∧ 𝐵 ≼ 𝑥) → (𝑥 ∈ ω → ¬ suc 𝑥 ≈ 𝐵)) |
80 | 79 | expcom 413 |
. . . . . . . 8
⊢ (𝐵 ≼ 𝑥 → (𝑥 ∈ ω → (𝑥 ∈ ω → ¬ suc 𝑥 ≈ 𝐵))) |
81 | 80 | pm2.43d 53 |
. . . . . . 7
⊢ (𝐵 ≼ 𝑥 → (𝑥 ∈ ω → ¬ suc 𝑥 ≈ 𝐵)) |
82 | 50, 81 | syli 39 |
. . . . . 6
⊢ (𝐵 ⊊ suc 𝑥 → (𝑥 ∈ ω → ¬ suc 𝑥 ≈ 𝐵)) |
83 | 82 | com12 32 |
. . . . 5
⊢ (𝑥 ∈ ω → (𝐵 ⊊ suc 𝑥 → ¬ suc 𝑥 ≈ 𝐵)) |
84 | | psseq2 4108 |
. . . . . 6
⊢ (𝐴 = suc 𝑥 → (𝐵 ⊊ 𝐴 ↔ 𝐵 ⊊ suc 𝑥)) |
85 | | breq1 5172 |
. . . . . . 7
⊢ (𝐴 = suc 𝑥 → (𝐴 ≈ 𝐵 ↔ suc 𝑥 ≈ 𝐵)) |
86 | 85 | notbid 318 |
. . . . . 6
⊢ (𝐴 = suc 𝑥 → (¬ 𝐴 ≈ 𝐵 ↔ ¬ suc 𝑥 ≈ 𝐵)) |
87 | 84, 86 | imbi12d 344 |
. . . . 5
⊢ (𝐴 = suc 𝑥 → ((𝐵 ⊊ 𝐴 → ¬ 𝐴 ≈ 𝐵) ↔ (𝐵 ⊊ suc 𝑥 → ¬ suc 𝑥 ≈ 𝐵))) |
88 | 83, 87 | syl5ibrcom 247 |
. . . 4
⊢ (𝑥 ∈ ω → (𝐴 = suc 𝑥 → (𝐵 ⊊ 𝐴 → ¬ 𝐴 ≈ 𝐵))) |
89 | 88 | rexlimiv 3150 |
. . 3
⊢
(∃𝑥 ∈
ω 𝐴 = suc 𝑥 → (𝐵 ⊊ 𝐴 → ¬ 𝐴 ≈ 𝐵)) |
90 | 10, 89 | syl 17 |
. 2
⊢ ((𝐴 ∈ ω ∧ 𝐵 ⊊ 𝐴) → (𝐵 ⊊ 𝐴 → ¬ 𝐴 ≈ 𝐵)) |
91 | 90 | syldbl2 840 |
1
⊢ ((𝐴 ∈ ω ∧ 𝐵 ⊊ 𝐴) → ¬ 𝐴 ≈ 𝐵) |