Step |
Hyp |
Ref |
Expression |
1 |
|
isf32lem.a |
⊢ ( 𝜑 → 𝐹 : ω ⟶ 𝒫 𝐺 ) |
2 |
|
isf32lem.b |
⊢ ( 𝜑 → ∀ 𝑥 ∈ ω ( 𝐹 ‘ suc 𝑥 ) ⊆ ( 𝐹 ‘ 𝑥 ) ) |
3 |
|
isf32lem.c |
⊢ ( 𝜑 → ¬ ∩ ran 𝐹 ∈ ran 𝐹 ) |
4 |
|
isf32lem.d |
⊢ 𝑆 = { 𝑦 ∈ ω ∣ ( 𝐹 ‘ suc 𝑦 ) ⊊ ( 𝐹 ‘ 𝑦 ) } |
5 |
|
isf32lem.e |
⊢ 𝐽 = ( 𝑢 ∈ ω ↦ ( ℩ 𝑣 ∈ 𝑆 ( 𝑣 ∩ 𝑆 ) ≈ 𝑢 ) ) |
6 |
|
isf32lem.f |
⊢ 𝐾 = ( ( 𝑤 ∈ 𝑆 ↦ ( ( 𝐹 ‘ 𝑤 ) ∖ ( 𝐹 ‘ suc 𝑤 ) ) ) ∘ 𝐽 ) |
7 |
|
isf32lem.g |
⊢ 𝐿 = ( 𝑡 ∈ 𝐺 ↦ ( ℩ 𝑠 ( 𝑠 ∈ ω ∧ 𝑡 ∈ ( 𝐾 ‘ 𝑠 ) ) ) ) |
8 |
1 2 3 4 5 6 7
|
isf32lem9 |
⊢ ( 𝜑 → 𝐿 : 𝐺 –onto→ ω ) |
9 |
|
fof |
⊢ ( 𝐿 : 𝐺 –onto→ ω → 𝐿 : 𝐺 ⟶ ω ) |
10 |
8 9
|
syl |
⊢ ( 𝜑 → 𝐿 : 𝐺 ⟶ ω ) |
11 |
|
fex |
⊢ ( ( 𝐿 : 𝐺 ⟶ ω ∧ 𝐺 ∈ 𝑉 ) → 𝐿 ∈ V ) |
12 |
10 11
|
sylan |
⊢ ( ( 𝜑 ∧ 𝐺 ∈ 𝑉 ) → 𝐿 ∈ V ) |
13 |
12
|
ex |
⊢ ( 𝜑 → ( 𝐺 ∈ 𝑉 → 𝐿 ∈ V ) ) |
14 |
|
fowdom |
⊢ ( ( 𝐿 ∈ V ∧ 𝐿 : 𝐺 –onto→ ω ) → ω ≼* 𝐺 ) |
15 |
14
|
expcom |
⊢ ( 𝐿 : 𝐺 –onto→ ω → ( 𝐿 ∈ V → ω ≼* 𝐺 ) ) |
16 |
8 13 15
|
sylsyld |
⊢ ( 𝜑 → ( 𝐺 ∈ 𝑉 → ω ≼* 𝐺 ) ) |