# Metamath Proof Explorer

## Theorem fin23lem12

Description: The beginning of the proof that every II-finite set (every chain of subsets has a maximal element) is III-finite (has no denumerable collection of subsets).

This first section is dedicated to the construction of U and its intersection. First, the value of U at a successor. (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 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)$

### 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 seqomsuc ${⊢}{A}\in \mathrm{\omega }\to {U}\left(\mathrm{suc}{A}\right)={A}\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){U}\left({A}\right)$
3 fvex ${⊢}{U}\left({A}\right)\in \mathrm{V}$
4 fveq2 ${⊢}{i}={A}\to {t}\left({i}\right)={t}\left({A}\right)$
5 4 ineq1d ${⊢}{i}={A}\to {t}\left({i}\right)\cap {u}={t}\left({A}\right)\cap {u}$
6 5 eqeq1d ${⊢}{i}={A}\to \left({t}\left({i}\right)\cap {u}=\varnothing ↔{t}\left({A}\right)\cap {u}=\varnothing \right)$
7 6 5 ifbieq2d ${⊢}{i}={A}\to if\left({t}\left({i}\right)\cap {u}=\varnothing ,{u},{t}\left({i}\right)\cap {u}\right)=if\left({t}\left({A}\right)\cap {u}=\varnothing ,{u},{t}\left({A}\right)\cap {u}\right)$
8 ineq2 ${⊢}{u}={U}\left({A}\right)\to {t}\left({A}\right)\cap {u}={t}\left({A}\right)\cap {U}\left({A}\right)$
9 8 eqeq1d ${⊢}{u}={U}\left({A}\right)\to \left({t}\left({A}\right)\cap {u}=\varnothing ↔{t}\left({A}\right)\cap {U}\left({A}\right)=\varnothing \right)$
10 id ${⊢}{u}={U}\left({A}\right)\to {u}={U}\left({A}\right)$
11 9 10 8 ifbieq12d ${⊢}{u}={U}\left({A}\right)\to if\left({t}\left({A}\right)\cap {u}=\varnothing ,{u},{t}\left({A}\right)\cap {u}\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)$
12 eqid ${⊢}\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)=\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)$
13 3 inex2 ${⊢}{t}\left({A}\right)\cap {U}\left({A}\right)\in \mathrm{V}$
14 3 13 ifex ${⊢}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)\in \mathrm{V}$
15 7 11 12 14 ovmpo ${⊢}\left({A}\in \mathrm{\omega }\wedge {U}\left({A}\right)\in \mathrm{V}\right)\to {A}\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){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)$
16 3 15 mpan2 ${⊢}{A}\in \mathrm{\omega }\to {A}\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){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)$
17 2 16 eqtrd ${⊢}{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)$