Metamath Proof Explorer


Theorem isf32lem10

Description: Lemma for isfin3-2 . Write in terms of weak dominance. (Contributed by Stefan O'Rear, 6-Nov-2014) (Revised by Mario Carneiro, 17-May-2015)

Ref Expression
Hypotheses isf32lem.a ( 𝜑𝐹 : ω ⟶ 𝒫 𝐺 )
isf32lem.b ( 𝜑 → ∀ 𝑥 ∈ ω ( 𝐹 ‘ suc 𝑥 ) ⊆ ( 𝐹𝑥 ) )
isf32lem.c ( 𝜑 → ¬ ran 𝐹 ∈ ran 𝐹 )
isf32lem.d 𝑆 = { 𝑦 ∈ ω ∣ ( 𝐹 ‘ suc 𝑦 ) ⊊ ( 𝐹𝑦 ) }
isf32lem.e 𝐽 = ( 𝑢 ∈ ω ↦ ( 𝑣𝑆 ( 𝑣𝑆 ) ≈ 𝑢 ) )
isf32lem.f 𝐾 = ( ( 𝑤𝑆 ↦ ( ( 𝐹𝑤 ) ∖ ( 𝐹 ‘ suc 𝑤 ) ) ) ∘ 𝐽 )
isf32lem.g 𝐿 = ( 𝑡𝐺 ↦ ( ℩ 𝑠 ( 𝑠 ∈ ω ∧ 𝑡 ∈ ( 𝐾𝑠 ) ) ) )
Assertion isf32lem10 ( 𝜑 → ( 𝐺𝑉 → ω ≼* 𝐺 ) )

Proof

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 ( 𝜑 → ( 𝐺𝑉 → ω ≼* 𝐺 ) )