Metamath Proof Explorer

Theorem isfin3ds

Description: Property of a III-finite set (descending sequence version). (Contributed by Mario Carneiro, 16-May-2015)

Ref Expression
Hypothesis isfin3ds.f ⊢ F = g | ∀ a ∈ 𝒫 g ω ∀ b ∈ ω a ⁡ suc ⁡ b ⊆ a ⁡ b → ⋂ ran ⁡ a ∈ ran ⁡ a
Assertion isfin3ds ⊢ A ∈ V → A ∈ F ↔ ∀ f ∈ 𝒫 A ω ∀ x ∈ ω f ⁡ suc ⁡ x ⊆ f ⁡ x → ⋂ ran ⁡ f ∈ ran ⁡ f

Proof

Step Hyp Ref Expression
1 isfin3ds.f ⊢ F = g | ∀ a ∈ 𝒫 g ω ∀ b ∈ ω a ⁡ suc ⁡ b ⊆ a ⁡ b → ⋂ ran ⁡ a ∈ ran ⁡ a
2 suceq ⊢ b = x → suc ⁡ b = suc ⁡ x
3 2 fveq2d ⊢ b = x → a ⁡ suc ⁡ b = a ⁡ suc ⁡ x
4 fveq2 ⊢ b = x → a ⁡ b = a ⁡ x
5 3 4 sseq12d ⊢ b = x → a ⁡ suc ⁡ b ⊆ a ⁡ b ↔ a ⁡ suc ⁡ x ⊆ a ⁡ x
6 5 cbvralvw ⊢ ∀ b ∈ ω a ⁡ suc ⁡ b ⊆ a ⁡ b ↔ ∀ x ∈ ω a ⁡ suc ⁡ x ⊆ a ⁡ x
7 fveq1 ⊢ a = f → a ⁡ suc ⁡ x = f ⁡ suc ⁡ x
8 fveq1 ⊢ a = f → a ⁡ x = f ⁡ x
9 7 8 sseq12d ⊢ a = f → a ⁡ suc ⁡ x ⊆ a ⁡ x ↔ f ⁡ suc ⁡ x ⊆ f ⁡ x
10 9 ralbidv ⊢ a = f → ∀ x ∈ ω a ⁡ suc ⁡ x ⊆ a ⁡ x ↔ ∀ x ∈ ω f ⁡ suc ⁡ x ⊆ f ⁡ x
11 6 10 syl5bb ⊢ a = f → ∀ b ∈ ω a ⁡ suc ⁡ b ⊆ a ⁡ b ↔ ∀ x ∈ ω f ⁡ suc ⁡ x ⊆ f ⁡ x
12 rneq ⊢ a = f → ran ⁡ a = ran ⁡ f
13 12 inteqd ⊢ a = f → ⋂ ran ⁡ a = ⋂ ran ⁡ f
14 13 12 eleq12d ⊢ a = f → ⋂ ran ⁡ a ∈ ran ⁡ a ↔ ⋂ ran ⁡ f ∈ ran ⁡ f
15 11 14 imbi12d ⊢ a = f → ∀ b ∈ ω a ⁡ suc ⁡ b ⊆ a ⁡ b → ⋂ ran ⁡ a ∈ ran ⁡ a ↔ ∀ x ∈ ω f ⁡ suc ⁡ x ⊆ f ⁡ x → ⋂ ran ⁡ f ∈ ran ⁡ f
16 15 cbvralvw ⊢ ∀ a ∈ 𝒫 g ω ∀ b ∈ ω a ⁡ suc ⁡ b ⊆ a ⁡ b → ⋂ ran ⁡ a ∈ ran ⁡ a ↔ ∀ f ∈ 𝒫 g ω ∀ x ∈ ω f ⁡ suc ⁡ x ⊆ f ⁡ x → ⋂ ran ⁡ f ∈ ran ⁡ f
17 pweq ⊢ g = A → 𝒫 g = 𝒫 A
18 17 oveq1d ⊢ g = A → 𝒫 g ω = 𝒫 A ω
19 18 raleqdv ⊢ g = A → ∀ f ∈ 𝒫 g ω ∀ x ∈ ω f ⁡ suc ⁡ x ⊆ f ⁡ x → ⋂ ran ⁡ f ∈ ran ⁡ f ↔ ∀ f ∈ 𝒫 A ω ∀ x ∈ ω f ⁡ suc ⁡ x ⊆ f ⁡ x → ⋂ ran ⁡ f ∈ ran ⁡ f
20 16 19 syl5bb ⊢ g = A → ∀ a ∈ 𝒫 g ω ∀ b ∈ ω a ⁡ suc ⁡ b ⊆ a ⁡ b → ⋂ ran ⁡ a ∈ ran ⁡ a ↔ ∀ f ∈ 𝒫 A ω ∀ x ∈ ω f ⁡ suc ⁡ x ⊆ f ⁡ x → ⋂ ran ⁡ f ∈ ran ⁡ f
21 20 1 elab2g ⊢ A ∈ V → A ∈ F ↔ ∀ f ∈ 𝒫 A ω ∀ x ∈ ω f ⁡ suc ⁡ x ⊆ f ⁡ x → ⋂ ran ⁡ f ∈ ran ⁡ f