Theorem fin23lem19

Description: Lemma for fin23 . The first set in U to see an input set is either contained in it or disjoint from it. (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	fin23lem19	$$⊢A\in \mathrm{\omega }\to \left(U\left(\mathrm{suc}A\right)\subseteq t\left(A\right)\vee U\left(\mathrm{suc}A\right)\cap t\left(A\right)=\varnothing \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		eqif	$$⊢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)\leftrightarrow \left(\left(t\left(A\right)\cap U\left(A\right)=\varnothing \wedge U\left(\mathrm{suc}A\right)=U\left(A\right)\right)\vee \left(\neg t\left(A\right)\cap U\left(A\right)=\varnothing \wedge U\left(\mathrm{suc}A\right)=t\left(A\right)\cap U\left(A\right)\right)\right)$$
4	2 3	sylib	$$⊢A\in \mathrm{\omega }\to \left(\left(t\left(A\right)\cap U\left(A\right)=\varnothing \wedge U\left(\mathrm{suc}A\right)=U\left(A\right)\right)\vee \left(\neg t\left(A\right)\cap U\left(A\right)=\varnothing \wedge U\left(\mathrm{suc}A\right)=t\left(A\right)\cap U\left(A\right)\right)\right)$$
5		incom	$$⊢U\left(\mathrm{suc}A\right)\cap t\left(A\right)=t\left(A\right)\cap U\left(\mathrm{suc}A\right)$$
6		ineq2	$$⊢U\left(\mathrm{suc}A\right)=U\left(A\right)\to t\left(A\right)\cap U\left(\mathrm{suc}A\right)=t\left(A\right)\cap U\left(A\right)$$
7	6	eqeq1d	$$⊢U\left(\mathrm{suc}A\right)=U\left(A\right)\to \left(t\left(A\right)\cap U\left(\mathrm{suc}A\right)=\varnothing \leftrightarrow t\left(A\right)\cap U\left(A\right)=\varnothing \right)$$
8	7	biimparc	$$⊢\left(t\left(A\right)\cap U\left(A\right)=\varnothing \wedge U\left(\mathrm{suc}A\right)=U\left(A\right)\right)\to t\left(A\right)\cap U\left(\mathrm{suc}A\right)=\varnothing$$
9	5 8	eqtrid	$$⊢\left(t\left(A\right)\cap U\left(A\right)=\varnothing \wedge U\left(\mathrm{suc}A\right)=U\left(A\right)\right)\to U\left(\mathrm{suc}A\right)\cap t\left(A\right)=\varnothing$$
10		inss1	$$⊢t\left(A\right)\cap U\left(A\right)\subseteq t\left(A\right)$$
11		sseq1	$$⊢U\left(\mathrm{suc}A\right)=t\left(A\right)\cap U\left(A\right)\to \left(U\left(\mathrm{suc}A\right)\subseteq t\left(A\right)\leftrightarrow t\left(A\right)\cap U\left(A\right)\subseteq t\left(A\right)\right)$$
12	10 11	mpbiri	$$⊢U\left(\mathrm{suc}A\right)=t\left(A\right)\cap U\left(A\right)\to U\left(\mathrm{suc}A\right)\subseteq t\left(A\right)$$
13	12	adantl	$$⊢\left(\neg t\left(A\right)\cap U\left(A\right)=\varnothing \wedge U\left(\mathrm{suc}A\right)=t\left(A\right)\cap U\left(A\right)\right)\to U\left(\mathrm{suc}A\right)\subseteq t\left(A\right)$$
14	9 13	orim12i	$$⊢\left(\left(t\left(A\right)\cap U\left(A\right)=\varnothing \wedge U\left(\mathrm{suc}A\right)=U\left(A\right)\right)\vee \left(\neg t\left(A\right)\cap U\left(A\right)=\varnothing \wedge U\left(\mathrm{suc}A\right)=t\left(A\right)\cap U\left(A\right)\right)\right)\to \left(U\left(\mathrm{suc}A\right)\cap t\left(A\right)=\varnothing \vee U\left(\mathrm{suc}A\right)\subseteq t\left(A\right)\right)$$
15	4 14	syl	$$⊢A\in \mathrm{\omega }\to \left(U\left(\mathrm{suc}A\right)\cap t\left(A\right)=\varnothing \vee U\left(\mathrm{suc}A\right)\subseteq t\left(A\right)\right)$$
16	15	orcomd	$$⊢A\in \mathrm{\omega }\to \left(U\left(\mathrm{suc}A\right)\subseteq t\left(A\right)\vee U\left(\mathrm{suc}A\right)\cap t\left(A\right)=\varnothing \right)$$