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

Metamath Proof Explorer

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	⊢ ( ( 𝐴 ∈ Fin^III ∧ 𝐹 : ω ⟶ 𝒫 𝐴 ∧ ∀ 𝑥 ∈ ω ( 𝐹 ‘ suc 𝑥 ) ⊆ ( 𝐹 ‘ 𝑥 ) ) → ∩ ran 𝐹 ∈ ran 𝐹 )

Proof

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