Metamath Proof Explorer

Theorem isf33lem

Description: Lemma for isfin3-3 . (Contributed by Stefan O'Rear, 17-May-2015)

Ref Expression
Assertion isf33lem ⊢ FinIII = g | ∀ a ∈ 𝒫 g ω ∀ x ∈ ω a ⁡ suc ⁡ x ⊆ a ⁡ x → ⋂ ran ⁡ a ∈ ran ⁡ a

Proof

Step Hyp Ref Expression
1 isfin32i ⊢ f ∈ FinIII → ¬ ω ≼ * f
2 fveq1 ⊢ a = b → a ⁡ suc ⁡ x = b ⁡ suc ⁡ x
3 fveq1 ⊢ a = b → a ⁡ x = b ⁡ x
4 2 3 sseq12d ⊢ a = b → a ⁡ suc ⁡ x ⊆ a ⁡ x ↔ b ⁡ suc ⁡ x ⊆ b ⁡ x
5 4 ralbidv ⊢ a = b → ∀ x ∈ ω a ⁡ suc ⁡ x ⊆ a ⁡ x ↔ ∀ x ∈ ω b ⁡ suc ⁡ x ⊆ b ⁡ x
6 rneq ⊢ a = b → ran ⁡ a = ran ⁡ b
7 6 inteqd ⊢ a = b → ⋂ ran ⁡ a = ⋂ ran ⁡ b
8 7 6 eleq12d ⊢ a = b → ⋂ ran ⁡ a ∈ ran ⁡ a ↔ ⋂ ran ⁡ b ∈ ran ⁡ b
9 5 8 imbi12d ⊢ a = b → ∀ x ∈ ω a ⁡ suc ⁡ x ⊆ a ⁡ x → ⋂ ran ⁡ a ∈ ran ⁡ a ↔ ∀ x ∈ ω b ⁡ suc ⁡ x ⊆ b ⁡ x → ⋂ ran ⁡ b ∈ ran ⁡ b
10 9 cbvralvw ⊢ ∀ a ∈ 𝒫 g ω ∀ x ∈ ω a ⁡ suc ⁡ x ⊆ a ⁡ x → ⋂ ran ⁡ a ∈ ran ⁡ a ↔ ∀ b ∈ 𝒫 g ω ∀ x ∈ ω b ⁡ suc ⁡ x ⊆ b ⁡ x → ⋂ ran ⁡ b ∈ ran ⁡ b
11 pweq ⊢ g = y → 𝒫 g = 𝒫 y
12 11 oveq1d ⊢ g = y → 𝒫 g ω = 𝒫 y ω
13 12 raleqdv ⊢ g = y → ∀ b ∈ 𝒫 g ω ∀ x ∈ ω b ⁡ suc ⁡ x ⊆ b ⁡ x → ⋂ ran ⁡ b ∈ ran ⁡ b ↔ ∀ b ∈ 𝒫 y ω ∀ x ∈ ω b ⁡ suc ⁡ x ⊆ b ⁡ x → ⋂ ran ⁡ b ∈ ran ⁡ b
14 10 13 bitrid ⊢ g = y → ∀ a ∈ 𝒫 g ω ∀ x ∈ ω a ⁡ suc ⁡ x ⊆ a ⁡ x → ⋂ ran ⁡ a ∈ ran ⁡ a ↔ ∀ b ∈ 𝒫 y ω ∀ x ∈ ω b ⁡ suc ⁡ x ⊆ b ⁡ x → ⋂ ran ⁡ b ∈ ran ⁡ b
15 14 cbvabv ⊢ g | ∀ a ∈ 𝒫 g ω ∀ x ∈ ω a ⁡ suc ⁡ x ⊆ a ⁡ x → ⋂ ran ⁡ a ∈ ran ⁡ a = y | ∀ b ∈ 𝒫 y ω ∀ x ∈ ω b ⁡ suc ⁡ x ⊆ b ⁡ x → ⋂ ran ⁡ b ∈ ran ⁡ b
16 15 isf32lem12 ⊢ f ∈ FinIII → ¬ ω ≼ * f → f ∈ g | ∀ a ∈ 𝒫 g ω ∀ x ∈ ω a ⁡ suc ⁡ x ⊆ a ⁡ x → ⋂ ran ⁡ a ∈ ran ⁡ a
17 1 16 mpd ⊢ f ∈ FinIII → f ∈ g | ∀ a ∈ 𝒫 g ω ∀ x ∈ ω a ⁡ suc ⁡ x ⊆ a ⁡ x → ⋂ ran ⁡ a ∈ ran ⁡ a
18 10 abbii ⊢ g | ∀ a ∈ 𝒫 g ω ∀ x ∈ ω a ⁡ suc ⁡ x ⊆ a ⁡ x → ⋂ ran ⁡ a ∈ ran ⁡ a = g | ∀ b ∈ 𝒫 g ω ∀ x ∈ ω b ⁡ suc ⁡ x ⊆ b ⁡ x → ⋂ ran ⁡ b ∈ ran ⁡ b
19 18 fin23lem41 ⊢ f ∈ g | ∀ a ∈ 𝒫 g ω ∀ x ∈ ω a ⁡ suc ⁡ x ⊆ a ⁡ x → ⋂ ran ⁡ a ∈ ran ⁡ a → f ∈ FinIII
20 17 19 impbii ⊢ f ∈ FinIII ↔ f ∈ g | ∀ a ∈ 𝒫 g ω ∀ x ∈ ω a ⁡ suc ⁡ x ⊆ a ⁡ x → ⋂ ran ⁡ a ∈ ran ⁡ a
21 20 eqriv ⊢ FinIII = g | ∀ a ∈ 𝒫 g ω ∀ x ∈ ω a ⁡ suc ⁡ x ⊆ a ⁡ x → ⋂ ran ⁡ a ∈ ran ⁡ a