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

Metamath Proof Explorer

Theorem fin34i

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

		Ref	Expression
	Assertion	fin34i	$⊢ (A \in {Fin}^{III} \land G : ω ⟶ 𝒫 A \land \forall x \in ω G (x) \subseteq G (suc x)) \to ⋃ ran G \in ran G$

Step	Hyp	Ref	Expression
1		eqid	$⊢ (y \in 𝒫 A ⟼ A ∖ y) = (y \in 𝒫 A ⟼ A ∖ y)$
2	1	isf34lem7	$⊢ (A \in {Fin}^{III} \land G : ω ⟶ 𝒫 A \land \forall x \in ω G (x) \subseteq G (suc x)) \to ⋃ ran G \in ran G$