Theorem fin34i

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

	Ref	Expression
Assertion	fin34i	$$⊢\left(A\in {\mathrm{Fin}}^{\mathrm{III}}\wedge G:\mathrm{\omega }⟶𝒫A\wedge \forall x\in \mathrm{\omega }G\left(x\right)\subseteq G\left(\mathrm{suc}x\right)\right)\to \bigcup \mathrm{ran}G\in \mathrm{ran}G$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢\left(y\in 𝒫A⟼A\setminus y\right)=\left(y\in 𝒫A⟼A\setminus y\right)$$
2	1	isf34lem7	$$⊢\left(A\in {\mathrm{Fin}}^{\mathrm{III}}\wedge G:\mathrm{\omega }⟶𝒫A\wedge \forall x\in \mathrm{\omega }G\left(x\right)\subseteq G\left(\mathrm{suc}x\right)\right)\to \bigcup \mathrm{ran}G\in \mathrm{ran}G$$