Description: Inference from isfin3-4 . (Contributed by Mario Carneiro, 17-May-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | fin34i | ⊢ ( ( 𝐴 ∈ FinIII ∧ 𝐺 : ω ⟶ 𝒫 𝐴 ∧ ∀ 𝑥 ∈ ω ( 𝐺 ‘ 𝑥 ) ⊆ ( 𝐺 ‘ suc 𝑥 ) ) → ∪ ran 𝐺 ∈ ran 𝐺 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid | ⊢ ( 𝑦 ∈ 𝒫 𝐴 ↦ ( 𝐴 ∖ 𝑦 ) ) = ( 𝑦 ∈ 𝒫 𝐴 ↦ ( 𝐴 ∖ 𝑦 ) ) | |
2 | 1 | isf34lem7 | ⊢ ( ( 𝐴 ∈ FinIII ∧ 𝐺 : ω ⟶ 𝒫 𝐴 ∧ ∀ 𝑥 ∈ ω ( 𝐺 ‘ 𝑥 ) ⊆ ( 𝐺 ‘ suc 𝑥 ) ) → ∪ ran 𝐺 ∈ ran 𝐺 ) |