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	$⊢ (A \in {Fin}^{III} \land F : ω ⟶ 𝒫 A \land \forall x \in ω F (suc x) \subseteq F (x)) \to ⋂ ran F \in ran F$

Proof

Step	Hyp	Ref	Expression
1		isfin32i	$⊢ A \in {Fin}^{III} \to \neg ω ≼^{*} A$
2	1	3ad2ant1	$⊢ (A \in {Fin}^{III} \land F : ω ⟶ 𝒫 A \land \forall x \in ω F (suc x) \subseteq F (x)) \to \neg ω ≼^{*} A$
3		isf32lem11	$⊢ (A \in {Fin}^{III} \land (F : ω ⟶ 𝒫 A \land \forall x \in ω F (suc x) \subseteq F (x) \land \neg ⋂ ran F \in ran F)) \to ω ≼^{*} A$
4	3	3exp2	$⊢ A \in {Fin}^{III} \to (F : ω ⟶ 𝒫 A \to (\forall x \in ω F (suc x) \subseteq F (x) \to (\neg ⋂ ran F \in ran F \to ω ≼^{*} A)))$
5	4	3imp	$⊢ (A \in {Fin}^{III} \land F : ω ⟶ 𝒫 A \land \forall x \in ω F (suc x) \subseteq F (x)) \to (\neg ⋂ ran F \in ran F \to ω ≼^{*} A)$
6	2 5	mt3d	$⊢ (A \in {Fin}^{III} \land F : ω ⟶ 𝒫 A \land \forall x \in ω F (suc x) \subseteq F (x)) \to ⋂ ran F \in ran F$