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 ⊢ F = g | ∀ a ∈ 𝒫 g ω ∀ x ∈ ω a ⁡ suc ⁡ x ⊆ a ⁡ x → ⋂ ran ⁡ a ∈ ran ⁡ a
Assertion isf32lem12 ⊢ G ∈ V → ¬ ω ≼ * G → G ∈ F

Proof

Step Hyp Ref Expression
1 isf32lem40.f ⊢ F = g | ∀ a ∈ 𝒫 g ω ∀ x ∈ ω a ⁡ suc ⁡ x ⊆ a ⁡ x → ⋂ ran ⁡ a ∈ ran ⁡ a
2 elmapi ⊢ f ∈ 𝒫 G ω → f : ω ⟶ 𝒫 G
3 isf32lem11 ⊢ G ∈ V ∧ f : ω ⟶ 𝒫 G ∧ ∀ b ∈ ω f ⁡ suc ⁡ b ⊆ f ⁡ b ∧ ¬ ⋂ ran ⁡ f ∈ ran ⁡ f → ω ≼ * G
4 3 expcom ⊢ f : ω ⟶ 𝒫 G ∧ ∀ b ∈ ω f ⁡ suc ⁡ b ⊆ f ⁡ b ∧ ¬ ⋂ ran ⁡ f ∈ ran ⁡ f → G ∈ V → ω ≼ * G
5 4 3expa ⊢ f : ω ⟶ 𝒫 G ∧ ∀ b ∈ ω f ⁡ suc ⁡ b ⊆ f ⁡ b ∧ ¬ ⋂ ran ⁡ f ∈ ran ⁡ f → G ∈ V → ω ≼ * G
6 5 impancom ⊢ f : ω ⟶ 𝒫 G ∧ ∀ b ∈ ω f ⁡ suc ⁡ b ⊆ f ⁡ b ∧ G ∈ V → ¬ ⋂ ran ⁡ f ∈ ran ⁡ f → ω ≼ * G
7 6 con1d ⊢ f : ω ⟶ 𝒫 G ∧ ∀ b ∈ ω f ⁡ suc ⁡ b ⊆ f ⁡ b ∧ G ∈ V → ¬ ω ≼ * G → ⋂ ran ⁡ f ∈ ran ⁡ f
8 7 exp31 ⊢ f : ω ⟶ 𝒫 G → ∀ b ∈ ω f ⁡ suc ⁡ b ⊆ f ⁡ b → G ∈ V → ¬ ω ≼ * G → ⋂ ran ⁡ f ∈ ran ⁡ f
9 2 8 syl ⊢ f ∈ 𝒫 G ω → ∀ b ∈ ω f ⁡ suc ⁡ b ⊆ f ⁡ b → G ∈ V → ¬ ω ≼ * G → ⋂ ran ⁡ f ∈ ran ⁡ f
10 9 com4t ⊢ G ∈ V → ¬ ω ≼ * G → f ∈ 𝒫 G ω → ∀ b ∈ ω f ⁡ suc ⁡ b ⊆ f ⁡ b → ⋂ ran ⁡ f ∈ ran ⁡ f
11 10 ralrimdv ⊢ G ∈ V → ¬ ω ≼ * G → ∀ f ∈ 𝒫 G ω ∀ b ∈ ω f ⁡ suc ⁡ b ⊆ f ⁡ b → ⋂ ran ⁡ f ∈ ran ⁡ f
12 1 isfin3ds ⊢ G ∈ V → G ∈ F ↔ ∀ f ∈ 𝒫 G ω ∀ b ∈ ω f ⁡ suc ⁡ b ⊆ f ⁡ b → ⋂ ran ⁡ f ∈ ran ⁡ f
13 11 12 sylibrd ⊢ G ∈ V → ¬ ω ≼ * G → G ∈ F