Step | Hyp | Ref
| Expression |
1 | | pssss 3986 |
. . . 4
⊢ (𝐵 ⊊ 𝐴 → 𝐵 ⊆ 𝐴) |
2 | | ssexg 5191 |
. . . 4
⊢ ((𝐵 ⊆ 𝐴 ∧ 𝐴 ∈ ω) → 𝐵 ∈ V) |
3 | 1, 2 | sylan 583 |
. . 3
⊢ ((𝐵 ⊊ 𝐴 ∧ 𝐴 ∈ ω) → 𝐵 ∈ V) |
4 | 3 | ancoms 462 |
. 2
⊢ ((𝐴 ∈ ω ∧ 𝐵 ⊊ 𝐴) → 𝐵 ∈ V) |
5 | | psseq2 3979 |
. . . . . . . 8
⊢ (𝑧 = ∅ → (𝑤 ⊊ 𝑧 ↔ 𝑤 ⊊ ∅)) |
6 | | rexeq 3311 |
. . . . . . . 8
⊢ (𝑧 = ∅ → (∃𝑥 ∈ 𝑧 𝑤 ≈ 𝑥 ↔ ∃𝑥 ∈ ∅ 𝑤 ≈ 𝑥)) |
7 | 5, 6 | imbi12d 348 |
. . . . . . 7
⊢ (𝑧 = ∅ → ((𝑤 ⊊ 𝑧 → ∃𝑥 ∈ 𝑧 𝑤 ≈ 𝑥) ↔ (𝑤 ⊊ ∅ → ∃𝑥 ∈ ∅ 𝑤 ≈ 𝑥))) |
8 | 7 | albidv 1927 |
. . . . . 6
⊢ (𝑧 = ∅ → (∀𝑤(𝑤 ⊊ 𝑧 → ∃𝑥 ∈ 𝑧 𝑤 ≈ 𝑥) ↔ ∀𝑤(𝑤 ⊊ ∅ → ∃𝑥 ∈ ∅ 𝑤 ≈ 𝑥))) |
9 | | psseq2 3979 |
. . . . . . . 8
⊢ (𝑧 = 𝑦 → (𝑤 ⊊ 𝑧 ↔ 𝑤 ⊊ 𝑦)) |
10 | | rexeq 3311 |
. . . . . . . 8
⊢ (𝑧 = 𝑦 → (∃𝑥 ∈ 𝑧 𝑤 ≈ 𝑥 ↔ ∃𝑥 ∈ 𝑦 𝑤 ≈ 𝑥)) |
11 | 9, 10 | imbi12d 348 |
. . . . . . 7
⊢ (𝑧 = 𝑦 → ((𝑤 ⊊ 𝑧 → ∃𝑥 ∈ 𝑧 𝑤 ≈ 𝑥) ↔ (𝑤 ⊊ 𝑦 → ∃𝑥 ∈ 𝑦 𝑤 ≈ 𝑥))) |
12 | 11 | albidv 1927 |
. . . . . 6
⊢ (𝑧 = 𝑦 → (∀𝑤(𝑤 ⊊ 𝑧 → ∃𝑥 ∈ 𝑧 𝑤 ≈ 𝑥) ↔ ∀𝑤(𝑤 ⊊ 𝑦 → ∃𝑥 ∈ 𝑦 𝑤 ≈ 𝑥))) |
13 | | psseq2 3979 |
. . . . . . . 8
⊢ (𝑧 = suc 𝑦 → (𝑤 ⊊ 𝑧 ↔ 𝑤 ⊊ suc 𝑦)) |
14 | | rexeq 3311 |
. . . . . . . 8
⊢ (𝑧 = suc 𝑦 → (∃𝑥 ∈ 𝑧 𝑤 ≈ 𝑥 ↔ ∃𝑥 ∈ suc 𝑦𝑤 ≈ 𝑥)) |
15 | 13, 14 | imbi12d 348 |
. . . . . . 7
⊢ (𝑧 = suc 𝑦 → ((𝑤 ⊊ 𝑧 → ∃𝑥 ∈ 𝑧 𝑤 ≈ 𝑥) ↔ (𝑤 ⊊ suc 𝑦 → ∃𝑥 ∈ suc 𝑦𝑤 ≈ 𝑥))) |
16 | 15 | albidv 1927 |
. . . . . 6
⊢ (𝑧 = suc 𝑦 → (∀𝑤(𝑤 ⊊ 𝑧 → ∃𝑥 ∈ 𝑧 𝑤 ≈ 𝑥) ↔ ∀𝑤(𝑤 ⊊ suc 𝑦 → ∃𝑥 ∈ suc 𝑦𝑤 ≈ 𝑥))) |
17 | | psseq2 3979 |
. . . . . . . 8
⊢ (𝑧 = 𝐴 → (𝑤 ⊊ 𝑧 ↔ 𝑤 ⊊ 𝐴)) |
18 | | rexeq 3311 |
. . . . . . . 8
⊢ (𝑧 = 𝐴 → (∃𝑥 ∈ 𝑧 𝑤 ≈ 𝑥 ↔ ∃𝑥 ∈ 𝐴 𝑤 ≈ 𝑥)) |
19 | 17, 18 | imbi12d 348 |
. . . . . . 7
⊢ (𝑧 = 𝐴 → ((𝑤 ⊊ 𝑧 → ∃𝑥 ∈ 𝑧 𝑤 ≈ 𝑥) ↔ (𝑤 ⊊ 𝐴 → ∃𝑥 ∈ 𝐴 𝑤 ≈ 𝑥))) |
20 | 19 | albidv 1927 |
. . . . . 6
⊢ (𝑧 = 𝐴 → (∀𝑤(𝑤 ⊊ 𝑧 → ∃𝑥 ∈ 𝑧 𝑤 ≈ 𝑥) ↔ ∀𝑤(𝑤 ⊊ 𝐴 → ∃𝑥 ∈ 𝐴 𝑤 ≈ 𝑥))) |
21 | | npss0 4335 |
. . . . . . . 8
⊢ ¬
𝑤 ⊊
∅ |
22 | 21 | pm2.21i 119 |
. . . . . . 7
⊢ (𝑤 ⊊ ∅ →
∃𝑥 ∈ ∅
𝑤 ≈ 𝑥) |
23 | 22 | ax-gen 1802 |
. . . . . 6
⊢
∀𝑤(𝑤 ⊊ ∅ →
∃𝑥 ∈ ∅
𝑤 ≈ 𝑥) |
24 | | nfv 1921 |
. . . . . . 7
⊢
Ⅎ𝑤 𝑦 ∈ ω |
25 | | nfa1 2156 |
. . . . . . 7
⊢
Ⅎ𝑤∀𝑤(𝑤 ⊊ 𝑦 → ∃𝑥 ∈ 𝑦 𝑤 ≈ 𝑥) |
26 | | elequ1 2121 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑧 = 𝑦 → (𝑧 ∈ 𝑤 ↔ 𝑦 ∈ 𝑤)) |
27 | 26 | biimpcd 252 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑧 ∈ 𝑤 → (𝑧 = 𝑦 → 𝑦 ∈ 𝑤)) |
28 | 27 | con3d 155 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 ∈ 𝑤 → (¬ 𝑦 ∈ 𝑤 → ¬ 𝑧 = 𝑦)) |
29 | 28 | adantl 485 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑤 ⊊ suc 𝑦 ∧ 𝑧 ∈ 𝑤) → (¬ 𝑦 ∈ 𝑤 → ¬ 𝑧 = 𝑦)) |
30 | | pssss 3986 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑤 ⊊ suc 𝑦 → 𝑤 ⊆ suc 𝑦) |
31 | 30 | sseld 3876 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑤 ⊊ suc 𝑦 → (𝑧 ∈ 𝑤 → 𝑧 ∈ suc 𝑦)) |
32 | | elsuci 6238 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑧 ∈ suc 𝑦 → (𝑧 ∈ 𝑦 ∨ 𝑧 = 𝑦)) |
33 | 32 | ord 863 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑧 ∈ suc 𝑦 → (¬ 𝑧 ∈ 𝑦 → 𝑧 = 𝑦)) |
34 | 33 | con1d 147 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑧 ∈ suc 𝑦 → (¬ 𝑧 = 𝑦 → 𝑧 ∈ 𝑦)) |
35 | 31, 34 | syl6 35 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑤 ⊊ suc 𝑦 → (𝑧 ∈ 𝑤 → (¬ 𝑧 = 𝑦 → 𝑧 ∈ 𝑦))) |
36 | 35 | imp 410 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑤 ⊊ suc 𝑦 ∧ 𝑧 ∈ 𝑤) → (¬ 𝑧 = 𝑦 → 𝑧 ∈ 𝑦)) |
37 | 29, 36 | syld 47 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑤 ⊊ suc 𝑦 ∧ 𝑧 ∈ 𝑤) → (¬ 𝑦 ∈ 𝑤 → 𝑧 ∈ 𝑦)) |
38 | 37 | impancom 455 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑤 ⊊ suc 𝑦 ∧ ¬ 𝑦 ∈ 𝑤) → (𝑧 ∈ 𝑤 → 𝑧 ∈ 𝑦)) |
39 | 38 | ssrdv 3883 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑤 ⊊ suc 𝑦 ∧ ¬ 𝑦 ∈ 𝑤) → 𝑤 ⊆ 𝑦) |
40 | 39 | anim1i 618 |
. . . . . . . . . . . . . . 15
⊢ (((𝑤 ⊊ suc 𝑦 ∧ ¬ 𝑦 ∈ 𝑤) ∧ ¬ 𝑤 = 𝑦) → (𝑤 ⊆ 𝑦 ∧ ¬ 𝑤 = 𝑦)) |
41 | | dfpss2 3976 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 ⊊ 𝑦 ↔ (𝑤 ⊆ 𝑦 ∧ ¬ 𝑤 = 𝑦)) |
42 | 40, 41 | sylibr 237 |
. . . . . . . . . . . . . 14
⊢ (((𝑤 ⊊ suc 𝑦 ∧ ¬ 𝑦 ∈ 𝑤) ∧ ¬ 𝑤 = 𝑦) → 𝑤 ⊊ 𝑦) |
43 | | elelsuc 6244 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ 𝑦 → 𝑥 ∈ suc 𝑦) |
44 | 43 | anim1i 618 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ 𝑦 ∧ 𝑤 ≈ 𝑥) → (𝑥 ∈ suc 𝑦 ∧ 𝑤 ≈ 𝑥)) |
45 | 44 | reximi2 3158 |
. . . . . . . . . . . . . 14
⊢
(∃𝑥 ∈
𝑦 𝑤 ≈ 𝑥 → ∃𝑥 ∈ suc 𝑦𝑤 ≈ 𝑥) |
46 | 42, 45 | imim12i 62 |
. . . . . . . . . . . . 13
⊢ ((𝑤 ⊊ 𝑦 → ∃𝑥 ∈ 𝑦 𝑤 ≈ 𝑥) → (((𝑤 ⊊ suc 𝑦 ∧ ¬ 𝑦 ∈ 𝑤) ∧ ¬ 𝑤 = 𝑦) → ∃𝑥 ∈ suc 𝑦𝑤 ≈ 𝑥)) |
47 | 46 | exp4c 436 |
. . . . . . . . . . . 12
⊢ ((𝑤 ⊊ 𝑦 → ∃𝑥 ∈ 𝑦 𝑤 ≈ 𝑥) → (𝑤 ⊊ suc 𝑦 → (¬ 𝑦 ∈ 𝑤 → (¬ 𝑤 = 𝑦 → ∃𝑥 ∈ suc 𝑦𝑤 ≈ 𝑥)))) |
48 | 47 | sps 2186 |
. . . . . . . . . . 11
⊢
(∀𝑤(𝑤 ⊊ 𝑦 → ∃𝑥 ∈ 𝑦 𝑤 ≈ 𝑥) → (𝑤 ⊊ suc 𝑦 → (¬ 𝑦 ∈ 𝑤 → (¬ 𝑤 = 𝑦 → ∃𝑥 ∈ suc 𝑦𝑤 ≈ 𝑥)))) |
49 | 48 | adantl 485 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ ω ∧
∀𝑤(𝑤 ⊊ 𝑦 → ∃𝑥 ∈ 𝑦 𝑤 ≈ 𝑥)) → (𝑤 ⊊ suc 𝑦 → (¬ 𝑦 ∈ 𝑤 → (¬ 𝑤 = 𝑦 → ∃𝑥 ∈ suc 𝑦𝑤 ≈ 𝑥)))) |
50 | 49 | com4t 93 |
. . . . . . . . 9
⊢ (¬
𝑦 ∈ 𝑤 → (¬ 𝑤 = 𝑦 → ((𝑦 ∈ ω ∧ ∀𝑤(𝑤 ⊊ 𝑦 → ∃𝑥 ∈ 𝑦 𝑤 ≈ 𝑥)) → (𝑤 ⊊ suc 𝑦 → ∃𝑥 ∈ suc 𝑦𝑤 ≈ 𝑥)))) |
51 | | anidm 568 |
. . . . . . . . . . . . . 14
⊢ ((𝑤 ⊊ suc 𝑦 ∧ 𝑤 ⊊ suc 𝑦) ↔ 𝑤 ⊊ suc 𝑦) |
52 | | ssdif 4030 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 ⊆ suc 𝑦 → (𝑤 ∖ {𝑦}) ⊆ (suc 𝑦 ∖ {𝑦})) |
53 | | nnord 7607 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ∈ ω → Ord 𝑦) |
54 | | orddif 6265 |
. . . . . . . . . . . . . . . . . . 19
⊢ (Ord
𝑦 → 𝑦 = (suc 𝑦 ∖ {𝑦})) |
55 | 53, 54 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ ω → 𝑦 = (suc 𝑦 ∖ {𝑦})) |
56 | 55 | sseq2d 3909 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ ω → ((𝑤 ∖ {𝑦}) ⊆ 𝑦 ↔ (𝑤 ∖ {𝑦}) ⊆ (suc 𝑦 ∖ {𝑦}))) |
57 | 52, 56 | syl5ibr 249 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ ω → (𝑤 ⊆ suc 𝑦 → (𝑤 ∖ {𝑦}) ⊆ 𝑦)) |
58 | 30, 57 | syl5 34 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ω → (𝑤 ⊊ suc 𝑦 → (𝑤 ∖ {𝑦}) ⊆ 𝑦)) |
59 | | pssnel 4360 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 ⊊ suc 𝑦 → ∃𝑧(𝑧 ∈ suc 𝑦 ∧ ¬ 𝑧 ∈ 𝑤)) |
60 | | eleq2 2821 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑤 ∖ {𝑦}) = 𝑦 → (𝑧 ∈ (𝑤 ∖ {𝑦}) ↔ 𝑧 ∈ 𝑦)) |
61 | | eldifi 4017 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑧 ∈ (𝑤 ∖ {𝑦}) → 𝑧 ∈ 𝑤) |
62 | 60, 61 | syl6bir 257 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑤 ∖ {𝑦}) = 𝑦 → (𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑤)) |
63 | 62 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑦 ∈ 𝑤 ∧ 𝑧 ∈ suc 𝑦) ∧ (𝑤 ∖ {𝑦}) = 𝑦) → (𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑤)) |
64 | | eleq1a 2828 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑦 ∈ 𝑤 → (𝑧 = 𝑦 → 𝑧 ∈ 𝑤)) |
65 | 33, 64 | sylan9r 512 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑦 ∈ 𝑤 ∧ 𝑧 ∈ suc 𝑦) → (¬ 𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑤)) |
66 | 65 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑦 ∈ 𝑤 ∧ 𝑧 ∈ suc 𝑦) ∧ (𝑤 ∖ {𝑦}) = 𝑦) → (¬ 𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑤)) |
67 | 63, 66 | pm2.61d 182 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑦 ∈ 𝑤 ∧ 𝑧 ∈ suc 𝑦) ∧ (𝑤 ∖ {𝑦}) = 𝑦) → 𝑧 ∈ 𝑤) |
68 | 67 | ex 416 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑦 ∈ 𝑤 ∧ 𝑧 ∈ suc 𝑦) → ((𝑤 ∖ {𝑦}) = 𝑦 → 𝑧 ∈ 𝑤)) |
69 | 68 | con3d 155 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ∈ 𝑤 ∧ 𝑧 ∈ suc 𝑦) → (¬ 𝑧 ∈ 𝑤 → ¬ (𝑤 ∖ {𝑦}) = 𝑦)) |
70 | 69 | expimpd 457 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ 𝑤 → ((𝑧 ∈ suc 𝑦 ∧ ¬ 𝑧 ∈ 𝑤) → ¬ (𝑤 ∖ {𝑦}) = 𝑦)) |
71 | 70 | exlimdv 1940 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ 𝑤 → (∃𝑧(𝑧 ∈ suc 𝑦 ∧ ¬ 𝑧 ∈ 𝑤) → ¬ (𝑤 ∖ {𝑦}) = 𝑦)) |
72 | 59, 71 | syl5 34 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ 𝑤 → (𝑤 ⊊ suc 𝑦 → ¬ (𝑤 ∖ {𝑦}) = 𝑦)) |
73 | 58, 72 | im2anan9r 624 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ 𝑤 ∧ 𝑦 ∈ ω) → ((𝑤 ⊊ suc 𝑦 ∧ 𝑤 ⊊ suc 𝑦) → ((𝑤 ∖ {𝑦}) ⊆ 𝑦 ∧ ¬ (𝑤 ∖ {𝑦}) = 𝑦))) |
74 | 51, 73 | syl5bir 246 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ 𝑤 ∧ 𝑦 ∈ ω) → (𝑤 ⊊ suc 𝑦 → ((𝑤 ∖ {𝑦}) ⊆ 𝑦 ∧ ¬ (𝑤 ∖ {𝑦}) = 𝑦))) |
75 | | dfpss2 3976 |
. . . . . . . . . . . . 13
⊢ ((𝑤 ∖ {𝑦}) ⊊ 𝑦 ↔ ((𝑤 ∖ {𝑦}) ⊆ 𝑦 ∧ ¬ (𝑤 ∖ {𝑦}) = 𝑦)) |
76 | 74, 75 | syl6ibr 255 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ 𝑤 ∧ 𝑦 ∈ ω) → (𝑤 ⊊ suc 𝑦 → (𝑤 ∖ {𝑦}) ⊊ 𝑦)) |
77 | | psseq1 3978 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 = 𝑧 → (𝑤 ⊊ 𝑦 ↔ 𝑧 ⊊ 𝑦)) |
78 | | breq1 5033 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 = 𝑧 → (𝑤 ≈ 𝑥 ↔ 𝑧 ≈ 𝑥)) |
79 | 78 | rexbidv 3207 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 = 𝑧 → (∃𝑥 ∈ 𝑦 𝑤 ≈ 𝑥 ↔ ∃𝑥 ∈ 𝑦 𝑧 ≈ 𝑥)) |
80 | 77, 79 | imbi12d 348 |
. . . . . . . . . . . . . 14
⊢ (𝑤 = 𝑧 → ((𝑤 ⊊ 𝑦 → ∃𝑥 ∈ 𝑦 𝑤 ≈ 𝑥) ↔ (𝑧 ⊊ 𝑦 → ∃𝑥 ∈ 𝑦 𝑧 ≈ 𝑥))) |
81 | 80 | cbvalvw 2048 |
. . . . . . . . . . . . 13
⊢
(∀𝑤(𝑤 ⊊ 𝑦 → ∃𝑥 ∈ 𝑦 𝑤 ≈ 𝑥) ↔ ∀𝑧(𝑧 ⊊ 𝑦 → ∃𝑥 ∈ 𝑦 𝑧 ≈ 𝑥)) |
82 | | vex 3402 |
. . . . . . . . . . . . . . 15
⊢ 𝑤 ∈ V |
83 | 82 | difexi 5196 |
. . . . . . . . . . . . . 14
⊢ (𝑤 ∖ {𝑦}) ∈ V |
84 | | psseq1 3978 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = (𝑤 ∖ {𝑦}) → (𝑧 ⊊ 𝑦 ↔ (𝑤 ∖ {𝑦}) ⊊ 𝑦)) |
85 | | breq1 5033 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = (𝑤 ∖ {𝑦}) → (𝑧 ≈ 𝑥 ↔ (𝑤 ∖ {𝑦}) ≈ 𝑥)) |
86 | 85 | rexbidv 3207 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = (𝑤 ∖ {𝑦}) → (∃𝑥 ∈ 𝑦 𝑧 ≈ 𝑥 ↔ ∃𝑥 ∈ 𝑦 (𝑤 ∖ {𝑦}) ≈ 𝑥)) |
87 | 84, 86 | imbi12d 348 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = (𝑤 ∖ {𝑦}) → ((𝑧 ⊊ 𝑦 → ∃𝑥 ∈ 𝑦 𝑧 ≈ 𝑥) ↔ ((𝑤 ∖ {𝑦}) ⊊ 𝑦 → ∃𝑥 ∈ 𝑦 (𝑤 ∖ {𝑦}) ≈ 𝑥))) |
88 | 83, 87 | spcv 3509 |
. . . . . . . . . . . . 13
⊢
(∀𝑧(𝑧 ⊊ 𝑦 → ∃𝑥 ∈ 𝑦 𝑧 ≈ 𝑥) → ((𝑤 ∖ {𝑦}) ⊊ 𝑦 → ∃𝑥 ∈ 𝑦 (𝑤 ∖ {𝑦}) ≈ 𝑥)) |
89 | 81, 88 | sylbi 220 |
. . . . . . . . . . . 12
⊢
(∀𝑤(𝑤 ⊊ 𝑦 → ∃𝑥 ∈ 𝑦 𝑤 ≈ 𝑥) → ((𝑤 ∖ {𝑦}) ⊊ 𝑦 → ∃𝑥 ∈ 𝑦 (𝑤 ∖ {𝑦}) ≈ 𝑥)) |
90 | 76, 89 | sylan9 511 |
. . . . . . . . . . 11
⊢ (((𝑦 ∈ 𝑤 ∧ 𝑦 ∈ ω) ∧ ∀𝑤(𝑤 ⊊ 𝑦 → ∃𝑥 ∈ 𝑦 𝑤 ≈ 𝑥)) → (𝑤 ⊊ suc 𝑦 → ∃𝑥 ∈ 𝑦 (𝑤 ∖ {𝑦}) ≈ 𝑥)) |
91 | | ordsucelsuc 7556 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (Ord
𝑦 → (𝑥 ∈ 𝑦 ↔ suc 𝑥 ∈ suc 𝑦)) |
92 | 91 | biimpd 232 |
. . . . . . . . . . . . . . . . . . 19
⊢ (Ord
𝑦 → (𝑥 ∈ 𝑦 → suc 𝑥 ∈ suc 𝑦)) |
93 | 53, 92 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ ω → (𝑥 ∈ 𝑦 → suc 𝑥 ∈ suc 𝑦)) |
94 | 93 | adantl 485 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ 𝑤 ∧ 𝑦 ∈ ω) → (𝑥 ∈ 𝑦 → suc 𝑥 ∈ suc 𝑦)) |
95 | 94 | adantrd 495 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ 𝑤 ∧ 𝑦 ∈ ω) → ((𝑥 ∈ 𝑦 ∧ (𝑤 ∖ {𝑦}) ≈ 𝑥) → suc 𝑥 ∈ suc 𝑦)) |
96 | | elnn 7609 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ ω) → 𝑥 ∈ ω) |
97 | | snex 5298 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
{〈𝑦, 𝑥〉} ∈
V |
98 | | vex 3402 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 𝑦 ∈ V |
99 | | vex 3402 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 𝑥 ∈ V |
100 | 98, 99 | f1osn 6657 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
{〈𝑦, 𝑥〉}:{𝑦}–1-1-onto→{𝑥} |
101 | | f1oen3g 8571 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(({〈𝑦, 𝑥〉} ∈ V ∧
{〈𝑦, 𝑥〉}:{𝑦}–1-1-onto→{𝑥}) → {𝑦} ≈ {𝑥}) |
102 | 97, 100, 101 | mp2an 692 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ {𝑦} ≈ {𝑥} |
103 | 102 | jctr 528 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑤 ∖ {𝑦}) ≈ 𝑥 → ((𝑤 ∖ {𝑦}) ≈ 𝑥 ∧ {𝑦} ≈ {𝑥})) |
104 | | nnord 7607 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥 ∈ ω → Ord 𝑥) |
105 | | orddisj 6210 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (Ord
𝑥 → (𝑥 ∩ {𝑥}) = ∅) |
106 | 104, 105 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 ∈ ω → (𝑥 ∩ {𝑥}) = ∅) |
107 | | incom 4091 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ({𝑦} ∩ (𝑤 ∖ {𝑦})) = ((𝑤 ∖ {𝑦}) ∩ {𝑦}) |
108 | | disjdif 4361 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ({𝑦} ∩ (𝑤 ∖ {𝑦})) = ∅ |
109 | 107, 108 | eqtr3i 2763 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑤 ∖ {𝑦}) ∩ {𝑦}) = ∅ |
110 | 106, 109 | jctil 523 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 ∈ ω → (((𝑤 ∖ {𝑦}) ∩ {𝑦}) = ∅ ∧ (𝑥 ∩ {𝑥}) = ∅)) |
111 | | unen 8644 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑤 ∖ {𝑦}) ≈ 𝑥 ∧ {𝑦} ≈ {𝑥}) ∧ (((𝑤 ∖ {𝑦}) ∩ {𝑦}) = ∅ ∧ (𝑥 ∩ {𝑥}) = ∅)) → ((𝑤 ∖ {𝑦}) ∪ {𝑦}) ≈ (𝑥 ∪ {𝑥})) |
112 | 103, 110,
111 | syl2an 599 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑤 ∖ {𝑦}) ≈ 𝑥 ∧ 𝑥 ∈ ω) → ((𝑤 ∖ {𝑦}) ∪ {𝑦}) ≈ (𝑥 ∪ {𝑥})) |
113 | | difsnid 4698 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑦 ∈ 𝑤 → ((𝑤 ∖ {𝑦}) ∪ {𝑦}) = 𝑤) |
114 | 113 | eqcomd 2744 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑦 ∈ 𝑤 → 𝑤 = ((𝑤 ∖ {𝑦}) ∪ {𝑦})) |
115 | | df-suc 6178 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ suc 𝑥 = (𝑥 ∪ {𝑥}) |
116 | 115 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑦 ∈ 𝑤 → suc 𝑥 = (𝑥 ∪ {𝑥})) |
117 | 114, 116 | breq12d 5043 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 ∈ 𝑤 → (𝑤 ≈ suc 𝑥 ↔ ((𝑤 ∖ {𝑦}) ∪ {𝑦}) ≈ (𝑥 ∪ {𝑥}))) |
118 | 112, 117 | syl5ibr 249 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 ∈ 𝑤 → (((𝑤 ∖ {𝑦}) ≈ 𝑥 ∧ 𝑥 ∈ ω) → 𝑤 ≈ suc 𝑥)) |
119 | 96, 118 | sylan2i 609 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ∈ 𝑤 → (((𝑤 ∖ {𝑦}) ≈ 𝑥 ∧ (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ ω)) → 𝑤 ≈ suc 𝑥)) |
120 | 119 | exp4d 437 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ 𝑤 → ((𝑤 ∖ {𝑦}) ≈ 𝑥 → (𝑥 ∈ 𝑦 → (𝑦 ∈ ω → 𝑤 ≈ suc 𝑥)))) |
121 | 120 | com24 95 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ 𝑤 → (𝑦 ∈ ω → (𝑥 ∈ 𝑦 → ((𝑤 ∖ {𝑦}) ≈ 𝑥 → 𝑤 ≈ suc 𝑥)))) |
122 | 121 | imp4b 425 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ 𝑤 ∧ 𝑦 ∈ ω) → ((𝑥 ∈ 𝑦 ∧ (𝑤 ∖ {𝑦}) ≈ 𝑥) → 𝑤 ≈ suc 𝑥)) |
123 | 95, 122 | jcad 516 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ 𝑤 ∧ 𝑦 ∈ ω) → ((𝑥 ∈ 𝑦 ∧ (𝑤 ∖ {𝑦}) ≈ 𝑥) → (suc 𝑥 ∈ suc 𝑦 ∧ 𝑤 ≈ suc 𝑥))) |
124 | | breq2 5034 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = suc 𝑥 → (𝑤 ≈ 𝑧 ↔ 𝑤 ≈ suc 𝑥)) |
125 | 124 | rspcev 3526 |
. . . . . . . . . . . . . . 15
⊢ ((suc
𝑥 ∈ suc 𝑦 ∧ 𝑤 ≈ suc 𝑥) → ∃𝑧 ∈ suc 𝑦𝑤 ≈ 𝑧) |
126 | 123, 125 | syl6 35 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ 𝑤 ∧ 𝑦 ∈ ω) → ((𝑥 ∈ 𝑦 ∧ (𝑤 ∖ {𝑦}) ≈ 𝑥) → ∃𝑧 ∈ suc 𝑦𝑤 ≈ 𝑧)) |
127 | 126 | exlimdv 1940 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ 𝑤 ∧ 𝑦 ∈ ω) → (∃𝑥(𝑥 ∈ 𝑦 ∧ (𝑤 ∖ {𝑦}) ≈ 𝑥) → ∃𝑧 ∈ suc 𝑦𝑤 ≈ 𝑧)) |
128 | | df-rex 3059 |
. . . . . . . . . . . . 13
⊢
(∃𝑥 ∈
𝑦 (𝑤 ∖ {𝑦}) ≈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ (𝑤 ∖ {𝑦}) ≈ 𝑥)) |
129 | | breq2 5034 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑧 → (𝑤 ≈ 𝑥 ↔ 𝑤 ≈ 𝑧)) |
130 | 129 | cbvrexvw 3350 |
. . . . . . . . . . . . 13
⊢
(∃𝑥 ∈ suc
𝑦𝑤 ≈ 𝑥 ↔ ∃𝑧 ∈ suc 𝑦𝑤 ≈ 𝑧) |
131 | 127, 128,
130 | 3imtr4g 299 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ 𝑤 ∧ 𝑦 ∈ ω) → (∃𝑥 ∈ 𝑦 (𝑤 ∖ {𝑦}) ≈ 𝑥 → ∃𝑥 ∈ suc 𝑦𝑤 ≈ 𝑥)) |
132 | 131 | adantr 484 |
. . . . . . . . . . 11
⊢ (((𝑦 ∈ 𝑤 ∧ 𝑦 ∈ ω) ∧ ∀𝑤(𝑤 ⊊ 𝑦 → ∃𝑥 ∈ 𝑦 𝑤 ≈ 𝑥)) → (∃𝑥 ∈ 𝑦 (𝑤 ∖ {𝑦}) ≈ 𝑥 → ∃𝑥 ∈ suc 𝑦𝑤 ≈ 𝑥)) |
133 | 90, 132 | syld 47 |
. . . . . . . . . 10
⊢ (((𝑦 ∈ 𝑤 ∧ 𝑦 ∈ ω) ∧ ∀𝑤(𝑤 ⊊ 𝑦 → ∃𝑥 ∈ 𝑦 𝑤 ≈ 𝑥)) → (𝑤 ⊊ suc 𝑦 → ∃𝑥 ∈ suc 𝑦𝑤 ≈ 𝑥)) |
134 | 133 | expl 461 |
. . . . . . . . 9
⊢ (𝑦 ∈ 𝑤 → ((𝑦 ∈ ω ∧ ∀𝑤(𝑤 ⊊ 𝑦 → ∃𝑥 ∈ 𝑦 𝑤 ≈ 𝑥)) → (𝑤 ⊊ suc 𝑦 → ∃𝑥 ∈ suc 𝑦𝑤 ≈ 𝑥))) |
135 | 82 | eqelsuc 6253 |
. . . . . . . . . . 11
⊢ (𝑤 = 𝑦 → 𝑤 ∈ suc 𝑦) |
136 | 82 | enref 8588 |
. . . . . . . . . . 11
⊢ 𝑤 ≈ 𝑤 |
137 | | breq2 5034 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑤 → (𝑤 ≈ 𝑥 ↔ 𝑤 ≈ 𝑤)) |
138 | 137 | rspcev 3526 |
. . . . . . . . . . 11
⊢ ((𝑤 ∈ suc 𝑦 ∧ 𝑤 ≈ 𝑤) → ∃𝑥 ∈ suc 𝑦𝑤 ≈ 𝑥) |
139 | 135, 136,
138 | sylancl 589 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑦 → ∃𝑥 ∈ suc 𝑦𝑤 ≈ 𝑥) |
140 | 139 | 2a1d 26 |
. . . . . . . . 9
⊢ (𝑤 = 𝑦 → ((𝑦 ∈ ω ∧ ∀𝑤(𝑤 ⊊ 𝑦 → ∃𝑥 ∈ 𝑦 𝑤 ≈ 𝑥)) → (𝑤 ⊊ suc 𝑦 → ∃𝑥 ∈ suc 𝑦𝑤 ≈ 𝑥))) |
141 | 50, 134, 140 | pm2.61ii 186 |
. . . . . . . 8
⊢ ((𝑦 ∈ ω ∧
∀𝑤(𝑤 ⊊ 𝑦 → ∃𝑥 ∈ 𝑦 𝑤 ≈ 𝑥)) → (𝑤 ⊊ suc 𝑦 → ∃𝑥 ∈ suc 𝑦𝑤 ≈ 𝑥)) |
142 | 141 | ex 416 |
. . . . . . 7
⊢ (𝑦 ∈ ω →
(∀𝑤(𝑤 ⊊ 𝑦 → ∃𝑥 ∈ 𝑦 𝑤 ≈ 𝑥) → (𝑤 ⊊ suc 𝑦 → ∃𝑥 ∈ suc 𝑦𝑤 ≈ 𝑥))) |
143 | 24, 25, 142 | alrimd 2217 |
. . . . . 6
⊢ (𝑦 ∈ ω →
(∀𝑤(𝑤 ⊊ 𝑦 → ∃𝑥 ∈ 𝑦 𝑤 ≈ 𝑥) → ∀𝑤(𝑤 ⊊ suc 𝑦 → ∃𝑥 ∈ suc 𝑦𝑤 ≈ 𝑥))) |
144 | 8, 12, 16, 20, 23, 143 | finds 7629 |
. . . . 5
⊢ (𝐴 ∈ ω →
∀𝑤(𝑤 ⊊ 𝐴 → ∃𝑥 ∈ 𝐴 𝑤 ≈ 𝑥)) |
145 | | psseq1 3978 |
. . . . . . 7
⊢ (𝑤 = 𝐵 → (𝑤 ⊊ 𝐴 ↔ 𝐵 ⊊ 𝐴)) |
146 | | breq1 5033 |
. . . . . . . 8
⊢ (𝑤 = 𝐵 → (𝑤 ≈ 𝑥 ↔ 𝐵 ≈ 𝑥)) |
147 | 146 | rexbidv 3207 |
. . . . . . 7
⊢ (𝑤 = 𝐵 → (∃𝑥 ∈ 𝐴 𝑤 ≈ 𝑥 ↔ ∃𝑥 ∈ 𝐴 𝐵 ≈ 𝑥)) |
148 | 145, 147 | imbi12d 348 |
. . . . . 6
⊢ (𝑤 = 𝐵 → ((𝑤 ⊊ 𝐴 → ∃𝑥 ∈ 𝐴 𝑤 ≈ 𝑥) ↔ (𝐵 ⊊ 𝐴 → ∃𝑥 ∈ 𝐴 𝐵 ≈ 𝑥))) |
149 | 148 | spcgv 3500 |
. . . . 5
⊢ (𝐵 ∈ V → (∀𝑤(𝑤 ⊊ 𝐴 → ∃𝑥 ∈ 𝐴 𝑤 ≈ 𝑥) → (𝐵 ⊊ 𝐴 → ∃𝑥 ∈ 𝐴 𝐵 ≈ 𝑥))) |
150 | 144, 149 | syl5 34 |
. . . 4
⊢ (𝐵 ∈ V → (𝐴 ∈ ω → (𝐵 ⊊ 𝐴 → ∃𝑥 ∈ 𝐴 𝐵 ≈ 𝑥))) |
151 | 150 | com3l 89 |
. . 3
⊢ (𝐴 ∈ ω → (𝐵 ⊊ 𝐴 → (𝐵 ∈ V → ∃𝑥 ∈ 𝐴 𝐵 ≈ 𝑥))) |
152 | 151 | imp 410 |
. 2
⊢ ((𝐴 ∈ ω ∧ 𝐵 ⊊ 𝐴) → (𝐵 ∈ V → ∃𝑥 ∈ 𝐴 𝐵 ≈ 𝑥)) |
153 | 4, 152 | mpd 15 |
1
⊢ ((𝐴 ∈ ω ∧ 𝐵 ⊊ 𝐴) → ∃𝑥 ∈ 𝐴 𝐵 ≈ 𝑥) |