| Step | Hyp | Ref
| Expression |
| 1 | | isf32lem.g |
. . . 4
⊢ 𝐿 = (𝑡 ∈ 𝐺 ↦ (℩𝑠(𝑠 ∈ ω ∧ 𝑡 ∈ (𝐾‘𝑠)))) |
| 2 | | ssab2 4079 |
. . . . . . 7
⊢ {𝑠 ∣ (𝑠 ∈ ω ∧ 𝑡 ∈ (𝐾‘𝑠))} ⊆ ω |
| 3 | | iotacl 6547 |
. . . . . . 7
⊢
(∃!𝑠(𝑠 ∈ ω ∧ 𝑡 ∈ (𝐾‘𝑠)) → (℩𝑠(𝑠 ∈ ω ∧ 𝑡 ∈ (𝐾‘𝑠))) ∈ {𝑠 ∣ (𝑠 ∈ ω ∧ 𝑡 ∈ (𝐾‘𝑠))}) |
| 4 | 2, 3 | sselid 3981 |
. . . . . 6
⊢
(∃!𝑠(𝑠 ∈ ω ∧ 𝑡 ∈ (𝐾‘𝑠)) → (℩𝑠(𝑠 ∈ ω ∧ 𝑡 ∈ (𝐾‘𝑠))) ∈ ω) |
| 5 | | iotanul 6539 |
. . . . . . 7
⊢ (¬
∃!𝑠(𝑠 ∈ ω ∧ 𝑡 ∈ (𝐾‘𝑠)) → (℩𝑠(𝑠 ∈ ω ∧ 𝑡 ∈ (𝐾‘𝑠))) = ∅) |
| 6 | | peano1 7910 |
. . . . . . 7
⊢ ∅
∈ ω |
| 7 | 5, 6 | eqeltrdi 2849 |
. . . . . 6
⊢ (¬
∃!𝑠(𝑠 ∈ ω ∧ 𝑡 ∈ (𝐾‘𝑠)) → (℩𝑠(𝑠 ∈ ω ∧ 𝑡 ∈ (𝐾‘𝑠))) ∈ ω) |
| 8 | 4, 7 | pm2.61i 182 |
. . . . 5
⊢
(℩𝑠(𝑠 ∈ ω ∧ 𝑡 ∈ (𝐾‘𝑠))) ∈ ω |
| 9 | 8 | a1i 11 |
. . . 4
⊢ (𝑡 ∈ 𝐺 → (℩𝑠(𝑠 ∈ ω ∧ 𝑡 ∈ (𝐾‘𝑠))) ∈ ω) |
| 10 | 1, 9 | fmpti 7132 |
. . 3
⊢ 𝐿:𝐺⟶ω |
| 11 | 10 | a1i 11 |
. 2
⊢ (𝜑 → 𝐿:𝐺⟶ω) |
| 12 | | isf32lem.a |
. . . . . 6
⊢ (𝜑 → 𝐹:ω⟶𝒫 𝐺) |
| 13 | | isf32lem.b |
. . . . . 6
⊢ (𝜑 → ∀𝑥 ∈ ω (𝐹‘suc 𝑥) ⊆ (𝐹‘𝑥)) |
| 14 | | isf32lem.c |
. . . . . 6
⊢ (𝜑 → ¬ ∩ ran 𝐹 ∈ ran 𝐹) |
| 15 | | isf32lem.d |
. . . . . 6
⊢ 𝑆 = {𝑦 ∈ ω ∣ (𝐹‘suc 𝑦) ⊊ (𝐹‘𝑦)} |
| 16 | | isf32lem.e |
. . . . . 6
⊢ 𝐽 = (𝑢 ∈ ω ↦ (℩𝑣 ∈ 𝑆 (𝑣 ∩ 𝑆) ≈ 𝑢)) |
| 17 | | isf32lem.f |
. . . . . 6
⊢ 𝐾 = ((𝑤 ∈ 𝑆 ↦ ((𝐹‘𝑤) ∖ (𝐹‘suc 𝑤))) ∘ 𝐽) |
| 18 | 12, 13, 14, 15, 16, 17 | isf32lem6 10398 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ ω) → (𝐾‘𝑎) ≠ ∅) |
| 19 | | n0 4353 |
. . . . 5
⊢ ((𝐾‘𝑎) ≠ ∅ ↔ ∃𝑏 𝑏 ∈ (𝐾‘𝑎)) |
| 20 | 18, 19 | sylib 218 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ ω) → ∃𝑏 𝑏 ∈ (𝐾‘𝑎)) |
| 21 | 12, 13, 14, 15, 16, 17 | isf32lem8 10400 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ ω) → (𝐾‘𝑎) ⊆ 𝐺) |
| 22 | 21 | sselda 3983 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑎 ∈ ω) ∧ 𝑏 ∈ (𝐾‘𝑎)) → 𝑏 ∈ 𝐺) |
| 23 | | eleq1w 2824 |
. . . . . . . . . . . . 13
⊢ (𝑡 = 𝑏 → (𝑡 ∈ (𝐾‘𝑠) ↔ 𝑏 ∈ (𝐾‘𝑠))) |
| 24 | 23 | anbi2d 630 |
. . . . . . . . . . . 12
⊢ (𝑡 = 𝑏 → ((𝑠 ∈ ω ∧ 𝑡 ∈ (𝐾‘𝑠)) ↔ (𝑠 ∈ ω ∧ 𝑏 ∈ (𝐾‘𝑠)))) |
| 25 | 24 | iotabidv 6545 |
. . . . . . . . . . 11
⊢ (𝑡 = 𝑏 → (℩𝑠(𝑠 ∈ ω ∧ 𝑡 ∈ (𝐾‘𝑠))) = (℩𝑠(𝑠 ∈ ω ∧ 𝑏 ∈ (𝐾‘𝑠)))) |
| 26 | | iotaex 6534 |
. . . . . . . . . . 11
⊢
(℩𝑠(𝑠 ∈ ω ∧ 𝑡 ∈ (𝐾‘𝑠))) ∈ V |
| 27 | 25, 1, 26 | fvmpt3i 7021 |
. . . . . . . . . 10
⊢ (𝑏 ∈ 𝐺 → (𝐿‘𝑏) = (℩𝑠(𝑠 ∈ ω ∧ 𝑏 ∈ (𝐾‘𝑠)))) |
| 28 | 22, 27 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ ω) ∧ 𝑏 ∈ (𝐾‘𝑎)) → (𝐿‘𝑏) = (℩𝑠(𝑠 ∈ ω ∧ 𝑏 ∈ (𝐾‘𝑠)))) |
| 29 | | simp1r 1199 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑏 ∈ (𝐾‘𝑎)) ∧ 𝑎 ∈ ω ∧ 𝑠 ∈ ω) → 𝑏 ∈ (𝐾‘𝑎)) |
| 30 | | simpl1 1192 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑎 ∈ ω ∧ 𝑠 ∈ ω) ∧ 𝑠 ≠ 𝑎) → 𝜑) |
| 31 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑎 ∈ ω ∧ 𝑠 ∈ ω) ∧ 𝑠 ≠ 𝑎) → 𝑠 ≠ 𝑎) |
| 32 | 31 | necomd 2996 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑎 ∈ ω ∧ 𝑠 ∈ ω) ∧ 𝑠 ≠ 𝑎) → 𝑎 ≠ 𝑠) |
| 33 | | simpl2 1193 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑎 ∈ ω ∧ 𝑠 ∈ ω) ∧ 𝑠 ≠ 𝑎) → 𝑎 ∈ ω) |
| 34 | | simpl3 1194 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑎 ∈ ω ∧ 𝑠 ∈ ω) ∧ 𝑠 ≠ 𝑎) → 𝑠 ∈ ω) |
| 35 | 12, 13, 14, 15, 16, 17 | isf32lem7 10399 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑎 ≠ 𝑠) ∧ (𝑎 ∈ ω ∧ 𝑠 ∈ ω)) → ((𝐾‘𝑎) ∩ (𝐾‘𝑠)) = ∅) |
| 36 | 30, 32, 33, 34, 35 | syl22anc 839 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑎 ∈ ω ∧ 𝑠 ∈ ω) ∧ 𝑠 ≠ 𝑎) → ((𝐾‘𝑎) ∩ (𝐾‘𝑠)) = ∅) |
| 37 | | disj1 4452 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐾‘𝑎) ∩ (𝐾‘𝑠)) = ∅ ↔ ∀𝑏(𝑏 ∈ (𝐾‘𝑎) → ¬ 𝑏 ∈ (𝐾‘𝑠))) |
| 38 | 36, 37 | sylib 218 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑎 ∈ ω ∧ 𝑠 ∈ ω) ∧ 𝑠 ≠ 𝑎) → ∀𝑏(𝑏 ∈ (𝐾‘𝑎) → ¬ 𝑏 ∈ (𝐾‘𝑠))) |
| 39 | 38 | ex 412 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑎 ∈ ω ∧ 𝑠 ∈ ω) → (𝑠 ≠ 𝑎 → ∀𝑏(𝑏 ∈ (𝐾‘𝑎) → ¬ 𝑏 ∈ (𝐾‘𝑠)))) |
| 40 | | sp 2183 |
. . . . . . . . . . . . . . . . . . 19
⊢
(∀𝑏(𝑏 ∈ (𝐾‘𝑎) → ¬ 𝑏 ∈ (𝐾‘𝑠)) → (𝑏 ∈ (𝐾‘𝑎) → ¬ 𝑏 ∈ (𝐾‘𝑠))) |
| 41 | 39, 40 | syl6 35 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑎 ∈ ω ∧ 𝑠 ∈ ω) → (𝑠 ≠ 𝑎 → (𝑏 ∈ (𝐾‘𝑎) → ¬ 𝑏 ∈ (𝐾‘𝑠)))) |
| 42 | 41 | com23 86 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑎 ∈ ω ∧ 𝑠 ∈ ω) → (𝑏 ∈ (𝐾‘𝑎) → (𝑠 ≠ 𝑎 → ¬ 𝑏 ∈ (𝐾‘𝑠)))) |
| 43 | 42 | 3adant1r 1178 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑏 ∈ (𝐾‘𝑎)) ∧ 𝑎 ∈ ω ∧ 𝑠 ∈ ω) → (𝑏 ∈ (𝐾‘𝑎) → (𝑠 ≠ 𝑎 → ¬ 𝑏 ∈ (𝐾‘𝑠)))) |
| 44 | 29, 43 | mpd 15 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑏 ∈ (𝐾‘𝑎)) ∧ 𝑎 ∈ ω ∧ 𝑠 ∈ ω) → (𝑠 ≠ 𝑎 → ¬ 𝑏 ∈ (𝐾‘𝑠))) |
| 45 | 44 | necon4ad 2959 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑏 ∈ (𝐾‘𝑎)) ∧ 𝑎 ∈ ω ∧ 𝑠 ∈ ω) → (𝑏 ∈ (𝐾‘𝑠) → 𝑠 = 𝑎)) |
| 46 | 45 | 3expia 1122 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑏 ∈ (𝐾‘𝑎)) ∧ 𝑎 ∈ ω) → (𝑠 ∈ ω → (𝑏 ∈ (𝐾‘𝑠) → 𝑠 = 𝑎))) |
| 47 | 46 | impd 410 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑏 ∈ (𝐾‘𝑎)) ∧ 𝑎 ∈ ω) → ((𝑠 ∈ ω ∧ 𝑏 ∈ (𝐾‘𝑠)) → 𝑠 = 𝑎)) |
| 48 | | eleq1w 2824 |
. . . . . . . . . . . . . . . 16
⊢ (𝑠 = 𝑎 → (𝑠 ∈ ω ↔ 𝑎 ∈ ω)) |
| 49 | | fveq2 6906 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑠 = 𝑎 → (𝐾‘𝑠) = (𝐾‘𝑎)) |
| 50 | 49 | eleq2d 2827 |
. . . . . . . . . . . . . . . 16
⊢ (𝑠 = 𝑎 → (𝑏 ∈ (𝐾‘𝑠) ↔ 𝑏 ∈ (𝐾‘𝑎))) |
| 51 | 48, 50 | anbi12d 632 |
. . . . . . . . . . . . . . 15
⊢ (𝑠 = 𝑎 → ((𝑠 ∈ ω ∧ 𝑏 ∈ (𝐾‘𝑠)) ↔ (𝑎 ∈ ω ∧ 𝑏 ∈ (𝐾‘𝑎)))) |
| 52 | 51 | biimprcd 250 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 ∈ ω ∧ 𝑏 ∈ (𝐾‘𝑎)) → (𝑠 = 𝑎 → (𝑠 ∈ ω ∧ 𝑏 ∈ (𝐾‘𝑠)))) |
| 53 | 52 | ancoms 458 |
. . . . . . . . . . . . 13
⊢ ((𝑏 ∈ (𝐾‘𝑎) ∧ 𝑎 ∈ ω) → (𝑠 = 𝑎 → (𝑠 ∈ ω ∧ 𝑏 ∈ (𝐾‘𝑠)))) |
| 54 | 53 | adantll 714 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑏 ∈ (𝐾‘𝑎)) ∧ 𝑎 ∈ ω) → (𝑠 = 𝑎 → (𝑠 ∈ ω ∧ 𝑏 ∈ (𝐾‘𝑠)))) |
| 55 | 47, 54 | impbid 212 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑏 ∈ (𝐾‘𝑎)) ∧ 𝑎 ∈ ω) → ((𝑠 ∈ ω ∧ 𝑏 ∈ (𝐾‘𝑠)) ↔ 𝑠 = 𝑎)) |
| 56 | 55 | iota5 6544 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑏 ∈ (𝐾‘𝑎)) ∧ 𝑎 ∈ ω) → (℩𝑠(𝑠 ∈ ω ∧ 𝑏 ∈ (𝐾‘𝑠))) = 𝑎) |
| 57 | 56 | an32s 652 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ ω) ∧ 𝑏 ∈ (𝐾‘𝑎)) → (℩𝑠(𝑠 ∈ ω ∧ 𝑏 ∈ (𝐾‘𝑠))) = 𝑎) |
| 58 | 28, 57 | eqtr2d 2778 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑎 ∈ ω) ∧ 𝑏 ∈ (𝐾‘𝑎)) → 𝑎 = (𝐿‘𝑏)) |
| 59 | 22, 58 | jca 511 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ ω) ∧ 𝑏 ∈ (𝐾‘𝑎)) → (𝑏 ∈ 𝐺 ∧ 𝑎 = (𝐿‘𝑏))) |
| 60 | 59 | ex 412 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ ω) → (𝑏 ∈ (𝐾‘𝑎) → (𝑏 ∈ 𝐺 ∧ 𝑎 = (𝐿‘𝑏)))) |
| 61 | 60 | eximdv 1917 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ ω) → (∃𝑏 𝑏 ∈ (𝐾‘𝑎) → ∃𝑏(𝑏 ∈ 𝐺 ∧ 𝑎 = (𝐿‘𝑏)))) |
| 62 | | df-rex 3071 |
. . . . 5
⊢
(∃𝑏 ∈
𝐺 𝑎 = (𝐿‘𝑏) ↔ ∃𝑏(𝑏 ∈ 𝐺 ∧ 𝑎 = (𝐿‘𝑏))) |
| 63 | 61, 62 | imbitrrdi 252 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ ω) → (∃𝑏 𝑏 ∈ (𝐾‘𝑎) → ∃𝑏 ∈ 𝐺 𝑎 = (𝐿‘𝑏))) |
| 64 | 20, 63 | mpd 15 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ ω) → ∃𝑏 ∈ 𝐺 𝑎 = (𝐿‘𝑏)) |
| 65 | 64 | ralrimiva 3146 |
. 2
⊢ (𝜑 → ∀𝑎 ∈ ω ∃𝑏 ∈ 𝐺 𝑎 = (𝐿‘𝑏)) |
| 66 | | dffo3 7122 |
. 2
⊢ (𝐿:𝐺–onto→ω ↔ (𝐿:𝐺⟶ω ∧ ∀𝑎 ∈ ω ∃𝑏 ∈ 𝐺 𝑎 = (𝐿‘𝑏))) |
| 67 | 11, 65, 66 | sylanbrc 583 |
1
⊢ (𝜑 → 𝐿:𝐺–onto→ω) |