Metamath Proof Explorer

Theorem isf32lem11

Description: Lemma for isfin3-2 . Remove hypotheses from isf32lem10 . (Contributed by Stefan O'Rear, 17-May-2015)

Ref Expression
Assertion isf32lem11 ⊢ G ∈ V ∧ F : ω ⟶ 𝒫 G ∧ ∀ b ∈ ω F ⁡ suc ⁡ b ⊆ F ⁡ b ∧ ¬ ⋂ ran ⁡ F ∈ ran ⁡ F → ω ≼ * G

Proof

Step Hyp Ref Expression
1 simp1 ⊢ F : ω ⟶ 𝒫 G ∧ ∀ b ∈ ω F ⁡ suc ⁡ b ⊆ F ⁡ b ∧ ¬ ⋂ ran ⁡ F ∈ ran ⁡ F → F : ω ⟶ 𝒫 G
2 suceq ⊢ b = c → suc ⁡ b = suc ⁡ c
3 2 fveq2d ⊢ b = c → F ⁡ suc ⁡ b = F ⁡ suc ⁡ c
4 fveq2 ⊢ b = c → F ⁡ b = F ⁡ c
5 3 4 sseq12d ⊢ b = c → F ⁡ suc ⁡ b ⊆ F ⁡ b ↔ F ⁡ suc ⁡ c ⊆ F ⁡ c
6 5 cbvralvw ⊢ ∀ b ∈ ω F ⁡ suc ⁡ b ⊆ F ⁡ b ↔ ∀ c ∈ ω F ⁡ suc ⁡ c ⊆ F ⁡ c
7 6 biimpi ⊢ ∀ b ∈ ω F ⁡ suc ⁡ b ⊆ F ⁡ b → ∀ c ∈ ω F ⁡ suc ⁡ c ⊆ F ⁡ c
8 7 3ad2ant2 ⊢ F : ω ⟶ 𝒫 G ∧ ∀ b ∈ ω F ⁡ suc ⁡ b ⊆ F ⁡ b ∧ ¬ ⋂ ran ⁡ F ∈ ran ⁡ F → ∀ c ∈ ω F ⁡ suc ⁡ c ⊆ F ⁡ c
9 simp3 ⊢ F : ω ⟶ 𝒫 G ∧ ∀ b ∈ ω F ⁡ suc ⁡ b ⊆ F ⁡ b ∧ ¬ ⋂ ran ⁡ F ∈ ran ⁡ F → ¬ ⋂ ran ⁡ F ∈ ran ⁡ F
10 suceq ⊢ e = d → suc ⁡ e = suc ⁡ d
11 10 fveq2d ⊢ e = d → F ⁡ suc ⁡ e = F ⁡ suc ⁡ d
12 fveq2 ⊢ e = d → F ⁡ e = F ⁡ d
13 11 12 psseq12d ⊢ e = d → F ⁡ suc ⁡ e ⊂ F ⁡ e ↔ F ⁡ suc ⁡ d ⊂ F ⁡ d
14 13 cbvrabv ⊢ e ∈ ω | F ⁡ suc ⁡ e ⊂ F ⁡ e = d ∈ ω | F ⁡ suc ⁡ d ⊂ F ⁡ d
15 eqid ⊢ f ∈ ω ⟼ ι g ∈ e ∈ ω | F ⁡ suc ⁡ e ⊂ F ⁡ e | g ∩ e ∈ ω | F ⁡ suc ⁡ e ⊂ F ⁡ e ≈ f = f ∈ ω ⟼ ι g ∈ e ∈ ω | F ⁡ suc ⁡ e ⊂ F ⁡ e | g ∩ e ∈ ω | F ⁡ suc ⁡ e ⊂ F ⁡ e ≈ f
16 eqid ⊢ h ∈ e ∈ ω | F ⁡ suc ⁡ e ⊂ F ⁡ e ⟼ F ⁡ h ∖ F ⁡ suc ⁡ h ∘ f ∈ ω ⟼ ι g ∈ e ∈ ω | F ⁡ suc ⁡ e ⊂ F ⁡ e | g ∩ e ∈ ω | F ⁡ suc ⁡ e ⊂ F ⁡ e ≈ f = h ∈ e ∈ ω | F ⁡ suc ⁡ e ⊂ F ⁡ e ⟼ F ⁡ h ∖ F ⁡ suc ⁡ h ∘ f ∈ ω ⟼ ι g ∈ e ∈ ω | F ⁡ suc ⁡ e ⊂ F ⁡ e | g ∩ e ∈ ω | F ⁡ suc ⁡ e ⊂ F ⁡ e ≈ f
17 eqid ⊢ k ∈ G ⟼ ι l | l ∈ ω ∧ k ∈ h ∈ e ∈ ω | F ⁡ suc ⁡ e ⊂ F ⁡ e ⟼ F ⁡ h ∖ F ⁡ suc ⁡ h ∘ f ∈ ω ⟼ ι g ∈ e ∈ ω | F ⁡ suc ⁡ e ⊂ F ⁡ e | g ∩ e ∈ ω | F ⁡ suc ⁡ e ⊂ F ⁡ e ≈ f ⁡ l = k ∈ G ⟼ ι l | l ∈ ω ∧ k ∈ h ∈ e ∈ ω | F ⁡ suc ⁡ e ⊂ F ⁡ e ⟼ F ⁡ h ∖ F ⁡ suc ⁡ h ∘ f ∈ ω ⟼ ι g ∈ e ∈ ω | F ⁡ suc ⁡ e ⊂ F ⁡ e | g ∩ e ∈ ω | F ⁡ suc ⁡ e ⊂ F ⁡ e ≈ f ⁡ l
18 1 8 9 14 15 16 17 isf32lem10 ⊢ F : ω ⟶ 𝒫 G ∧ ∀ b ∈ ω F ⁡ suc ⁡ b ⊆ F ⁡ b ∧ ¬ ⋂ ran ⁡ F ∈ ran ⁡ F → G ∈ V → ω ≼ * G
19 18 impcom ⊢ G ∈ V ∧ F : ω ⟶ 𝒫 G ∧ ∀ b ∈ ω F ⁡ suc ⁡ b ⊆ F ⁡ b ∧ ¬ ⋂ ran ⁡ F ∈ ran ⁡ F → ω ≼ * G