| Step | Hyp | Ref
| Expression |
| 1 | | isf32lem.a |
. . . 4
⊢ (𝜑 → 𝐹:ω⟶𝒫 𝐺) |
| 2 | | isf32lem.b |
. . . 4
⊢ (𝜑 → ∀𝑥 ∈ ω (𝐹‘suc 𝑥) ⊆ (𝐹‘𝑥)) |
| 3 | | isf32lem.c |
. . . 4
⊢ (𝜑 → ¬ ∩ ran 𝐹 ∈ ran 𝐹) |
| 4 | 1, 2, 3 | isf32lem2 10394 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ ω) → ∃𝑏 ∈ ω (𝑎 ∈ 𝑏 ∧ (𝐹‘suc 𝑏) ⊊ (𝐹‘𝑏))) |
| 5 | 4 | ralrimiva 3146 |
. 2
⊢ (𝜑 → ∀𝑎 ∈ ω ∃𝑏 ∈ ω (𝑎 ∈ 𝑏 ∧ (𝐹‘suc 𝑏) ⊊ (𝐹‘𝑏))) |
| 6 | | isf32lem.d |
. . . . . . . 8
⊢ 𝑆 = {𝑦 ∈ ω ∣ (𝐹‘suc 𝑦) ⊊ (𝐹‘𝑦)} |
| 7 | 6 | ssrab3 4082 |
. . . . . . 7
⊢ 𝑆 ⊆
ω |
| 8 | | nnunifi 9327 |
. . . . . . 7
⊢ ((𝑆 ⊆ ω ∧ 𝑆 ∈ Fin) → ∪ 𝑆
∈ ω) |
| 9 | 7, 8 | mpan 690 |
. . . . . 6
⊢ (𝑆 ∈ Fin → ∪ 𝑆
∈ ω) |
| 10 | 9 | adantl 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑆 ∈ Fin) → ∪ 𝑆
∈ ω) |
| 11 | | elssuni 4937 |
. . . . . . . . . . . . 13
⊢ (𝑏 ∈ 𝑆 → 𝑏 ⊆ ∪ 𝑆) |
| 12 | | nnon 7893 |
. . . . . . . . . . . . . 14
⊢ (𝑏 ∈ ω → 𝑏 ∈ On) |
| 13 | | omsson 7891 |
. . . . . . . . . . . . . . 15
⊢ ω
⊆ On |
| 14 | 13, 10 | sselid 3981 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑆 ∈ Fin) → ∪ 𝑆
∈ On) |
| 15 | | ontri1 6418 |
. . . . . . . . . . . . . 14
⊢ ((𝑏 ∈ On ∧ ∪ 𝑆
∈ On) → (𝑏
⊆ ∪ 𝑆 ↔ ¬ ∪
𝑆 ∈ 𝑏)) |
| 16 | 12, 14, 15 | syl2anr 597 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑆 ∈ Fin) ∧ 𝑏 ∈ ω) → (𝑏 ⊆ ∪ 𝑆 ↔ ¬ ∪ 𝑆
∈ 𝑏)) |
| 17 | 11, 16 | imbitrid 244 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑆 ∈ Fin) ∧ 𝑏 ∈ ω) → (𝑏 ∈ 𝑆 → ¬ ∪
𝑆 ∈ 𝑏)) |
| 18 | 17 | con2d 134 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑆 ∈ Fin) ∧ 𝑏 ∈ ω) → (∪ 𝑆
∈ 𝑏 → ¬ 𝑏 ∈ 𝑆)) |
| 19 | 18 | impr 454 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑆 ∈ Fin) ∧ (𝑏 ∈ ω ∧ ∪ 𝑆
∈ 𝑏)) → ¬
𝑏 ∈ 𝑆) |
| 20 | 6 | eleq2i 2833 |
. . . . . . . . . 10
⊢ (𝑏 ∈ 𝑆 ↔ 𝑏 ∈ {𝑦 ∈ ω ∣ (𝐹‘suc 𝑦) ⊊ (𝐹‘𝑦)}) |
| 21 | 19, 20 | sylnib 328 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑆 ∈ Fin) ∧ (𝑏 ∈ ω ∧ ∪ 𝑆
∈ 𝑏)) → ¬
𝑏 ∈ {𝑦 ∈ ω ∣ (𝐹‘suc 𝑦) ⊊ (𝐹‘𝑦)}) |
| 22 | | suceq 6450 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝑏 → suc 𝑦 = suc 𝑏) |
| 23 | 22 | fveq2d 6910 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑏 → (𝐹‘suc 𝑦) = (𝐹‘suc 𝑏)) |
| 24 | | fveq2 6906 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑏 → (𝐹‘𝑦) = (𝐹‘𝑏)) |
| 25 | 23, 24 | psseq12d 4097 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑏 → ((𝐹‘suc 𝑦) ⊊ (𝐹‘𝑦) ↔ (𝐹‘suc 𝑏) ⊊ (𝐹‘𝑏))) |
| 26 | 25 | elrab3 3693 |
. . . . . . . . . 10
⊢ (𝑏 ∈ ω → (𝑏 ∈ {𝑦 ∈ ω ∣ (𝐹‘suc 𝑦) ⊊ (𝐹‘𝑦)} ↔ (𝐹‘suc 𝑏) ⊊ (𝐹‘𝑏))) |
| 27 | 26 | ad2antrl 728 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑆 ∈ Fin) ∧ (𝑏 ∈ ω ∧ ∪ 𝑆
∈ 𝑏)) → (𝑏 ∈ {𝑦 ∈ ω ∣ (𝐹‘suc 𝑦) ⊊ (𝐹‘𝑦)} ↔ (𝐹‘suc 𝑏) ⊊ (𝐹‘𝑏))) |
| 28 | 21, 27 | mtbid 324 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑆 ∈ Fin) ∧ (𝑏 ∈ ω ∧ ∪ 𝑆
∈ 𝑏)) → ¬
(𝐹‘suc 𝑏) ⊊ (𝐹‘𝑏)) |
| 29 | 28 | expr 456 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑆 ∈ Fin) ∧ 𝑏 ∈ ω) → (∪ 𝑆
∈ 𝑏 → ¬
(𝐹‘suc 𝑏) ⊊ (𝐹‘𝑏))) |
| 30 | | imnan 399 |
. . . . . . 7
⊢ ((∪ 𝑆
∈ 𝑏 → ¬
(𝐹‘suc 𝑏) ⊊ (𝐹‘𝑏)) ↔ ¬ (∪
𝑆 ∈ 𝑏 ∧ (𝐹‘suc 𝑏) ⊊ (𝐹‘𝑏))) |
| 31 | 29, 30 | sylib 218 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑆 ∈ Fin) ∧ 𝑏 ∈ ω) → ¬ (∪ 𝑆
∈ 𝑏 ∧ (𝐹‘suc 𝑏) ⊊ (𝐹‘𝑏))) |
| 32 | 31 | nrexdv 3149 |
. . . . 5
⊢ ((𝜑 ∧ 𝑆 ∈ Fin) → ¬ ∃𝑏 ∈ ω (∪ 𝑆
∈ 𝑏 ∧ (𝐹‘suc 𝑏) ⊊ (𝐹‘𝑏))) |
| 33 | | eleq1 2829 |
. . . . . . . . 9
⊢ (𝑎 = ∪
𝑆 → (𝑎 ∈ 𝑏 ↔ ∪ 𝑆 ∈ 𝑏)) |
| 34 | 33 | anbi1d 631 |
. . . . . . . 8
⊢ (𝑎 = ∪
𝑆 → ((𝑎 ∈ 𝑏 ∧ (𝐹‘suc 𝑏) ⊊ (𝐹‘𝑏)) ↔ (∪ 𝑆 ∈ 𝑏 ∧ (𝐹‘suc 𝑏) ⊊ (𝐹‘𝑏)))) |
| 35 | 34 | rexbidv 3179 |
. . . . . . 7
⊢ (𝑎 = ∪
𝑆 → (∃𝑏 ∈ ω (𝑎 ∈ 𝑏 ∧ (𝐹‘suc 𝑏) ⊊ (𝐹‘𝑏)) ↔ ∃𝑏 ∈ ω (∪
𝑆 ∈ 𝑏 ∧ (𝐹‘suc 𝑏) ⊊ (𝐹‘𝑏)))) |
| 36 | 35 | notbid 318 |
. . . . . 6
⊢ (𝑎 = ∪
𝑆 → (¬
∃𝑏 ∈ ω
(𝑎 ∈ 𝑏 ∧ (𝐹‘suc 𝑏) ⊊ (𝐹‘𝑏)) ↔ ¬ ∃𝑏 ∈ ω (∪
𝑆 ∈ 𝑏 ∧ (𝐹‘suc 𝑏) ⊊ (𝐹‘𝑏)))) |
| 37 | 36 | rspcev 3622 |
. . . . 5
⊢ ((∪ 𝑆
∈ ω ∧ ¬ ∃𝑏 ∈ ω (∪
𝑆 ∈ 𝑏 ∧ (𝐹‘suc 𝑏) ⊊ (𝐹‘𝑏))) → ∃𝑎 ∈ ω ¬ ∃𝑏 ∈ ω (𝑎 ∈ 𝑏 ∧ (𝐹‘suc 𝑏) ⊊ (𝐹‘𝑏))) |
| 38 | 10, 32, 37 | syl2anc 584 |
. . . 4
⊢ ((𝜑 ∧ 𝑆 ∈ Fin) → ∃𝑎 ∈ ω ¬
∃𝑏 ∈ ω
(𝑎 ∈ 𝑏 ∧ (𝐹‘suc 𝑏) ⊊ (𝐹‘𝑏))) |
| 39 | | rexnal 3100 |
. . . 4
⊢
(∃𝑎 ∈
ω ¬ ∃𝑏
∈ ω (𝑎 ∈
𝑏 ∧ (𝐹‘suc 𝑏) ⊊ (𝐹‘𝑏)) ↔ ¬ ∀𝑎 ∈ ω ∃𝑏 ∈ ω (𝑎 ∈ 𝑏 ∧ (𝐹‘suc 𝑏) ⊊ (𝐹‘𝑏))) |
| 40 | 38, 39 | sylib 218 |
. . 3
⊢ ((𝜑 ∧ 𝑆 ∈ Fin) → ¬ ∀𝑎 ∈ ω ∃𝑏 ∈ ω (𝑎 ∈ 𝑏 ∧ (𝐹‘suc 𝑏) ⊊ (𝐹‘𝑏))) |
| 41 | 40 | ex 412 |
. 2
⊢ (𝜑 → (𝑆 ∈ Fin → ¬ ∀𝑎 ∈ ω ∃𝑏 ∈ ω (𝑎 ∈ 𝑏 ∧ (𝐹‘suc 𝑏) ⊊ (𝐹‘𝑏)))) |
| 42 | 5, 41 | mt2d 136 |
1
⊢ (𝜑 → ¬ 𝑆 ∈ Fin) |