This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 bitrid ⊢ ( 𝑔 = 𝑦 → ( ∀ 𝑎 ∈ ( 𝒫 𝑔 ↑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 𝑎 ) }