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 ⊢ φ → F : ω ⟶ 𝒫 G
isf32lem.b ⊢ φ → ∀ x ∈ ω F ⁡ suc ⁡ x ⊆ F ⁡ x
isf32lem.c ⊢ φ → ¬ ⋂ ran ⁡ F ∈ ran ⁡ F
isf32lem.d ⊢ S = y ∈ ω | F ⁡ suc ⁡ y ⊂ F ⁡ y
isf32lem.e ⊢ J = u ∈ ω ⟼ ι v ∈ S | v ∩ S ≈ u
isf32lem.f ⊢ K = w ∈ S ⟼ F ⁡ w ∖ F ⁡ suc ⁡ w ∘ J
isf32lem.g ⊢ L = t ∈ G ⟼ ι s | s ∈ ω ∧ t ∈ K ⁡ s
Assertion isf32lem10 ⊢ φ → G ∈ V → ω ≼ * G

Proof

Step Hyp Ref Expression
1 isf32lem.a ⊢ φ → F : ω ⟶ 𝒫 G
2 isf32lem.b ⊢ φ → ∀ x ∈ ω F ⁡ suc ⁡ x ⊆ F ⁡ x
3 isf32lem.c ⊢ φ → ¬ ⋂ ran ⁡ F ∈ ran ⁡ F
4 isf32lem.d ⊢ S = y ∈ ω | F ⁡ suc ⁡ y ⊂ F ⁡ y
5 isf32lem.e ⊢ J = u ∈ ω ⟼ ι v ∈ S | v ∩ S ≈ u
6 isf32lem.f ⊢ K = w ∈ S ⟼ F ⁡ w ∖ F ⁡ suc ⁡ w ∘ J
7 isf32lem.g ⊢ L = t ∈ G ⟼ ι s | s ∈ ω ∧ t ∈ K ⁡ s
8 1 2 3 4 5 6 7 isf32lem9 ⊢ φ → L : G ⟶ onto ω
9 fof ⊢ L : G ⟶ onto ω → L : G ⟶ ω
10 8 9 syl ⊢ φ → L : G ⟶ ω
11 fex ⊢ L : G ⟶ ω ∧ G ∈ V → L ∈ V
12 10 11 sylan ⊢ φ ∧ G ∈ V → L ∈ V
13 12 ex ⊢ φ → G ∈ V → L ∈ V
14 fowdom ⊢ L ∈ V ∧ L : G ⟶ onto ω → ω ≼ * G
15 14 expcom ⊢ L : G ⟶ onto ω → L ∈ V → ω ≼ * G
16 8 13 15 sylsyld ⊢ φ → G ∈ V → ω ≼ * G