Step | Hyp | Ref
| Expression |
1 | | 0ss 4330 |
. . . . . 6
⊢ ∅
⊆ 𝐵 |
2 | | sspsstr 4040 |
. . . . . 6
⊢ ((∅
⊆ 𝐵 ∧ 𝐵 ⊊ 𝐴) → ∅ ⊊ 𝐴) |
3 | 1, 2 | mpan 687 |
. . . . 5
⊢ (𝐵 ⊊ 𝐴 → ∅ ⊊ 𝐴) |
4 | | 0pss 4378 |
. . . . . 6
⊢ (∅
⊊ 𝐴 ↔ 𝐴 ≠ ∅) |
5 | | df-ne 2944 |
. . . . . 6
⊢ (𝐴 ≠ ∅ ↔ ¬ 𝐴 = ∅) |
6 | 4, 5 | bitri 274 |
. . . . 5
⊢ (∅
⊊ 𝐴 ↔ ¬
𝐴 =
∅) |
7 | 3, 6 | sylib 217 |
. . . 4
⊢ (𝐵 ⊊ 𝐴 → ¬ 𝐴 = ∅) |
8 | | nn0suc 7742 |
. . . . 5
⊢ (𝐴 ∈ ω → (𝐴 = ∅ ∨ ∃𝑥 ∈ ω 𝐴 = suc 𝑥)) |
9 | 8 | orcanai 1000 |
. . . 4
⊢ ((𝐴 ∈ ω ∧ ¬
𝐴 = ∅) →
∃𝑥 ∈ ω
𝐴 = suc 𝑥) |
10 | 7, 9 | sylan2 593 |
. . 3
⊢ ((𝐴 ∈ ω ∧ 𝐵 ⊊ 𝐴) → ∃𝑥 ∈ ω 𝐴 = suc 𝑥) |
11 | | pssnel 4404 |
. . . . . . . 8
⊢ (𝐵 ⊊ suc 𝑥 → ∃𝑦(𝑦 ∈ suc 𝑥 ∧ ¬ 𝑦 ∈ 𝐵)) |
12 | | pssss 4030 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐵 ⊊ suc 𝑥 → 𝐵 ⊆ suc 𝑥) |
13 | | ssdif 4074 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐵 ⊆ suc 𝑥 → (𝐵 ∖ {𝑦}) ⊆ (suc 𝑥 ∖ {𝑦})) |
14 | | disjsn 4647 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐵 ∩ {𝑦}) = ∅ ↔ ¬ 𝑦 ∈ 𝐵) |
15 | | disj3 4387 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐵 ∩ {𝑦}) = ∅ ↔ 𝐵 = (𝐵 ∖ {𝑦})) |
16 | 14, 15 | bitr3i 276 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (¬
𝑦 ∈ 𝐵 ↔ 𝐵 = (𝐵 ∖ {𝑦})) |
17 | | sseq1 3946 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐵 = (𝐵 ∖ {𝑦}) → (𝐵 ⊆ (suc 𝑥 ∖ {𝑦}) ↔ (𝐵 ∖ {𝑦}) ⊆ (suc 𝑥 ∖ {𝑦}))) |
18 | 16, 17 | sylbi 216 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (¬
𝑦 ∈ 𝐵 → (𝐵 ⊆ (suc 𝑥 ∖ {𝑦}) ↔ (𝐵 ∖ {𝑦}) ⊆ (suc 𝑥 ∖ {𝑦}))) |
19 | 13, 18 | syl5ibr 245 |
. . . . . . . . . . . . . . . . . . 19
⊢ (¬
𝑦 ∈ 𝐵 → (𝐵 ⊆ suc 𝑥 → 𝐵 ⊆ (suc 𝑥 ∖ {𝑦}))) |
20 | 12, 19 | syl5 34 |
. . . . . . . . . . . . . . . . . 18
⊢ (¬
𝑦 ∈ 𝐵 → (𝐵 ⊊ suc 𝑥 → 𝐵 ⊆ (suc 𝑥 ∖ {𝑦}))) |
21 | | peano2 7737 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ ω → suc 𝑥 ∈
ω) |
22 | | nnfi 8950 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (suc
𝑥 ∈ ω → suc
𝑥 ∈
Fin) |
23 | | diffi 8962 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (suc
𝑥 ∈ Fin → (suc
𝑥 ∖ {𝑦}) ∈ Fin) |
24 | 21, 22, 23 | 3syl 18 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ ω → (suc
𝑥 ∖ {𝑦}) ∈ Fin) |
25 | | ssdomfi 8982 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((suc
𝑥 ∖ {𝑦}) ∈ Fin → (𝐵 ⊆ (suc 𝑥 ∖ {𝑦}) → 𝐵 ≼ (suc 𝑥 ∖ {𝑦}))) |
26 | 24, 25 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ ω → (𝐵 ⊆ (suc 𝑥 ∖ {𝑦}) → 𝐵 ≼ (suc 𝑥 ∖ {𝑦}))) |
27 | 20, 26 | sylan9 508 |
. . . . . . . . . . . . . . . . 17
⊢ ((¬
𝑦 ∈ 𝐵 ∧ 𝑥 ∈ ω) → (𝐵 ⊊ suc 𝑥 → 𝐵 ≼ (suc 𝑥 ∖ {𝑦}))) |
28 | 27 | 3impia 1116 |
. . . . . . . . . . . . . . . 16
⊢ ((¬
𝑦 ∈ 𝐵 ∧ 𝑥 ∈ ω ∧ 𝐵 ⊊ suc 𝑥) → 𝐵 ≼ (suc 𝑥 ∖ {𝑦})) |
29 | 28 | 3com23 1125 |
. . . . . . . . . . . . . . 15
⊢ ((¬
𝑦 ∈ 𝐵 ∧ 𝐵 ⊊ suc 𝑥 ∧ 𝑥 ∈ ω) → 𝐵 ≼ (suc 𝑥 ∖ {𝑦})) |
30 | 29 | 3expa 1117 |
. . . . . . . . . . . . . 14
⊢ (((¬
𝑦 ∈ 𝐵 ∧ 𝐵 ⊊ suc 𝑥) ∧ 𝑥 ∈ ω) → 𝐵 ≼ (suc 𝑥 ∖ {𝑦})) |
31 | 30 | adantrr 714 |
. . . . . . . . . . . . 13
⊢ (((¬
𝑦 ∈ 𝐵 ∧ 𝐵 ⊊ suc 𝑥) ∧ (𝑥 ∈ ω ∧ 𝑦 ∈ suc 𝑥)) → 𝐵 ≼ (suc 𝑥 ∖ {𝑦})) |
32 | | nnfi 8950 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ω → 𝑥 ∈ Fin) |
33 | 32 | ad2antrl 725 |
. . . . . . . . . . . . . 14
⊢ ((𝐵 ≼ (suc 𝑥 ∖ {𝑦}) ∧ (𝑥 ∈ ω ∧ 𝑦 ∈ suc 𝑥)) → 𝑥 ∈ Fin) |
34 | | simpl 483 |
. . . . . . . . . . . . . 14
⊢ ((𝐵 ≼ (suc 𝑥 ∖ {𝑦}) ∧ (𝑥 ∈ ω ∧ 𝑦 ∈ suc 𝑥)) → 𝐵 ≼ (suc 𝑥 ∖ {𝑦})) |
35 | | simpr 485 |
. . . . . . . . . . . . . 14
⊢ ((𝐵 ≼ (suc 𝑥 ∖ {𝑦}) ∧ (𝑥 ∈ ω ∧ 𝑦 ∈ suc 𝑥)) → (𝑥 ∈ ω ∧ 𝑦 ∈ suc 𝑥)) |
36 | | phplem1 8990 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ suc 𝑥) → 𝑥 ≈ (suc 𝑥 ∖ {𝑦})) |
37 | | ensymfib 8970 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ Fin → (𝑥 ≈ (suc 𝑥 ∖ {𝑦}) ↔ (suc 𝑥 ∖ {𝑦}) ≈ 𝑥)) |
38 | 32, 37 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ ω → (𝑥 ≈ (suc 𝑥 ∖ {𝑦}) ↔ (suc 𝑥 ∖ {𝑦}) ≈ 𝑥)) |
39 | 38 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ suc 𝑥) → (𝑥 ≈ (suc 𝑥 ∖ {𝑦}) ↔ (suc 𝑥 ∖ {𝑦}) ≈ 𝑥)) |
40 | 36, 39 | mpbid 231 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ suc 𝑥) → (suc 𝑥 ∖ {𝑦}) ≈ 𝑥) |
41 | | endom 8767 |
. . . . . . . . . . . . . . . 16
⊢ ((suc
𝑥 ∖ {𝑦}) ≈ 𝑥 → (suc 𝑥 ∖ {𝑦}) ≼ 𝑥) |
42 | 40, 41 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ suc 𝑥) → (suc 𝑥 ∖ {𝑦}) ≼ 𝑥) |
43 | | domtrfir 8980 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ Fin ∧ 𝐵 ≼ (suc 𝑥 ∖ {𝑦}) ∧ (suc 𝑥 ∖ {𝑦}) ≼ 𝑥) → 𝐵 ≼ 𝑥) |
44 | 42, 43 | syl3an3 1164 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ Fin ∧ 𝐵 ≼ (suc 𝑥 ∖ {𝑦}) ∧ (𝑥 ∈ ω ∧ 𝑦 ∈ suc 𝑥)) → 𝐵 ≼ 𝑥) |
45 | 33, 34, 35, 44 | syl3anc 1370 |
. . . . . . . . . . . . 13
⊢ ((𝐵 ≼ (suc 𝑥 ∖ {𝑦}) ∧ (𝑥 ∈ ω ∧ 𝑦 ∈ suc 𝑥)) → 𝐵 ≼ 𝑥) |
46 | 31, 45 | sylancom 588 |
. . . . . . . . . . . 12
⊢ (((¬
𝑦 ∈ 𝐵 ∧ 𝐵 ⊊ suc 𝑥) ∧ (𝑥 ∈ ω ∧ 𝑦 ∈ suc 𝑥)) → 𝐵 ≼ 𝑥) |
47 | 46 | exp43 437 |
. . . . . . . . . . 11
⊢ (¬
𝑦 ∈ 𝐵 → (𝐵 ⊊ suc 𝑥 → (𝑥 ∈ ω → (𝑦 ∈ suc 𝑥 → 𝐵 ≼ 𝑥)))) |
48 | 47 | com4r 94 |
. . . . . . . . . 10
⊢ (𝑦 ∈ suc 𝑥 → (¬ 𝑦 ∈ 𝐵 → (𝐵 ⊊ suc 𝑥 → (𝑥 ∈ ω → 𝐵 ≼ 𝑥)))) |
49 | 48 | imp 407 |
. . . . . . . . 9
⊢ ((𝑦 ∈ suc 𝑥 ∧ ¬ 𝑦 ∈ 𝐵) → (𝐵 ⊊ suc 𝑥 → (𝑥 ∈ ω → 𝐵 ≼ 𝑥))) |
50 | 49 | exlimiv 1933 |
. . . . . . . 8
⊢
(∃𝑦(𝑦 ∈ suc 𝑥 ∧ ¬ 𝑦 ∈ 𝐵) → (𝐵 ⊊ suc 𝑥 → (𝑥 ∈ ω → 𝐵 ≼ 𝑥))) |
51 | 11, 50 | mpcom 38 |
. . . . . . 7
⊢ (𝐵 ⊊ suc 𝑥 → (𝑥 ∈ ω → 𝐵 ≼ 𝑥)) |
52 | | simp1 1135 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ω ∧ suc 𝑥 ≈ 𝐵 ∧ 𝐵 ≼ 𝑥) → 𝑥 ∈ ω) |
53 | | endom 8767 |
. . . . . . . . . . . . . . 15
⊢ (suc
𝑥 ≈ 𝐵 → suc 𝑥 ≼ 𝐵) |
54 | | domtrfir 8980 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ Fin ∧ suc 𝑥 ≼ 𝐵 ∧ 𝐵 ≼ 𝑥) → suc 𝑥 ≼ 𝑥) |
55 | 53, 54 | syl3an2 1163 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ Fin ∧ suc 𝑥 ≈ 𝐵 ∧ 𝐵 ≼ 𝑥) → suc 𝑥 ≼ 𝑥) |
56 | 32, 55 | syl3an1 1162 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ω ∧ suc 𝑥 ≈ 𝐵 ∧ 𝐵 ≼ 𝑥) → suc 𝑥 ≼ 𝑥) |
57 | | sssucid 6343 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑥 ⊆ suc 𝑥 |
58 | | ssdomfi 8982 |
. . . . . . . . . . . . . . . . 17
⊢ (suc
𝑥 ∈ Fin → (𝑥 ⊆ suc 𝑥 → 𝑥 ≼ suc 𝑥)) |
59 | 22, 57, 58 | mpisyl 21 |
. . . . . . . . . . . . . . . 16
⊢ (suc
𝑥 ∈ ω →
𝑥 ≼ suc 𝑥) |
60 | 21, 59 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ω → 𝑥 ≼ suc 𝑥) |
61 | 60 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ω ∧ suc 𝑥 ≼ 𝑥) → 𝑥 ≼ suc 𝑥) |
62 | | sbthfi 8985 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ Fin ∧ suc 𝑥 ≼ 𝑥 ∧ 𝑥 ≼ suc 𝑥) → suc 𝑥 ≈ 𝑥) |
63 | 32, 62 | syl3an1 1162 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ω ∧ suc 𝑥 ≼ 𝑥 ∧ 𝑥 ≼ suc 𝑥) → suc 𝑥 ≈ 𝑥) |
64 | 61, 63 | mpd3an3 1461 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ω ∧ suc 𝑥 ≼ 𝑥) → suc 𝑥 ≈ 𝑥) |
65 | 52, 56, 64 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ω ∧ suc 𝑥 ≈ 𝐵 ∧ 𝐵 ≼ 𝑥) → suc 𝑥 ≈ 𝑥) |
66 | 65 | 3com23 1125 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ω ∧ 𝐵 ≼ 𝑥 ∧ suc 𝑥 ≈ 𝐵) → suc 𝑥 ≈ 𝑥) |
67 | 66 | 3expia 1120 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ω ∧ 𝐵 ≼ 𝑥) → (suc 𝑥 ≈ 𝐵 → suc 𝑥 ≈ 𝑥)) |
68 | | peano2b 7729 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ω ↔ suc 𝑥 ∈
ω) |
69 | | nnord 7720 |
. . . . . . . . . . . . 13
⊢ (suc
𝑥 ∈ ω → Ord
suc 𝑥) |
70 | 68, 69 | sylbi 216 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ω → Ord suc
𝑥) |
71 | | vex 3436 |
. . . . . . . . . . . . 13
⊢ 𝑥 ∈ V |
72 | 71 | sucid 6345 |
. . . . . . . . . . . 12
⊢ 𝑥 ∈ suc 𝑥 |
73 | | nordeq 6285 |
. . . . . . . . . . . 12
⊢ ((Ord suc
𝑥 ∧ 𝑥 ∈ suc 𝑥) → suc 𝑥 ≠ 𝑥) |
74 | 70, 72, 73 | sylancl 586 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ω → suc 𝑥 ≠ 𝑥) |
75 | | nneneq 8992 |
. . . . . . . . . . . . . 14
⊢ ((suc
𝑥 ∈ ω ∧
𝑥 ∈ ω) →
(suc 𝑥 ≈ 𝑥 ↔ suc 𝑥 = 𝑥)) |
76 | 68, 75 | sylanb 581 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ω ∧ 𝑥 ∈ ω) → (suc
𝑥 ≈ 𝑥 ↔ suc 𝑥 = 𝑥)) |
77 | 76 | anidms 567 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ω → (suc
𝑥 ≈ 𝑥 ↔ suc 𝑥 = 𝑥)) |
78 | 77 | necon3bbid 2981 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ω → (¬
suc 𝑥 ≈ 𝑥 ↔ suc 𝑥 ≠ 𝑥)) |
79 | 74, 78 | mpbird 256 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ω → ¬ suc
𝑥 ≈ 𝑥) |
80 | 67, 79 | nsyli 157 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ω ∧ 𝐵 ≼ 𝑥) → (𝑥 ∈ ω → ¬ suc 𝑥 ≈ 𝐵)) |
81 | 80 | expcom 414 |
. . . . . . . 8
⊢ (𝐵 ≼ 𝑥 → (𝑥 ∈ ω → (𝑥 ∈ ω → ¬ suc 𝑥 ≈ 𝐵))) |
82 | 81 | pm2.43d 53 |
. . . . . . 7
⊢ (𝐵 ≼ 𝑥 → (𝑥 ∈ ω → ¬ suc 𝑥 ≈ 𝐵)) |
83 | 51, 82 | syli 39 |
. . . . . 6
⊢ (𝐵 ⊊ suc 𝑥 → (𝑥 ∈ ω → ¬ suc 𝑥 ≈ 𝐵)) |
84 | 83 | com12 32 |
. . . . 5
⊢ (𝑥 ∈ ω → (𝐵 ⊊ suc 𝑥 → ¬ suc 𝑥 ≈ 𝐵)) |
85 | | psseq2 4023 |
. . . . . 6
⊢ (𝐴 = suc 𝑥 → (𝐵 ⊊ 𝐴 ↔ 𝐵 ⊊ suc 𝑥)) |
86 | | breq1 5077 |
. . . . . . 7
⊢ (𝐴 = suc 𝑥 → (𝐴 ≈ 𝐵 ↔ suc 𝑥 ≈ 𝐵)) |
87 | 86 | notbid 318 |
. . . . . 6
⊢ (𝐴 = suc 𝑥 → (¬ 𝐴 ≈ 𝐵 ↔ ¬ suc 𝑥 ≈ 𝐵)) |
88 | 85, 87 | imbi12d 345 |
. . . . 5
⊢ (𝐴 = suc 𝑥 → ((𝐵 ⊊ 𝐴 → ¬ 𝐴 ≈ 𝐵) ↔ (𝐵 ⊊ suc 𝑥 → ¬ suc 𝑥 ≈ 𝐵))) |
89 | 84, 88 | syl5ibrcom 246 |
. . . 4
⊢ (𝑥 ∈ ω → (𝐴 = suc 𝑥 → (𝐵 ⊊ 𝐴 → ¬ 𝐴 ≈ 𝐵))) |
90 | 89 | rexlimiv 3209 |
. . 3
⊢
(∃𝑥 ∈
ω 𝐴 = suc 𝑥 → (𝐵 ⊊ 𝐴 → ¬ 𝐴 ≈ 𝐵)) |
91 | 10, 90 | syl 17 |
. 2
⊢ ((𝐴 ∈ ω ∧ 𝐵 ⊊ 𝐴) → (𝐵 ⊊ 𝐴 → ¬ 𝐴 ≈ 𝐵)) |
92 | 91 | syldbl2 838 |
1
⊢ ((𝐴 ∈ ω ∧ 𝐵 ⊊ 𝐴) → ¬ 𝐴 ≈ 𝐵) |