Theorem fin23lem20

Description: Lemma for fin23 . X is either contained in or disjoint from all input sets. (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	fin23lem20	$$⊢A\in \mathrm{\omega }\to \left(\bigcap \mathrm{ran}U\subseteq t\left(A\right)\vee \bigcap \mathrm{ran}U\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	fnseqom	$$⊢UFn\mathrm{\omega }$$
3		peano2	$$⊢A\in \mathrm{\omega }\to \mathrm{suc}A\in \mathrm{\omega }$$
4		fnfvelrn	$$⊢\left(UFn\mathrm{\omega }\wedge \mathrm{suc}A\in \mathrm{\omega }\right)\to U\left(\mathrm{suc}A\right)\in \mathrm{ran}U$$
5	2 3 4	sylancr	$$⊢A\in \mathrm{\omega }\to U\left(\mathrm{suc}A\right)\in \mathrm{ran}U$$
6		intss1	$$⊢U\left(\mathrm{suc}A\right)\in \mathrm{ran}U\to \bigcap \mathrm{ran}U\subseteq U\left(\mathrm{suc}A\right)$$
7	5 6	syl	$$⊢A\in \mathrm{\omega }\to \bigcap \mathrm{ran}U\subseteq U\left(\mathrm{suc}A\right)$$
8	1	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)$$
9		sstr2	$$⊢\bigcap \mathrm{ran}U\subseteq U\left(\mathrm{suc}A\right)\to \left(U\left(\mathrm{suc}A\right)\subseteq t\left(A\right)\to \bigcap \mathrm{ran}U\subseteq t\left(A\right)\right)$$
10		ssdisj	$$⊢\left(\bigcap \mathrm{ran}U\subseteq U\left(\mathrm{suc}A\right)\wedge U\left(\mathrm{suc}A\right)\cap t\left(A\right)=\varnothing \right)\to \bigcap \mathrm{ran}U\cap t\left(A\right)=\varnothing$$
11	10	ex	$$⊢\bigcap \mathrm{ran}U\subseteq U\left(\mathrm{suc}A\right)\to \left(U\left(\mathrm{suc}A\right)\cap t\left(A\right)=\varnothing \to \bigcap \mathrm{ran}U\cap t\left(A\right)=\varnothing \right)$$
12	9 11	orim12d	$$⊢\bigcap \mathrm{ran}U\subseteq U\left(\mathrm{suc}A\right)\to \left(\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)\to \left(\bigcap \mathrm{ran}U\subseteq t\left(A\right)\vee \bigcap \mathrm{ran}U\cap t\left(A\right)=\varnothing \right)\right)$$
13	7 8 12	sylc	$$⊢A\in \mathrm{\omega }\to \left(\bigcap \mathrm{ran}U\subseteq t\left(A\right)\vee \bigcap \mathrm{ran}U\cap t\left(A\right)=\varnothing \right)$$