Metamath Proof Explorer


Theorem isf33lem

Description: Lemma for isfin3-3 . (Contributed by Stefan O'Rear, 17-May-2015)

Ref Expression
Assertion isf33lem FinIII = { 𝑔 ∣ ∀ 𝑎 ∈ ( 𝒫 𝑔m ω ) ( ∀ 𝑥 ∈ ω ( 𝑎 ‘ suc 𝑥 ) ⊆ ( 𝑎𝑥 ) → ran 𝑎 ∈ ran 𝑎 ) }

Proof

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 𝑎 ) }