Step | Hyp | Ref
| Expression |
1 | | isf32lem.g |
. . . 4
⊢ 𝐿 = (𝑡 ∈ 𝐺 ↦ (℩𝑠(𝑠 ∈ ω ∧ 𝑡 ∈ (𝐾‘𝑠)))) |
2 | | ssab2 3969 |
. . . . . . 7
⊢ {𝑠 ∣ (𝑠 ∈ ω ∧ 𝑡 ∈ (𝐾‘𝑠))} ⊆ ω |
3 | | iotacl 6326 |
. . . . . . 7
⊢
(∃!𝑠(𝑠 ∈ ω ∧ 𝑡 ∈ (𝐾‘𝑠)) → (℩𝑠(𝑠 ∈ ω ∧ 𝑡 ∈ (𝐾‘𝑠))) ∈ {𝑠 ∣ (𝑠 ∈ ω ∧ 𝑡 ∈ (𝐾‘𝑠))}) |
4 | 2, 3 | sseldi 3876 |
. . . . . 6
⊢
(∃!𝑠(𝑠 ∈ ω ∧ 𝑡 ∈ (𝐾‘𝑠)) → (℩𝑠(𝑠 ∈ ω ∧ 𝑡 ∈ (𝐾‘𝑠))) ∈ ω) |
5 | | iotanul 6318 |
. . . . . . 7
⊢ (¬
∃!𝑠(𝑠 ∈ ω ∧ 𝑡 ∈ (𝐾‘𝑠)) → (℩𝑠(𝑠 ∈ ω ∧ 𝑡 ∈ (𝐾‘𝑠))) = ∅) |
6 | | peano1 7623 |
. . . . . . 7
⊢ ∅
∈ ω |
7 | 5, 6 | eqeltrdi 2842 |
. . . . . 6
⊢ (¬
∃!𝑠(𝑠 ∈ ω ∧ 𝑡 ∈ (𝐾‘𝑠)) → (℩𝑠(𝑠 ∈ ω ∧ 𝑡 ∈ (𝐾‘𝑠))) ∈ ω) |
8 | 4, 7 | pm2.61i 185 |
. . . . 5
⊢
(℩𝑠(𝑠 ∈ ω ∧ 𝑡 ∈ (𝐾‘𝑠))) ∈ ω |
9 | 8 | a1i 11 |
. . . 4
⊢ (𝑡 ∈ 𝐺 → (℩𝑠(𝑠 ∈ ω ∧ 𝑡 ∈ (𝐾‘𝑠))) ∈ ω) |
10 | 1, 9 | fmpti 6889 |
. . 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 9861 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ ω) → (𝐾‘𝑎) ≠ ∅) |
19 | | n0 4236 |
. . . . 5
⊢ ((𝐾‘𝑎) ≠ ∅ ↔ ∃𝑏 𝑏 ∈ (𝐾‘𝑎)) |
20 | 18, 19 | sylib 221 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ ω) → ∃𝑏 𝑏 ∈ (𝐾‘𝑎)) |
21 | 12, 13, 14, 15, 16, 17 | isf32lem8 9863 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ ω) → (𝐾‘𝑎) ⊆ 𝐺) |
22 | 21 | sselda 3878 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑎 ∈ ω) ∧ 𝑏 ∈ (𝐾‘𝑎)) → 𝑏 ∈ 𝐺) |
23 | | eleq1w 2816 |
. . . . . . . . . . . . 13
⊢ (𝑡 = 𝑏 → (𝑡 ∈ (𝐾‘𝑠) ↔ 𝑏 ∈ (𝐾‘𝑠))) |
24 | 23 | anbi2d 632 |
. . . . . . . . . . . 12
⊢ (𝑡 = 𝑏 → ((𝑠 ∈ ω ∧ 𝑡 ∈ (𝐾‘𝑠)) ↔ (𝑠 ∈ ω ∧ 𝑏 ∈ (𝐾‘𝑠)))) |
25 | 24 | iotabidv 6324 |
. . . . . . . . . . 11
⊢ (𝑡 = 𝑏 → (℩𝑠(𝑠 ∈ ω ∧ 𝑡 ∈ (𝐾‘𝑠))) = (℩𝑠(𝑠 ∈ ω ∧ 𝑏 ∈ (𝐾‘𝑠)))) |
26 | | iotaex 6320 |
. . . . . . . . . . 11
⊢
(℩𝑠(𝑠 ∈ ω ∧ 𝑡 ∈ (𝐾‘𝑠))) ∈ V |
27 | 25, 1, 26 | fvmpt3i 6783 |
. . . . . . . . . 10
⊢ (𝑏 ∈ 𝐺 → (𝐿‘𝑏) = (℩𝑠(𝑠 ∈ ω ∧ 𝑏 ∈ (𝐾‘𝑠)))) |
28 | 22, 27 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ ω) ∧ 𝑏 ∈ (𝐾‘𝑎)) → (𝐿‘𝑏) = (℩𝑠(𝑠 ∈ ω ∧ 𝑏 ∈ (𝐾‘𝑠)))) |
29 | | simp1r 1199 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑏 ∈ (𝐾‘𝑎)) ∧ 𝑎 ∈ ω ∧ 𝑠 ∈ ω) → 𝑏 ∈ (𝐾‘𝑎)) |
30 | | simpl1 1192 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑎 ∈ ω ∧ 𝑠 ∈ ω) ∧ 𝑠 ≠ 𝑎) → 𝜑) |
31 | | simpr 488 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑎 ∈ ω ∧ 𝑠 ∈ ω) ∧ 𝑠 ≠ 𝑎) → 𝑠 ≠ 𝑎) |
32 | 31 | necomd 2990 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑎 ∈ ω ∧ 𝑠 ∈ ω) ∧ 𝑠 ≠ 𝑎) → 𝑎 ≠ 𝑠) |
33 | | simpl2 1193 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑎 ∈ ω ∧ 𝑠 ∈ ω) ∧ 𝑠 ≠ 𝑎) → 𝑎 ∈ ω) |
34 | | simpl3 1194 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑎 ∈ ω ∧ 𝑠 ∈ ω) ∧ 𝑠 ≠ 𝑎) → 𝑠 ∈ ω) |
35 | 12, 13, 14, 15, 16, 17 | isf32lem7 9862 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑎 ≠ 𝑠) ∧ (𝑎 ∈ ω ∧ 𝑠 ∈ ω)) → ((𝐾‘𝑎) ∩ (𝐾‘𝑠)) = ∅) |
36 | 30, 32, 33, 34, 35 | syl22anc 838 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑎 ∈ ω ∧ 𝑠 ∈ ω) ∧ 𝑠 ≠ 𝑎) → ((𝐾‘𝑎) ∩ (𝐾‘𝑠)) = ∅) |
37 | | disj1 4341 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐾‘𝑎) ∩ (𝐾‘𝑠)) = ∅ ↔ ∀𝑏(𝑏 ∈ (𝐾‘𝑎) → ¬ 𝑏 ∈ (𝐾‘𝑠))) |
38 | 36, 37 | sylib 221 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑎 ∈ ω ∧ 𝑠 ∈ ω) ∧ 𝑠 ≠ 𝑎) → ∀𝑏(𝑏 ∈ (𝐾‘𝑎) → ¬ 𝑏 ∈ (𝐾‘𝑠))) |
39 | 38 | ex 416 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑎 ∈ ω ∧ 𝑠 ∈ ω) → (𝑠 ≠ 𝑎 → ∀𝑏(𝑏 ∈ (𝐾‘𝑎) → ¬ 𝑏 ∈ (𝐾‘𝑠)))) |
40 | | sp 2184 |
. . . . . . . . . . . . . . . . . . 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 2954 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑏 ∈ (𝐾‘𝑎)) ∧ 𝑎 ∈ ω ∧ 𝑠 ∈ ω) → (𝑏 ∈ (𝐾‘𝑠) → 𝑠 = 𝑎)) |
46 | 45 | 3expia 1122 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑏 ∈ (𝐾‘𝑎)) ∧ 𝑎 ∈ ω) → (𝑠 ∈ ω → (𝑏 ∈ (𝐾‘𝑠) → 𝑠 = 𝑎))) |
47 | 46 | impd 414 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑏 ∈ (𝐾‘𝑎)) ∧ 𝑎 ∈ ω) → ((𝑠 ∈ ω ∧ 𝑏 ∈ (𝐾‘𝑠)) → 𝑠 = 𝑎)) |
48 | | eleq1w 2816 |
. . . . . . . . . . . . . . . 16
⊢ (𝑠 = 𝑎 → (𝑠 ∈ ω ↔ 𝑎 ∈ ω)) |
49 | | fveq2 6677 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑠 = 𝑎 → (𝐾‘𝑠) = (𝐾‘𝑎)) |
50 | 49 | eleq2d 2819 |
. . . . . . . . . . . . . . . 16
⊢ (𝑠 = 𝑎 → (𝑏 ∈ (𝐾‘𝑠) ↔ 𝑏 ∈ (𝐾‘𝑎))) |
51 | 48, 50 | anbi12d 634 |
. . . . . . . . . . . . . . 15
⊢ (𝑠 = 𝑎 → ((𝑠 ∈ ω ∧ 𝑏 ∈ (𝐾‘𝑠)) ↔ (𝑎 ∈ ω ∧ 𝑏 ∈ (𝐾‘𝑎)))) |
52 | 51 | biimprcd 253 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 ∈ ω ∧ 𝑏 ∈ (𝐾‘𝑎)) → (𝑠 = 𝑎 → (𝑠 ∈ ω ∧ 𝑏 ∈ (𝐾‘𝑠)))) |
53 | 52 | ancoms 462 |
. . . . . . . . . . . . 13
⊢ ((𝑏 ∈ (𝐾‘𝑎) ∧ 𝑎 ∈ ω) → (𝑠 = 𝑎 → (𝑠 ∈ ω ∧ 𝑏 ∈ (𝐾‘𝑠)))) |
54 | 53 | adantll 714 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑏 ∈ (𝐾‘𝑎)) ∧ 𝑎 ∈ ω) → (𝑠 = 𝑎 → (𝑠 ∈ ω ∧ 𝑏 ∈ (𝐾‘𝑠)))) |
55 | 47, 54 | impbid 215 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑏 ∈ (𝐾‘𝑎)) ∧ 𝑎 ∈ ω) → ((𝑠 ∈ ω ∧ 𝑏 ∈ (𝐾‘𝑠)) ↔ 𝑠 = 𝑎)) |
56 | 55 | iota5 6323 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑏 ∈ (𝐾‘𝑎)) ∧ 𝑎 ∈ ω) → (℩𝑠(𝑠 ∈ ω ∧ 𝑏 ∈ (𝐾‘𝑠))) = 𝑎) |
57 | 56 | an32s 652 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ ω) ∧ 𝑏 ∈ (𝐾‘𝑎)) → (℩𝑠(𝑠 ∈ ω ∧ 𝑏 ∈ (𝐾‘𝑠))) = 𝑎) |
58 | 28, 57 | eqtr2d 2775 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑎 ∈ ω) ∧ 𝑏 ∈ (𝐾‘𝑎)) → 𝑎 = (𝐿‘𝑏)) |
59 | 22, 58 | jca 515 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ ω) ∧ 𝑏 ∈ (𝐾‘𝑎)) → (𝑏 ∈ 𝐺 ∧ 𝑎 = (𝐿‘𝑏))) |
60 | 59 | ex 416 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ ω) → (𝑏 ∈ (𝐾‘𝑎) → (𝑏 ∈ 𝐺 ∧ 𝑎 = (𝐿‘𝑏)))) |
61 | 60 | eximdv 1924 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ ω) → (∃𝑏 𝑏 ∈ (𝐾‘𝑎) → ∃𝑏(𝑏 ∈ 𝐺 ∧ 𝑎 = (𝐿‘𝑏)))) |
62 | | df-rex 3060 |
. . . . 5
⊢
(∃𝑏 ∈
𝐺 𝑎 = (𝐿‘𝑏) ↔ ∃𝑏(𝑏 ∈ 𝐺 ∧ 𝑎 = (𝐿‘𝑏))) |
63 | 61, 62 | syl6ibr 255 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ ω) → (∃𝑏 𝑏 ∈ (𝐾‘𝑎) → ∃𝑏 ∈ 𝐺 𝑎 = (𝐿‘𝑏))) |
64 | 20, 63 | mpd 15 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ ω) → ∃𝑏 ∈ 𝐺 𝑎 = (𝐿‘𝑏)) |
65 | 64 | ralrimiva 3097 |
. 2
⊢ (𝜑 → ∀𝑎 ∈ ω ∃𝑏 ∈ 𝐺 𝑎 = (𝐿‘𝑏)) |
66 | | dffo3 6881 |
. 2
⊢ (𝐿:𝐺–onto→ω ↔ (𝐿:𝐺⟶ω ∧ ∀𝑎 ∈ ω ∃𝑏 ∈ 𝐺 𝑎 = (𝐿‘𝑏))) |
67 | 11, 65, 66 | sylanbrc 586 |
1
⊢ (𝜑 → 𝐿:𝐺–onto→ω) |