This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐹 = { 𝑔 ∣ ∀ 𝑎 ∈ ( 𝒫 𝑔 ↑m ω ) ( ∀ 𝑏 ∈ ω ( 𝑎 ‘ suc 𝑏 ) ⊆ ( 𝑎 ‘ 𝑏 ) → ∩ ran 𝑎 ∈ ran 𝑎 ) }
Assertion isfin3ds ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ 𝐹 ↔ ∀ 𝑓 ∈ ( 𝒫 𝐴 ↑m ω ) ( ∀ 𝑥 ∈ ω ( 𝑓 ‘ suc 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) → ∩ ran 𝑓 ∈ ran 𝑓 ) ) )

Proof

Step Hyp Ref Expression
1 isfin3ds.f ⊢ 𝐹 = { 𝑔 ∣ ∀ 𝑎 ∈ ( 𝒫 𝑔 ↑m ω ) ( ∀ 𝑏 ∈ ω ( 𝑎 ‘ suc 𝑏 ) ⊆ ( 𝑎 ‘ 𝑏 ) → ∩ ran 𝑎 ∈ ran 𝑎 ) }
2 suceq ⊢ ( 𝑏 = 𝑥 → suc 𝑏 = suc 𝑥 )
3 2 fveq2d ⊢ ( 𝑏 = 𝑥 → ( 𝑎 ‘ suc 𝑏 ) = ( 𝑎 ‘ suc 𝑥 ) )
4 fveq2 ⊢ ( 𝑏 = 𝑥 → ( 𝑎 ‘ 𝑏 ) = ( 𝑎 ‘ 𝑥 ) )
5 3 4 sseq12d ⊢ ( 𝑏 = 𝑥 → ( ( 𝑎 ‘ suc 𝑏 ) ⊆ ( 𝑎 ‘ 𝑏 ) ↔ ( 𝑎 ‘ suc 𝑥 ) ⊆ ( 𝑎 ‘ 𝑥 ) ) )
6 5 cbvralvw ⊢ ( ∀ 𝑏 ∈ ω ( 𝑎 ‘ suc 𝑏 ) ⊆ ( 𝑎 ‘ 𝑏 ) ↔ ∀ 𝑥 ∈ ω ( 𝑎 ‘ suc 𝑥 ) ⊆ ( 𝑎 ‘ 𝑥 ) )
7 fveq1 ⊢ ( 𝑎 = 𝑓 → ( 𝑎 ‘ suc 𝑥 ) = ( 𝑓 ‘ suc 𝑥 ) )
8 fveq1 ⊢ ( 𝑎 = 𝑓 → ( 𝑎 ‘ 𝑥 ) = ( 𝑓 ‘ 𝑥 ) )
9 7 8 sseq12d ⊢ ( 𝑎 = 𝑓 → ( ( 𝑎 ‘ suc 𝑥 ) ⊆ ( 𝑎 ‘ 𝑥 ) ↔ ( 𝑓 ‘ suc 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ) )
10 9 ralbidv ⊢ ( 𝑎 = 𝑓 → ( ∀ 𝑥 ∈ ω ( 𝑎 ‘ suc 𝑥 ) ⊆ ( 𝑎 ‘ 𝑥 ) ↔ ∀ 𝑥 ∈ ω ( 𝑓 ‘ suc 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ) )
11 6 10 bitrid ⊢ ( 𝑎 = 𝑓 → ( ∀ 𝑏 ∈ ω ( 𝑎 ‘ suc 𝑏 ) ⊆ ( 𝑎 ‘ 𝑏 ) ↔ ∀ 𝑥 ∈ ω ( 𝑓 ‘ suc 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ) )
12 rneq ⊢ ( 𝑎 = 𝑓 → ran 𝑎 = ran 𝑓 )
13 12 inteqd ⊢ ( 𝑎 = 𝑓 → ∩ ran 𝑎 = ∩ ran 𝑓 )
14 13 12 eleq12d ⊢ ( 𝑎 = 𝑓 → ( ∩ ran 𝑎 ∈ ran 𝑎 ↔ ∩ ran 𝑓 ∈ ran 𝑓 ) )
15 11 14 imbi12d ⊢ ( 𝑎 = 𝑓 → ( ( ∀ 𝑏 ∈ ω ( 𝑎 ‘ suc 𝑏 ) ⊆ ( 𝑎 ‘ 𝑏 ) → ∩ ran 𝑎 ∈ ran 𝑎 ) ↔ ( ∀ 𝑥 ∈ ω ( 𝑓 ‘ suc 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) → ∩ ran 𝑓 ∈ ran 𝑓 ) ) )
16 15 cbvralvw ⊢ ( ∀ 𝑎 ∈ ( 𝒫 𝑔 ↑m ω ) ( ∀ 𝑏 ∈ ω ( 𝑎 ‘ suc 𝑏 ) ⊆ ( 𝑎 ‘ 𝑏 ) → ∩ ran 𝑎 ∈ ran 𝑎 ) ↔ ∀ 𝑓 ∈ ( 𝒫 𝑔 ↑m ω ) ( ∀ 𝑥 ∈ ω ( 𝑓 ‘ suc 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) → ∩ ran 𝑓 ∈ ran 𝑓 ) )
17 pweq ⊢ ( 𝑔 = 𝐴 → 𝒫 𝑔 = 𝒫 𝐴 )
18 17 oveq1d ⊢ ( 𝑔 = 𝐴 → ( 𝒫 𝑔 ↑m ω ) = ( 𝒫 𝐴 ↑m ω ) )
19 18 raleqdv ⊢ ( 𝑔 = 𝐴 → ( ∀ 𝑓 ∈ ( 𝒫 𝑔 ↑m ω ) ( ∀ 𝑥 ∈ ω ( 𝑓 ‘ suc 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) → ∩ ran 𝑓 ∈ ran 𝑓 ) ↔ ∀ 𝑓 ∈ ( 𝒫 𝐴 ↑m ω ) ( ∀ 𝑥 ∈ ω ( 𝑓 ‘ suc 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) → ∩ ran 𝑓 ∈ ran 𝑓 ) ) )
20 16 19 bitrid ⊢ ( 𝑔 = 𝐴 → ( ∀ 𝑎 ∈ ( 𝒫 𝑔 ↑m ω ) ( ∀ 𝑏 ∈ ω ( 𝑎 ‘ suc 𝑏 ) ⊆ ( 𝑎 ‘ 𝑏 ) → ∩ ran 𝑎 ∈ ran 𝑎 ) ↔ ∀ 𝑓 ∈ ( 𝒫 𝐴 ↑m ω ) ( ∀ 𝑥 ∈ ω ( 𝑓 ‘ suc 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) → ∩ ran 𝑓 ∈ ran 𝑓 ) ) )
21 20 1 elab2g ⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ 𝐹 ↔ ∀ 𝑓 ∈ ( 𝒫 𝐴 ↑m ω ) ( ∀ 𝑥 ∈ ω ( 𝑓 ‘ suc 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) → ∩ ran 𝑓 ∈ ran 𝑓 ) ) )