Step |
Hyp |
Ref |
Expression |
1 |
|
isfin32i |
⊢ ( 𝑓 ∈ FinIII → ¬ ω ≼* 𝑓 ) |
2 |
|
fveq1 |
⊢ ( 𝑎 = 𝑏 → ( 𝑎 ‘ suc 𝑥 ) = ( 𝑏 ‘ suc 𝑥 ) ) |
3 |
|
fveq1 |
⊢ ( 𝑎 = 𝑏 → ( 𝑎 ‘ 𝑥 ) = ( 𝑏 ‘ 𝑥 ) ) |
4 |
2 3
|
sseq12d |
⊢ ( 𝑎 = 𝑏 → ( ( 𝑎 ‘ suc 𝑥 ) ⊆ ( 𝑎 ‘ 𝑥 ) ↔ ( 𝑏 ‘ suc 𝑥 ) ⊆ ( 𝑏 ‘ 𝑥 ) ) ) |
5 |
4
|
ralbidv |
⊢ ( 𝑎 = 𝑏 → ( ∀ 𝑥 ∈ ω ( 𝑎 ‘ suc 𝑥 ) ⊆ ( 𝑎 ‘ 𝑥 ) ↔ ∀ 𝑥 ∈ ω ( 𝑏 ‘ suc 𝑥 ) ⊆ ( 𝑏 ‘ 𝑥 ) ) ) |
6 |
|
rneq |
⊢ ( 𝑎 = 𝑏 → ran 𝑎 = ran 𝑏 ) |
7 |
6
|
inteqd |
⊢ ( 𝑎 = 𝑏 → ∩ ran 𝑎 = ∩ ran 𝑏 ) |
8 |
7 6
|
eleq12d |
⊢ ( 𝑎 = 𝑏 → ( ∩ ran 𝑎 ∈ ran 𝑎 ↔ ∩ ran 𝑏 ∈ ran 𝑏 ) ) |
9 |
5 8
|
imbi12d |
⊢ ( 𝑎 = 𝑏 → ( ( ∀ 𝑥 ∈ ω ( 𝑎 ‘ suc 𝑥 ) ⊆ ( 𝑎 ‘ 𝑥 ) → ∩ ran 𝑎 ∈ ran 𝑎 ) ↔ ( ∀ 𝑥 ∈ ω ( 𝑏 ‘ suc 𝑥 ) ⊆ ( 𝑏 ‘ 𝑥 ) → ∩ ran 𝑏 ∈ ran 𝑏 ) ) ) |
10 |
9
|
cbvralvw |
⊢ ( ∀ 𝑎 ∈ ( 𝒫 𝑔 ↑m ω ) ( ∀ 𝑥 ∈ ω ( 𝑎 ‘ suc 𝑥 ) ⊆ ( 𝑎 ‘ 𝑥 ) → ∩ ran 𝑎 ∈ ran 𝑎 ) ↔ ∀ 𝑏 ∈ ( 𝒫 𝑔 ↑m ω ) ( ∀ 𝑥 ∈ ω ( 𝑏 ‘ suc 𝑥 ) ⊆ ( 𝑏 ‘ 𝑥 ) → ∩ ran 𝑏 ∈ ran 𝑏 ) ) |
11 |
|
pweq |
⊢ ( 𝑔 = 𝑦 → 𝒫 𝑔 = 𝒫 𝑦 ) |
12 |
11
|
oveq1d |
⊢ ( 𝑔 = 𝑦 → ( 𝒫 𝑔 ↑m ω ) = ( 𝒫 𝑦 ↑m ω ) ) |
13 |
12
|
raleqdv |
⊢ ( 𝑔 = 𝑦 → ( ∀ 𝑏 ∈ ( 𝒫 𝑔 ↑m ω ) ( ∀ 𝑥 ∈ ω ( 𝑏 ‘ suc 𝑥 ) ⊆ ( 𝑏 ‘ 𝑥 ) → ∩ ran 𝑏 ∈ ran 𝑏 ) ↔ ∀ 𝑏 ∈ ( 𝒫 𝑦 ↑m ω ) ( ∀ 𝑥 ∈ ω ( 𝑏 ‘ suc 𝑥 ) ⊆ ( 𝑏 ‘ 𝑥 ) → ∩ ran 𝑏 ∈ ran 𝑏 ) ) ) |
14 |
10 13
|
syl5bb |
⊢ ( 𝑔 = 𝑦 → ( ∀ 𝑎 ∈ ( 𝒫 𝑔 ↑m ω ) ( ∀ 𝑥 ∈ ω ( 𝑎 ‘ suc 𝑥 ) ⊆ ( 𝑎 ‘ 𝑥 ) → ∩ ran 𝑎 ∈ ran 𝑎 ) ↔ ∀ 𝑏 ∈ ( 𝒫 𝑦 ↑m ω ) ( ∀ 𝑥 ∈ ω ( 𝑏 ‘ suc 𝑥 ) ⊆ ( 𝑏 ‘ 𝑥 ) → ∩ ran 𝑏 ∈ ran 𝑏 ) ) ) |
15 |
14
|
cbvabv |
⊢ { 𝑔 ∣ ∀ 𝑎 ∈ ( 𝒫 𝑔 ↑m ω ) ( ∀ 𝑥 ∈ ω ( 𝑎 ‘ suc 𝑥 ) ⊆ ( 𝑎 ‘ 𝑥 ) → ∩ ran 𝑎 ∈ ran 𝑎 ) } = { 𝑦 ∣ ∀ 𝑏 ∈ ( 𝒫 𝑦 ↑m ω ) ( ∀ 𝑥 ∈ ω ( 𝑏 ‘ suc 𝑥 ) ⊆ ( 𝑏 ‘ 𝑥 ) → ∩ ran 𝑏 ∈ ran 𝑏 ) } |
16 |
15
|
isf32lem12 |
⊢ ( 𝑓 ∈ FinIII → ( ¬ ω ≼* 𝑓 → 𝑓 ∈ { 𝑔 ∣ ∀ 𝑎 ∈ ( 𝒫 𝑔 ↑m ω ) ( ∀ 𝑥 ∈ ω ( 𝑎 ‘ suc 𝑥 ) ⊆ ( 𝑎 ‘ 𝑥 ) → ∩ ran 𝑎 ∈ ran 𝑎 ) } ) ) |
17 |
1 16
|
mpd |
⊢ ( 𝑓 ∈ FinIII → 𝑓 ∈ { 𝑔 ∣ ∀ 𝑎 ∈ ( 𝒫 𝑔 ↑m ω ) ( ∀ 𝑥 ∈ ω ( 𝑎 ‘ suc 𝑥 ) ⊆ ( 𝑎 ‘ 𝑥 ) → ∩ ran 𝑎 ∈ ran 𝑎 ) } ) |
18 |
10
|
abbii |
⊢ { 𝑔 ∣ ∀ 𝑎 ∈ ( 𝒫 𝑔 ↑m ω ) ( ∀ 𝑥 ∈ ω ( 𝑎 ‘ suc 𝑥 ) ⊆ ( 𝑎 ‘ 𝑥 ) → ∩ ran 𝑎 ∈ ran 𝑎 ) } = { 𝑔 ∣ ∀ 𝑏 ∈ ( 𝒫 𝑔 ↑m ω ) ( ∀ 𝑥 ∈ ω ( 𝑏 ‘ suc 𝑥 ) ⊆ ( 𝑏 ‘ 𝑥 ) → ∩ ran 𝑏 ∈ ran 𝑏 ) } |
19 |
18
|
fin23lem41 |
⊢ ( 𝑓 ∈ { 𝑔 ∣ ∀ 𝑎 ∈ ( 𝒫 𝑔 ↑m ω ) ( ∀ 𝑥 ∈ ω ( 𝑎 ‘ suc 𝑥 ) ⊆ ( 𝑎 ‘ 𝑥 ) → ∩ ran 𝑎 ∈ ran 𝑎 ) } → 𝑓 ∈ FinIII ) |
20 |
17 19
|
impbii |
⊢ ( 𝑓 ∈ FinIII ↔ 𝑓 ∈ { 𝑔 ∣ ∀ 𝑎 ∈ ( 𝒫 𝑔 ↑m ω ) ( ∀ 𝑥 ∈ ω ( 𝑎 ‘ suc 𝑥 ) ⊆ ( 𝑎 ‘ 𝑥 ) → ∩ ran 𝑎 ∈ ran 𝑎 ) } ) |
21 |
20
|
eqriv |
⊢ FinIII = { 𝑔 ∣ ∀ 𝑎 ∈ ( 𝒫 𝑔 ↑m ω ) ( ∀ 𝑥 ∈ ω ( 𝑎 ‘ suc 𝑥 ) ⊆ ( 𝑎 ‘ 𝑥 ) → ∩ ran 𝑎 ∈ ran 𝑎 ) } |