Theorem fin23lem13

Description: Lemma for fin23 . Each step of U is a decrease. (Contributed by Stefan O'Rear, 1-Nov-2014)

	Ref	Expression
Hypothesis	fin23lem.a	$$⊢U={seq}_{\omega }\left(\left(i\in \mathrm{\omega },u\in \mathrm{V}⟼if\left(t\left(i\right)\cap u=\varnothing ,u,t\left(i\right)\cap u\right)\right),\bigcup \mathrm{ran}t\right)$$
Assertion	fin23lem13	$$⊢A\in \mathrm{\omega }\to U\left(\mathrm{suc}A\right)\subseteq U\left(A\right)$$

Proof

Step	Hyp	Ref	Expression
1		fin23lem.a	$$⊢U={seq}_{\omega }\left(\left(i\in \mathrm{\omega },u\in \mathrm{V}⟼if\left(t\left(i\right)\cap u=\varnothing ,u,t\left(i\right)\cap u\right)\right),\bigcup \mathrm{ran}t\right)$$
2	1	fin23lem12	$$⊢A\in \mathrm{\omega }\to U\left(\mathrm{suc}A\right)=if\left(t\left(A\right)\cap U\left(A\right)=\varnothing ,U\left(A\right),t\left(A\right)\cap U\left(A\right)\right)$$
3		sseq1	$$⊢U\left(A\right)=if\left(t\left(A\right)\cap U\left(A\right)=\varnothing ,U\left(A\right),t\left(A\right)\cap U\left(A\right)\right)\to \left(U\left(A\right)\subseteq U\left(A\right)\leftrightarrow if\left(t\left(A\right)\cap U\left(A\right)=\varnothing ,U\left(A\right),t\left(A\right)\cap U\left(A\right)\right)\subseteq U\left(A\right)\right)$$
4		sseq1	$$⊢t\left(A\right)\cap U\left(A\right)=if\left(t\left(A\right)\cap U\left(A\right)=\varnothing ,U\left(A\right),t\left(A\right)\cap U\left(A\right)\right)\to \left(t\left(A\right)\cap U\left(A\right)\subseteq U\left(A\right)\leftrightarrow if\left(t\left(A\right)\cap U\left(A\right)=\varnothing ,U\left(A\right),t\left(A\right)\cap U\left(A\right)\right)\subseteq U\left(A\right)\right)$$
5		ssid	$$⊢U\left(A\right)\subseteq U\left(A\right)$$
6		inss2	$$⊢t\left(A\right)\cap U\left(A\right)\subseteq U\left(A\right)$$
7	3 4 5 6	keephyp	$$⊢if\left(t\left(A\right)\cap U\left(A\right)=\varnothing ,U\left(A\right),t\left(A\right)\cap U\left(A\right)\right)\subseteq U\left(A\right)$$
8	2 7	eqsstrdi	$$⊢A\in \mathrm{\omega }\to U\left(\mathrm{suc}A\right)\subseteq U\left(A\right)$$