Theorem fin33i

Description: Inference from isfin3-3 . (This is actually a bit stronger than isfin3-3 because it does not assume F is a set and does not use the Axiom of Infinity either.) (Contributed by Mario Carneiro, 17-May-2015)

	Ref	Expression
Assertion	fin33i	⊢ ( ( 𝐴 ∈ FinIII ∧ 𝐹 : ω ⟶ 𝒫 𝐴 ∧ ∀ 𝑥 ∈ ω ( 𝐹 ‘ suc 𝑥 ) ⊆ ( 𝐹 ‘ 𝑥 ) ) → ∩ ran 𝐹 ∈ ran 𝐹 )

Proof

Step	Hyp	Ref	Expression
1		isfin32i	⊢ ( 𝐴 ∈ FinIII → ¬ ω ≼* 𝐴 )
2	1	3ad2ant1	⊢ ( ( 𝐴 ∈ FinIII ∧ 𝐹 : ω ⟶ 𝒫 𝐴 ∧ ∀ 𝑥 ∈ ω ( 𝐹 ‘ suc 𝑥 ) ⊆ ( 𝐹 ‘ 𝑥 ) ) → ¬ ω ≼* 𝐴 )
3		isf32lem11	⊢ ( ( 𝐴 ∈ FinIII ∧ ( 𝐹 : ω ⟶ 𝒫 𝐴 ∧ ∀ 𝑥 ∈ ω ( 𝐹 ‘ suc 𝑥 ) ⊆ ( 𝐹 ‘ 𝑥 ) ∧ ¬ ∩ ran 𝐹 ∈ ran 𝐹 ) ) → ω ≼* 𝐴 )
4	3	3exp2	⊢ ( 𝐴 ∈ FinIII → ( 𝐹 : ω ⟶ 𝒫 𝐴 → ( ∀ 𝑥 ∈ ω ( 𝐹 ‘ suc 𝑥 ) ⊆ ( 𝐹 ‘ 𝑥 ) → ( ¬ ∩ ran 𝐹 ∈ ran 𝐹 → ω ≼* 𝐴 ) ) ) )
5	4	3imp	⊢ ( ( 𝐴 ∈ FinIII ∧ 𝐹 : ω ⟶ 𝒫 𝐴 ∧ ∀ 𝑥 ∈ ω ( 𝐹 ‘ suc 𝑥 ) ⊆ ( 𝐹 ‘ 𝑥 ) ) → ( ¬ ∩ ran 𝐹 ∈ ran 𝐹 → ω ≼* 𝐴 ) )
6	2 5	mt3d	⊢ ( ( 𝐴 ∈ FinIII ∧ 𝐹 : ω ⟶ 𝒫 𝐴 ∧ ∀ 𝑥 ∈ ω ( 𝐹 ‘ suc 𝑥 ) ⊆ ( 𝐹 ‘ 𝑥 ) ) → ∩ ran 𝐹 ∈ ran 𝐹 )