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 \leftrightarrow 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 \leftrightarrow 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)$$