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

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