Step | Hyp | Ref
| Expression |
1 | | isf32lem.g |
. . . 4
⊢ 𝐿 = (𝑡 ∈ 𝐺 ↦ (℩𝑠(𝑠 ∈ ω ∧ 𝑡 ∈ (𝐾‘𝑠)))) |
2 | | ssab2 4012 |
. . . . . . 7
⊢ {𝑠 ∣ (𝑠 ∈ ω ∧ 𝑡 ∈ (𝐾‘𝑠))} ⊆ ω |
3 | | iotacl 6419 |
. . . . . . 7
⊢
(∃!𝑠(𝑠 ∈ ω ∧ 𝑡 ∈ (𝐾‘𝑠)) → (℩𝑠(𝑠 ∈ ω ∧ 𝑡 ∈ (𝐾‘𝑠))) ∈ {𝑠 ∣ (𝑠 ∈ ω ∧ 𝑡 ∈ (𝐾‘𝑠))}) |
4 | 2, 3 | sselid 3919 |
. . . . . 6
⊢
(∃!𝑠(𝑠 ∈ ω ∧ 𝑡 ∈ (𝐾‘𝑠)) → (℩𝑠(𝑠 ∈ ω ∧ 𝑡 ∈ (𝐾‘𝑠))) ∈ ω) |
5 | | iotanul 6411 |
. . . . . . 7
⊢ (¬
∃!𝑠(𝑠 ∈ ω ∧ 𝑡 ∈ (𝐾‘𝑠)) → (℩𝑠(𝑠 ∈ ω ∧ 𝑡 ∈ (𝐾‘𝑠))) = ∅) |
6 | | peano1 7735 |
. . . . . . 7
⊢ ∅
∈ ω |
7 | 5, 6 | eqeltrdi 2847 |
. . . . . 6
⊢ (¬
∃!𝑠(𝑠 ∈ ω ∧ 𝑡 ∈ (𝐾‘𝑠)) → (℩𝑠(𝑠 ∈ ω ∧ 𝑡 ∈ (𝐾‘𝑠))) ∈ ω) |
8 | 4, 7 | pm2.61i 182 |
. . . . 5
⊢
(℩𝑠(𝑠 ∈ ω ∧ 𝑡 ∈ (𝐾‘𝑠))) ∈ ω |
9 | 8 | a1i 11 |
. . . 4
⊢ (𝑡 ∈ 𝐺 → (℩𝑠(𝑠 ∈ ω ∧ 𝑡 ∈ (𝐾‘𝑠))) ∈ ω) |
10 | 1, 9 | fmpti 6986 |
. . 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 10114 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ ω) → (𝐾‘𝑎) ≠ ∅) |
19 | | n0 4280 |
. . . . 5
⊢ ((𝐾‘𝑎) ≠ ∅ ↔ ∃𝑏 𝑏 ∈ (𝐾‘𝑎)) |
20 | 18, 19 | sylib 217 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ ω) → ∃𝑏 𝑏 ∈ (𝐾‘𝑎)) |
21 | 12, 13, 14, 15, 16, 17 | isf32lem8 10116 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ ω) → (𝐾‘𝑎) ⊆ 𝐺) |
22 | 21 | sselda 3921 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑎 ∈ ω) ∧ 𝑏 ∈ (𝐾‘𝑎)) → 𝑏 ∈ 𝐺) |
23 | | eleq1w 2821 |
. . . . . . . . . . . . 13
⊢ (𝑡 = 𝑏 → (𝑡 ∈ (𝐾‘𝑠) ↔ 𝑏 ∈ (𝐾‘𝑠))) |
24 | 23 | anbi2d 629 |
. . . . . . . . . . . 12
⊢ (𝑡 = 𝑏 → ((𝑠 ∈ ω ∧ 𝑡 ∈ (𝐾‘𝑠)) ↔ (𝑠 ∈ ω ∧ 𝑏 ∈ (𝐾‘𝑠)))) |
25 | 24 | iotabidv 6417 |
. . . . . . . . . . 11
⊢ (𝑡 = 𝑏 → (℩𝑠(𝑠 ∈ ω ∧ 𝑡 ∈ (𝐾‘𝑠))) = (℩𝑠(𝑠 ∈ ω ∧ 𝑏 ∈ (𝐾‘𝑠)))) |
26 | | iotaex 6413 |
. . . . . . . . . . 11
⊢
(℩𝑠(𝑠 ∈ ω ∧ 𝑡 ∈ (𝐾‘𝑠))) ∈ V |
27 | 25, 1, 26 | fvmpt3i 6880 |
. . . . . . . . . 10
⊢ (𝑏 ∈ 𝐺 → (𝐿‘𝑏) = (℩𝑠(𝑠 ∈ ω ∧ 𝑏 ∈ (𝐾‘𝑠)))) |
28 | 22, 27 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ ω) ∧ 𝑏 ∈ (𝐾‘𝑎)) → (𝐿‘𝑏) = (℩𝑠(𝑠 ∈ ω ∧ 𝑏 ∈ (𝐾‘𝑠)))) |
29 | | simp1r 1197 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑏 ∈ (𝐾‘𝑎)) ∧ 𝑎 ∈ ω ∧ 𝑠 ∈ ω) → 𝑏 ∈ (𝐾‘𝑎)) |
30 | | simpl1 1190 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑎 ∈ ω ∧ 𝑠 ∈ ω) ∧ 𝑠 ≠ 𝑎) → 𝜑) |
31 | | simpr 485 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑎 ∈ ω ∧ 𝑠 ∈ ω) ∧ 𝑠 ≠ 𝑎) → 𝑠 ≠ 𝑎) |
32 | 31 | necomd 2999 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑎 ∈ ω ∧ 𝑠 ∈ ω) ∧ 𝑠 ≠ 𝑎) → 𝑎 ≠ 𝑠) |
33 | | simpl2 1191 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑎 ∈ ω ∧ 𝑠 ∈ ω) ∧ 𝑠 ≠ 𝑎) → 𝑎 ∈ ω) |
34 | | simpl3 1192 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑎 ∈ ω ∧ 𝑠 ∈ ω) ∧ 𝑠 ≠ 𝑎) → 𝑠 ∈ ω) |
35 | 12, 13, 14, 15, 16, 17 | isf32lem7 10115 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑎 ≠ 𝑠) ∧ (𝑎 ∈ ω ∧ 𝑠 ∈ ω)) → ((𝐾‘𝑎) ∩ (𝐾‘𝑠)) = ∅) |
36 | 30, 32, 33, 34, 35 | syl22anc 836 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑎 ∈ ω ∧ 𝑠 ∈ ω) ∧ 𝑠 ≠ 𝑎) → ((𝐾‘𝑎) ∩ (𝐾‘𝑠)) = ∅) |
37 | | disj1 4384 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐾‘𝑎) ∩ (𝐾‘𝑠)) = ∅ ↔ ∀𝑏(𝑏 ∈ (𝐾‘𝑎) → ¬ 𝑏 ∈ (𝐾‘𝑠))) |
38 | 36, 37 | sylib 217 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑎 ∈ ω ∧ 𝑠 ∈ ω) ∧ 𝑠 ≠ 𝑎) → ∀𝑏(𝑏 ∈ (𝐾‘𝑎) → ¬ 𝑏 ∈ (𝐾‘𝑠))) |
39 | 38 | ex 413 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑎 ∈ ω ∧ 𝑠 ∈ ω) → (𝑠 ≠ 𝑎 → ∀𝑏(𝑏 ∈ (𝐾‘𝑎) → ¬ 𝑏 ∈ (𝐾‘𝑠)))) |
40 | | sp 2176 |
. . . . . . . . . . . . . . . . . . 19
⊢
(∀𝑏(𝑏 ∈ (𝐾‘𝑎) → ¬ 𝑏 ∈ (𝐾‘𝑠)) → (𝑏 ∈ (𝐾‘𝑎) → ¬ 𝑏 ∈ (𝐾‘𝑠))) |
41 | 39, 40 | syl6 35 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑎 ∈ ω ∧ 𝑠 ∈ ω) → (𝑠 ≠ 𝑎 → (𝑏 ∈ (𝐾‘𝑎) → ¬ 𝑏 ∈ (𝐾‘𝑠)))) |
42 | 41 | com23 86 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑎 ∈ ω ∧ 𝑠 ∈ ω) → (𝑏 ∈ (𝐾‘𝑎) → (𝑠 ≠ 𝑎 → ¬ 𝑏 ∈ (𝐾‘𝑠)))) |
43 | 42 | 3adant1r 1176 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑏 ∈ (𝐾‘𝑎)) ∧ 𝑎 ∈ ω ∧ 𝑠 ∈ ω) → (𝑏 ∈ (𝐾‘𝑎) → (𝑠 ≠ 𝑎 → ¬ 𝑏 ∈ (𝐾‘𝑠)))) |
44 | 29, 43 | mpd 15 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑏 ∈ (𝐾‘𝑎)) ∧ 𝑎 ∈ ω ∧ 𝑠 ∈ ω) → (𝑠 ≠ 𝑎 → ¬ 𝑏 ∈ (𝐾‘𝑠))) |
45 | 44 | necon4ad 2962 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑏 ∈ (𝐾‘𝑎)) ∧ 𝑎 ∈ ω ∧ 𝑠 ∈ ω) → (𝑏 ∈ (𝐾‘𝑠) → 𝑠 = 𝑎)) |
46 | 45 | 3expia 1120 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑏 ∈ (𝐾‘𝑎)) ∧ 𝑎 ∈ ω) → (𝑠 ∈ ω → (𝑏 ∈ (𝐾‘𝑠) → 𝑠 = 𝑎))) |
47 | 46 | impd 411 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑏 ∈ (𝐾‘𝑎)) ∧ 𝑎 ∈ ω) → ((𝑠 ∈ ω ∧ 𝑏 ∈ (𝐾‘𝑠)) → 𝑠 = 𝑎)) |
48 | | eleq1w 2821 |
. . . . . . . . . . . . . . . 16
⊢ (𝑠 = 𝑎 → (𝑠 ∈ ω ↔ 𝑎 ∈ ω)) |
49 | | fveq2 6774 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑠 = 𝑎 → (𝐾‘𝑠) = (𝐾‘𝑎)) |
50 | 49 | eleq2d 2824 |
. . . . . . . . . . . . . . . 16
⊢ (𝑠 = 𝑎 → (𝑏 ∈ (𝐾‘𝑠) ↔ 𝑏 ∈ (𝐾‘𝑎))) |
51 | 48, 50 | anbi12d 631 |
. . . . . . . . . . . . . . 15
⊢ (𝑠 = 𝑎 → ((𝑠 ∈ ω ∧ 𝑏 ∈ (𝐾‘𝑠)) ↔ (𝑎 ∈ ω ∧ 𝑏 ∈ (𝐾‘𝑎)))) |
52 | 51 | biimprcd 249 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 ∈ ω ∧ 𝑏 ∈ (𝐾‘𝑎)) → (𝑠 = 𝑎 → (𝑠 ∈ ω ∧ 𝑏 ∈ (𝐾‘𝑠)))) |
53 | 52 | ancoms 459 |
. . . . . . . . . . . . 13
⊢ ((𝑏 ∈ (𝐾‘𝑎) ∧ 𝑎 ∈ ω) → (𝑠 = 𝑎 → (𝑠 ∈ ω ∧ 𝑏 ∈ (𝐾‘𝑠)))) |
54 | 53 | adantll 711 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑏 ∈ (𝐾‘𝑎)) ∧ 𝑎 ∈ ω) → (𝑠 = 𝑎 → (𝑠 ∈ ω ∧ 𝑏 ∈ (𝐾‘𝑠)))) |
55 | 47, 54 | impbid 211 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑏 ∈ (𝐾‘𝑎)) ∧ 𝑎 ∈ ω) → ((𝑠 ∈ ω ∧ 𝑏 ∈ (𝐾‘𝑠)) ↔ 𝑠 = 𝑎)) |
56 | 55 | iota5 6416 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑏 ∈ (𝐾‘𝑎)) ∧ 𝑎 ∈ ω) → (℩𝑠(𝑠 ∈ ω ∧ 𝑏 ∈ (𝐾‘𝑠))) = 𝑎) |
57 | 56 | an32s 649 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ ω) ∧ 𝑏 ∈ (𝐾‘𝑎)) → (℩𝑠(𝑠 ∈ ω ∧ 𝑏 ∈ (𝐾‘𝑠))) = 𝑎) |
58 | 28, 57 | eqtr2d 2779 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑎 ∈ ω) ∧ 𝑏 ∈ (𝐾‘𝑎)) → 𝑎 = (𝐿‘𝑏)) |
59 | 22, 58 | jca 512 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ ω) ∧ 𝑏 ∈ (𝐾‘𝑎)) → (𝑏 ∈ 𝐺 ∧ 𝑎 = (𝐿‘𝑏))) |
60 | 59 | ex 413 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ ω) → (𝑏 ∈ (𝐾‘𝑎) → (𝑏 ∈ 𝐺 ∧ 𝑎 = (𝐿‘𝑏)))) |
61 | 60 | eximdv 1920 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ ω) → (∃𝑏 𝑏 ∈ (𝐾‘𝑎) → ∃𝑏(𝑏 ∈ 𝐺 ∧ 𝑎 = (𝐿‘𝑏)))) |
62 | | df-rex 3070 |
. . . . 5
⊢
(∃𝑏 ∈
𝐺 𝑎 = (𝐿‘𝑏) ↔ ∃𝑏(𝑏 ∈ 𝐺 ∧ 𝑎 = (𝐿‘𝑏))) |
63 | 61, 62 | syl6ibr 251 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ ω) → (∃𝑏 𝑏 ∈ (𝐾‘𝑎) → ∃𝑏 ∈ 𝐺 𝑎 = (𝐿‘𝑏))) |
64 | 20, 63 | mpd 15 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ ω) → ∃𝑏 ∈ 𝐺 𝑎 = (𝐿‘𝑏)) |
65 | 64 | ralrimiva 3103 |
. 2
⊢ (𝜑 → ∀𝑎 ∈ ω ∃𝑏 ∈ 𝐺 𝑎 = (𝐿‘𝑏)) |
66 | | dffo3 6978 |
. 2
⊢ (𝐿:𝐺–onto→ω ↔ (𝐿:𝐺⟶ω ∧ ∀𝑎 ∈ ω ∃𝑏 ∈ 𝐺 𝑎 = (𝐿‘𝑏))) |
67 | 11, 65, 66 | sylanbrc 583 |
1
⊢ (𝜑 → 𝐿:𝐺–onto→ω) |