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

Metamath Proof Explorer

Theorem isf32lem12

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

		Ref	Expression
	Hypothesis	isf32lem40.f	⊢ 𝐹 = { 𝑔 ∣ ∀ 𝑎 ∈ ( 𝒫 𝑔 ↑_m ω ) ( ∀ 𝑥 ∈ ω ( 𝑎 ‘ suc 𝑥 ) ⊆ ( 𝑎 ‘ 𝑥 ) → ∩ ran 𝑎 ∈ ran 𝑎 ) }
	Assertion	isf32lem12	⊢ ( 𝐺 ∈ 𝑉 → ( ¬ ω ≼^* 𝐺 → 𝐺 ∈ 𝐹 ) )

Proof

Step	Hyp	Ref	Expression
1		isf32lem40.f	⊢ 𝐹 = { 𝑔 ∣ ∀ 𝑎 ∈ ( 𝒫 𝑔 ↑_m ω ) ( ∀ 𝑥 ∈ ω ( 𝑎 ‘ suc 𝑥 ) ⊆ ( 𝑎 ‘ 𝑥 ) → ∩ ran 𝑎 ∈ ran 𝑎 ) }
2		elmapi	⊢ ( 𝑓 ∈ ( 𝒫 𝐺 ↑_m ω ) → 𝑓 : ω ⟶ 𝒫 𝐺 )
3		isf32lem11	⊢ ( ( 𝐺 ∈ 𝑉 ∧ ( 𝑓 : ω ⟶ 𝒫 𝐺 ∧ ∀ 𝑏 ∈ ω ( 𝑓 ‘ suc 𝑏 ) ⊆ ( 𝑓 ‘ 𝑏 ) ∧ ¬ ∩ ran 𝑓 ∈ ran 𝑓 ) ) → ω ≼^* 𝐺 )
4	3	expcom	⊢ ( ( 𝑓 : ω ⟶ 𝒫 𝐺 ∧ ∀ 𝑏 ∈ ω ( 𝑓 ‘ suc 𝑏 ) ⊆ ( 𝑓 ‘ 𝑏 ) ∧ ¬ ∩ ran 𝑓 ∈ ran 𝑓 ) → ( 𝐺 ∈ 𝑉 → ω ≼^* 𝐺 ) )
5	4	3expa	⊢ ( ( ( 𝑓 : ω ⟶ 𝒫 𝐺 ∧ ∀ 𝑏 ∈ ω ( 𝑓 ‘ suc 𝑏 ) ⊆ ( 𝑓 ‘ 𝑏 ) ) ∧ ¬ ∩ ran 𝑓 ∈ ran 𝑓 ) → ( 𝐺 ∈ 𝑉 → ω ≼^* 𝐺 ) )
6	5	impancom	⊢ ( ( ( 𝑓 : ω ⟶ 𝒫 𝐺 ∧ ∀ 𝑏 ∈ ω ( 𝑓 ‘ suc 𝑏 ) ⊆ ( 𝑓 ‘ 𝑏 ) ) ∧ 𝐺 ∈ 𝑉 ) → ( ¬ ∩ ran 𝑓 ∈ ran 𝑓 → ω ≼^* 𝐺 ) )
7	6	con1d	⊢ ( ( ( 𝑓 : ω ⟶ 𝒫 𝐺 ∧ ∀ 𝑏 ∈ ω ( 𝑓 ‘ suc 𝑏 ) ⊆ ( 𝑓 ‘ 𝑏 ) ) ∧ 𝐺 ∈ 𝑉 ) → ( ¬ ω ≼^* 𝐺 → ∩ ran 𝑓 ∈ ran 𝑓 ) )
8	7	exp31	⊢ ( 𝑓 : ω ⟶ 𝒫 𝐺 → ( ∀ 𝑏 ∈ ω ( 𝑓 ‘ suc 𝑏 ) ⊆ ( 𝑓 ‘ 𝑏 ) → ( 𝐺 ∈ 𝑉 → ( ¬ ω ≼^* 𝐺 → ∩ ran 𝑓 ∈ ran 𝑓 ) ) ) )
9	2 8	syl	⊢ ( 𝑓 ∈ ( 𝒫 𝐺 ↑_m ω ) → ( ∀ 𝑏 ∈ ω ( 𝑓 ‘ suc 𝑏 ) ⊆ ( 𝑓 ‘ 𝑏 ) → ( 𝐺 ∈ 𝑉 → ( ¬ ω ≼^* 𝐺 → ∩ ran 𝑓 ∈ ran 𝑓 ) ) ) )
10	9	com4t	⊢ ( 𝐺 ∈ 𝑉 → ( ¬ ω ≼^* 𝐺 → ( 𝑓 ∈ ( 𝒫 𝐺 ↑_m ω ) → ( ∀ 𝑏 ∈ ω ( 𝑓 ‘ suc 𝑏 ) ⊆ ( 𝑓 ‘ 𝑏 ) → ∩ ran 𝑓 ∈ ran 𝑓 ) ) ) )
11	10	ralrimdv	⊢ ( 𝐺 ∈ 𝑉 → ( ¬ ω ≼^* 𝐺 → ∀ 𝑓 ∈ ( 𝒫 𝐺 ↑_m ω ) ( ∀ 𝑏 ∈ ω ( 𝑓 ‘ suc 𝑏 ) ⊆ ( 𝑓 ‘ 𝑏 ) → ∩ ran 𝑓 ∈ ran 𝑓 ) ) )
12	1	isfin3ds	⊢ ( 𝐺 ∈ 𝑉 → ( 𝐺 ∈ 𝐹 ↔ ∀ 𝑓 ∈ ( 𝒫 𝐺 ↑_m ω ) ( ∀ 𝑏 ∈ ω ( 𝑓 ‘ suc 𝑏 ) ⊆ ( 𝑓 ‘ 𝑏 ) → ∩ ran 𝑓 ∈ ran 𝑓 ) ) )
13	11 12	sylibrd	⊢ ( 𝐺 ∈ 𝑉 → ( ¬ ω ≼^* 𝐺 → 𝐺 ∈ 𝐹 ) )