Theorem fin34i

Description: Inference from isfin3-4 . (Contributed by Mario Carneiro, 17-May-2015)

	Ref	Expression
Assertion	fin34i	⊢ ( ( 𝐴 ∈ FinIII ∧ 𝐺 : ω ⟶ 𝒫 𝐴 ∧ ∀ 𝑥 ∈ ω ( 𝐺 ‘ 𝑥 ) ⊆ ( 𝐺 ‘ suc 𝑥 ) ) → ∪ ran 𝐺 ∈ ran 𝐺 )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( 𝑦 ∈ 𝒫 𝐴 ↦ ( 𝐴 ∖ 𝑦 ) ) = ( 𝑦 ∈ 𝒫 𝐴 ↦ ( 𝐴 ∖ 𝑦 ) )
2	1	isf34lem7	⊢ ( ( 𝐴 ∈ FinIII ∧ 𝐺 : ω ⟶ 𝒫 𝐴 ∧ ∀ 𝑥 ∈ ω ( 𝐺 ‘ 𝑥 ) ⊆ ( 𝐺 ‘ suc 𝑥 ) ) → ∪ ran 𝐺 ∈ ran 𝐺 )