Step | Hyp | Ref
| Expression |
1 | | isf32lem.a |
. . . 4
⊢ (𝜑 → 𝐹:ω⟶𝒫 𝐺) |
2 | | isf32lem.b |
. . . 4
⊢ (𝜑 → ∀𝑥 ∈ ω (𝐹‘suc 𝑥) ⊆ (𝐹‘𝑥)) |
3 | | isf32lem.c |
. . . 4
⊢ (𝜑 → ¬ ∩ ran 𝐹 ∈ ran 𝐹) |
4 | 1, 2, 3 | isf32lem2 9770 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ ω) → ∃𝑏 ∈ ω (𝑎 ∈ 𝑏 ∧ (𝐹‘suc 𝑏) ⊊ (𝐹‘𝑏))) |
5 | 4 | ralrimiva 3182 |
. 2
⊢ (𝜑 → ∀𝑎 ∈ ω ∃𝑏 ∈ ω (𝑎 ∈ 𝑏 ∧ (𝐹‘suc 𝑏) ⊊ (𝐹‘𝑏))) |
6 | | isf32lem.d |
. . . . . . . 8
⊢ 𝑆 = {𝑦 ∈ ω ∣ (𝐹‘suc 𝑦) ⊊ (𝐹‘𝑦)} |
7 | 6 | ssrab3 4057 |
. . . . . . 7
⊢ 𝑆 ⊆
ω |
8 | | nnunifi 8763 |
. . . . . . 7
⊢ ((𝑆 ⊆ ω ∧ 𝑆 ∈ Fin) → ∪ 𝑆
∈ ω) |
9 | 7, 8 | mpan 688 |
. . . . . 6
⊢ (𝑆 ∈ Fin → ∪ 𝑆
∈ ω) |
10 | 9 | adantl 484 |
. . . . 5
⊢ ((𝜑 ∧ 𝑆 ∈ Fin) → ∪ 𝑆
∈ ω) |
11 | | elssuni 4861 |
. . . . . . . . . . . . 13
⊢ (𝑏 ∈ 𝑆 → 𝑏 ⊆ ∪ 𝑆) |
12 | | nnon 7580 |
. . . . . . . . . . . . . 14
⊢ (𝑏 ∈ ω → 𝑏 ∈ On) |
13 | | omsson 7578 |
. . . . . . . . . . . . . . 15
⊢ ω
⊆ On |
14 | 13, 10 | sseldi 3965 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑆 ∈ Fin) → ∪ 𝑆
∈ On) |
15 | | ontri1 6220 |
. . . . . . . . . . . . . 14
⊢ ((𝑏 ∈ On ∧ ∪ 𝑆
∈ On) → (𝑏
⊆ ∪ 𝑆 ↔ ¬ ∪
𝑆 ∈ 𝑏)) |
16 | 12, 14, 15 | syl2anr 598 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑆 ∈ Fin) ∧ 𝑏 ∈ ω) → (𝑏 ⊆ ∪ 𝑆 ↔ ¬ ∪ 𝑆
∈ 𝑏)) |
17 | 11, 16 | syl5ib 246 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑆 ∈ Fin) ∧ 𝑏 ∈ ω) → (𝑏 ∈ 𝑆 → ¬ ∪
𝑆 ∈ 𝑏)) |
18 | 17 | con2d 136 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑆 ∈ Fin) ∧ 𝑏 ∈ ω) → (∪ 𝑆
∈ 𝑏 → ¬ 𝑏 ∈ 𝑆)) |
19 | 18 | impr 457 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑆 ∈ Fin) ∧ (𝑏 ∈ ω ∧ ∪ 𝑆
∈ 𝑏)) → ¬
𝑏 ∈ 𝑆) |
20 | 6 | eleq2i 2904 |
. . . . . . . . . 10
⊢ (𝑏 ∈ 𝑆 ↔ 𝑏 ∈ {𝑦 ∈ ω ∣ (𝐹‘suc 𝑦) ⊊ (𝐹‘𝑦)}) |
21 | 19, 20 | sylnib 330 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑆 ∈ Fin) ∧ (𝑏 ∈ ω ∧ ∪ 𝑆
∈ 𝑏)) → ¬
𝑏 ∈ {𝑦 ∈ ω ∣ (𝐹‘suc 𝑦) ⊊ (𝐹‘𝑦)}) |
22 | | suceq 6251 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝑏 → suc 𝑦 = suc 𝑏) |
23 | 22 | fveq2d 6669 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑏 → (𝐹‘suc 𝑦) = (𝐹‘suc 𝑏)) |
24 | | fveq2 6665 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑏 → (𝐹‘𝑦) = (𝐹‘𝑏)) |
25 | 23, 24 | psseq12d 4071 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑏 → ((𝐹‘suc 𝑦) ⊊ (𝐹‘𝑦) ↔ (𝐹‘suc 𝑏) ⊊ (𝐹‘𝑏))) |
26 | 25 | elrab3 3681 |
. . . . . . . . . 10
⊢ (𝑏 ∈ ω → (𝑏 ∈ {𝑦 ∈ ω ∣ (𝐹‘suc 𝑦) ⊊ (𝐹‘𝑦)} ↔ (𝐹‘suc 𝑏) ⊊ (𝐹‘𝑏))) |
27 | 26 | ad2antrl 726 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑆 ∈ Fin) ∧ (𝑏 ∈ ω ∧ ∪ 𝑆
∈ 𝑏)) → (𝑏 ∈ {𝑦 ∈ ω ∣ (𝐹‘suc 𝑦) ⊊ (𝐹‘𝑦)} ↔ (𝐹‘suc 𝑏) ⊊ (𝐹‘𝑏))) |
28 | 21, 27 | mtbid 326 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑆 ∈ Fin) ∧ (𝑏 ∈ ω ∧ ∪ 𝑆
∈ 𝑏)) → ¬
(𝐹‘suc 𝑏) ⊊ (𝐹‘𝑏)) |
29 | 28 | expr 459 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑆 ∈ Fin) ∧ 𝑏 ∈ ω) → (∪ 𝑆
∈ 𝑏 → ¬
(𝐹‘suc 𝑏) ⊊ (𝐹‘𝑏))) |
30 | | imnan 402 |
. . . . . . 7
⊢ ((∪ 𝑆
∈ 𝑏 → ¬
(𝐹‘suc 𝑏) ⊊ (𝐹‘𝑏)) ↔ ¬ (∪
𝑆 ∈ 𝑏 ∧ (𝐹‘suc 𝑏) ⊊ (𝐹‘𝑏))) |
31 | 29, 30 | sylib 220 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑆 ∈ Fin) ∧ 𝑏 ∈ ω) → ¬ (∪ 𝑆
∈ 𝑏 ∧ (𝐹‘suc 𝑏) ⊊ (𝐹‘𝑏))) |
32 | 31 | nrexdv 3270 |
. . . . 5
⊢ ((𝜑 ∧ 𝑆 ∈ Fin) → ¬ ∃𝑏 ∈ ω (∪ 𝑆
∈ 𝑏 ∧ (𝐹‘suc 𝑏) ⊊ (𝐹‘𝑏))) |
33 | | eleq1 2900 |
. . . . . . . . 9
⊢ (𝑎 = ∪
𝑆 → (𝑎 ∈ 𝑏 ↔ ∪ 𝑆 ∈ 𝑏)) |
34 | 33 | anbi1d 631 |
. . . . . . . 8
⊢ (𝑎 = ∪
𝑆 → ((𝑎 ∈ 𝑏 ∧ (𝐹‘suc 𝑏) ⊊ (𝐹‘𝑏)) ↔ (∪ 𝑆 ∈ 𝑏 ∧ (𝐹‘suc 𝑏) ⊊ (𝐹‘𝑏)))) |
35 | 34 | rexbidv 3297 |
. . . . . . 7
⊢ (𝑎 = ∪
𝑆 → (∃𝑏 ∈ ω (𝑎 ∈ 𝑏 ∧ (𝐹‘suc 𝑏) ⊊ (𝐹‘𝑏)) ↔ ∃𝑏 ∈ ω (∪
𝑆 ∈ 𝑏 ∧ (𝐹‘suc 𝑏) ⊊ (𝐹‘𝑏)))) |
36 | 35 | notbid 320 |
. . . . . 6
⊢ (𝑎 = ∪
𝑆 → (¬
∃𝑏 ∈ ω
(𝑎 ∈ 𝑏 ∧ (𝐹‘suc 𝑏) ⊊ (𝐹‘𝑏)) ↔ ¬ ∃𝑏 ∈ ω (∪
𝑆 ∈ 𝑏 ∧ (𝐹‘suc 𝑏) ⊊ (𝐹‘𝑏)))) |
37 | 36 | rspcev 3623 |
. . . . 5
⊢ ((∪ 𝑆
∈ ω ∧ ¬ ∃𝑏 ∈ ω (∪
𝑆 ∈ 𝑏 ∧ (𝐹‘suc 𝑏) ⊊ (𝐹‘𝑏))) → ∃𝑎 ∈ ω ¬ ∃𝑏 ∈ ω (𝑎 ∈ 𝑏 ∧ (𝐹‘suc 𝑏) ⊊ (𝐹‘𝑏))) |
38 | 10, 32, 37 | syl2anc 586 |
. . . 4
⊢ ((𝜑 ∧ 𝑆 ∈ Fin) → ∃𝑎 ∈ ω ¬
∃𝑏 ∈ ω
(𝑎 ∈ 𝑏 ∧ (𝐹‘suc 𝑏) ⊊ (𝐹‘𝑏))) |
39 | | rexnal 3238 |
. . . 4
⊢
(∃𝑎 ∈
ω ¬ ∃𝑏
∈ ω (𝑎 ∈
𝑏 ∧ (𝐹‘suc 𝑏) ⊊ (𝐹‘𝑏)) ↔ ¬ ∀𝑎 ∈ ω ∃𝑏 ∈ ω (𝑎 ∈ 𝑏 ∧ (𝐹‘suc 𝑏) ⊊ (𝐹‘𝑏))) |
40 | 38, 39 | sylib 220 |
. . 3
⊢ ((𝜑 ∧ 𝑆 ∈ Fin) → ¬ ∀𝑎 ∈ ω ∃𝑏 ∈ ω (𝑎 ∈ 𝑏 ∧ (𝐹‘suc 𝑏) ⊊ (𝐹‘𝑏))) |
41 | 40 | ex 415 |
. 2
⊢ (𝜑 → (𝑆 ∈ Fin → ¬ ∀𝑎 ∈ ω ∃𝑏 ∈ ω (𝑎 ∈ 𝑏 ∧ (𝐹‘suc 𝑏) ⊊ (𝐹‘𝑏)))) |
42 | 5, 41 | mt2d 138 |
1
⊢ (𝜑 → ¬ 𝑆 ∈ Fin) |