# Metamath Proof Explorer

## 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)↔\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(¬{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(¬{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 ↔{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 syl5eq ${⊢}\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)↔{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(¬{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(¬{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)$