Theorem fin23lem35

Description: Lemma for fin23 . Strict order property of Y . (Contributed by Stefan O'Rear, 2-Nov-2014)

	Ref	Expression
Hypotheses	fin23lem33.f	$$⊢F=\left\{g|\forall a\in \left({𝒫g}^{\mathrm{\omega }}\right)\left(\forall x\in \mathrm{\omega }a\left(\mathrm{suc}x\right)\subseteq a\left(x\right)\to \bigcap \mathrm{ran}a\in \mathrm{ran}a\right)\right\}$$
	fin23lem.f	$$⊢\phi \to h:\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}$$
	fin23lem.g	$$⊢\phi \to \bigcup \mathrm{ran}h\subseteq G$$
	fin23lem.h	$$⊢\phi \to \forall j\left(\left(j:\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}\wedge \bigcup \mathrm{ran}j\subseteq G\right)\to \left(i\left(j\right):\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}\wedge \bigcup \mathrm{ran}i\left(j\right)\subset \bigcup \mathrm{ran}j\right)\right)$$
	fin23lem.i	$$⊢Y={\mathrm{rec}\left(i,h\right)\upharpoonright }_{\mathrm{\omega }}$$
Assertion	fin23lem35	$$⊢\left(\phi \wedge A\in \mathrm{\omega }\right)\to \bigcup \mathrm{ran}Y\left(\mathrm{suc}A\right)\subset \bigcup \mathrm{ran}Y\left(A\right)$$

Proof

Step	Hyp	Ref	Expression
1		fin23lem33.f	$$⊢F=\left\{g|\forall a\in \left({𝒫g}^{\mathrm{\omega }}\right)\left(\forall x\in \mathrm{\omega }a\left(\mathrm{suc}x\right)\subseteq a\left(x\right)\to \bigcap \mathrm{ran}a\in \mathrm{ran}a\right)\right\}$$
2		fin23lem.f	$$⊢\phi \to h:\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}$$
3		fin23lem.g	$$⊢\phi \to \bigcup \mathrm{ran}h\subseteq G$$
4		fin23lem.h	$$⊢\phi \to \forall j\left(\left(j:\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}\wedge \bigcup \mathrm{ran}j\subseteq G\right)\to \left(i\left(j\right):\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}\wedge \bigcup \mathrm{ran}i\left(j\right)\subset \bigcup \mathrm{ran}j\right)\right)$$
5		fin23lem.i	$$⊢Y={\mathrm{rec}\left(i,h\right)\upharpoonright }_{\mathrm{\omega }}$$
6	1 2 3 4 5	fin23lem34	$$⊢\left(\phi \wedge A\in \mathrm{\omega }\right)\to \left(Y\left(A\right):\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}\wedge \bigcup \mathrm{ran}Y\left(A\right)\subseteq G\right)$$
7		fvex	$$⊢Y\left(A\right)\in \mathrm{V}$$
8		f1eq1	$$⊢j=Y\left(A\right)\to \left(j:\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}\leftrightarrow Y\left(A\right):\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}\right)$$
9		rneq	$$⊢j=Y\left(A\right)\to \mathrm{ran}j=\mathrm{ran}Y\left(A\right)$$
10	9	unieqd	$$⊢j=Y\left(A\right)\to \bigcup \mathrm{ran}j=\bigcup \mathrm{ran}Y\left(A\right)$$
11	10	sseq1d	$$⊢j=Y\left(A\right)\to \left(\bigcup \mathrm{ran}j\subseteq G\leftrightarrow \bigcup \mathrm{ran}Y\left(A\right)\subseteq G\right)$$
12	8 11	anbi12d	$$⊢j=Y\left(A\right)\to \left(\left(j:\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}\wedge \bigcup \mathrm{ran}j\subseteq G\right)\leftrightarrow \left(Y\left(A\right):\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}\wedge \bigcup \mathrm{ran}Y\left(A\right)\subseteq G\right)\right)$$
13		fveq2	$$⊢j=Y\left(A\right)\to i\left(j\right)=i\left(Y\left(A\right)\right)$$
14		f1eq1	$$⊢i\left(j\right)=i\left(Y\left(A\right)\right)\to \left(i\left(j\right):\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}\leftrightarrow i\left(Y\left(A\right)\right):\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}\right)$$
15	13 14	syl	$$⊢j=Y\left(A\right)\to \left(i\left(j\right):\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}\leftrightarrow i\left(Y\left(A\right)\right):\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}\right)$$
16	13	rneqd	$$⊢j=Y\left(A\right)\to \mathrm{ran}i\left(j\right)=\mathrm{ran}i\left(Y\left(A\right)\right)$$
17	16	unieqd	$$⊢j=Y\left(A\right)\to \bigcup \mathrm{ran}i\left(j\right)=\bigcup \mathrm{ran}i\left(Y\left(A\right)\right)$$
18	17 10	psseq12d	$$⊢j=Y\left(A\right)\to \left(\bigcup \mathrm{ran}i\left(j\right)\subset \bigcup \mathrm{ran}j\leftrightarrow \bigcup \mathrm{ran}i\left(Y\left(A\right)\right)\subset \bigcup \mathrm{ran}Y\left(A\right)\right)$$
19	15 18	anbi12d	$$⊢j=Y\left(A\right)\to \left(\left(i\left(j\right):\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}\wedge \bigcup \mathrm{ran}i\left(j\right)\subset \bigcup \mathrm{ran}j\right)\leftrightarrow \left(i\left(Y\left(A\right)\right):\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}\wedge \bigcup \mathrm{ran}i\left(Y\left(A\right)\right)\subset \bigcup \mathrm{ran}Y\left(A\right)\right)\right)$$
20	12 19	imbi12d	$$⊢j=Y\left(A\right)\to \left(\left(\left(j:\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}\wedge \bigcup \mathrm{ran}j\subseteq G\right)\to \left(i\left(j\right):\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}\wedge \bigcup \mathrm{ran}i\left(j\right)\subset \bigcup \mathrm{ran}j\right)\right)\leftrightarrow \left(\left(Y\left(A\right):\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}\wedge \bigcup \mathrm{ran}Y\left(A\right)\subseteq G\right)\to \left(i\left(Y\left(A\right)\right):\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}\wedge \bigcup \mathrm{ran}i\left(Y\left(A\right)\right)\subset \bigcup \mathrm{ran}Y\left(A\right)\right)\right)\right)$$
21	7 20	spcv	$$⊢\forall j\left(\left(j:\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}\wedge \bigcup \mathrm{ran}j\subseteq G\right)\to \left(i\left(j\right):\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}\wedge \bigcup \mathrm{ran}i\left(j\right)\subset \bigcup \mathrm{ran}j\right)\right)\to \left(\left(Y\left(A\right):\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}\wedge \bigcup \mathrm{ran}Y\left(A\right)\subseteq G\right)\to \left(i\left(Y\left(A\right)\right):\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}\wedge \bigcup \mathrm{ran}i\left(Y\left(A\right)\right)\subset \bigcup \mathrm{ran}Y\left(A\right)\right)\right)$$
22	4 21	syl	$$⊢\phi \to \left(\left(Y\left(A\right):\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}\wedge \bigcup \mathrm{ran}Y\left(A\right)\subseteq G\right)\to \left(i\left(Y\left(A\right)\right):\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}\wedge \bigcup \mathrm{ran}i\left(Y\left(A\right)\right)\subset \bigcup \mathrm{ran}Y\left(A\right)\right)\right)$$
23	22	adantr	$$⊢\left(\phi \wedge A\in \mathrm{\omega }\right)\to \left(\left(Y\left(A\right):\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}\wedge \bigcup \mathrm{ran}Y\left(A\right)\subseteq G\right)\to \left(i\left(Y\left(A\right)\right):\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}\wedge \bigcup \mathrm{ran}i\left(Y\left(A\right)\right)\subset \bigcup \mathrm{ran}Y\left(A\right)\right)\right)$$
24	6 23	mpd	$$⊢\left(\phi \wedge A\in \mathrm{\omega }\right)\to \left(i\left(Y\left(A\right)\right):\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}\wedge \bigcup \mathrm{ran}i\left(Y\left(A\right)\right)\subset \bigcup \mathrm{ran}Y\left(A\right)\right)$$
25	24	simprd	$$⊢\left(\phi \wedge A\in \mathrm{\omega }\right)\to \bigcup \mathrm{ran}i\left(Y\left(A\right)\right)\subset \bigcup \mathrm{ran}Y\left(A\right)$$
26		frsuc	$$⊢A\in \mathrm{\omega }\to \left({\mathrm{rec}\left(i,h\right)\upharpoonright }_{\mathrm{\omega }}\right)\left(\mathrm{suc}A\right)=i\left(\left({\mathrm{rec}\left(i,h\right)\upharpoonright }_{\mathrm{\omega }}\right)\left(A\right)\right)$$
27	26	adantl	$$⊢\left(\phi \wedge A\in \mathrm{\omega }\right)\to \left({\mathrm{rec}\left(i,h\right)\upharpoonright }_{\mathrm{\omega }}\right)\left(\mathrm{suc}A\right)=i\left(\left({\mathrm{rec}\left(i,h\right)\upharpoonright }_{\mathrm{\omega }}\right)\left(A\right)\right)$$
28	5	fveq1i	$$⊢Y\left(\mathrm{suc}A\right)=\left({\mathrm{rec}\left(i,h\right)\upharpoonright }_{\mathrm{\omega }}\right)\left(\mathrm{suc}A\right)$$
29	5	fveq1i	$$⊢Y\left(A\right)=\left({\mathrm{rec}\left(i,h\right)\upharpoonright }_{\mathrm{\omega }}\right)\left(A\right)$$
30	29	fveq2i	$$⊢i\left(Y\left(A\right)\right)=i\left(\left({\mathrm{rec}\left(i,h\right)\upharpoonright }_{\mathrm{\omega }}\right)\left(A\right)\right)$$
31	27 28 30	3eqtr4g	$$⊢\left(\phi \wedge A\in \mathrm{\omega }\right)\to Y\left(\mathrm{suc}A\right)=i\left(Y\left(A\right)\right)$$
32	31	rneqd	$$⊢\left(\phi \wedge A\in \mathrm{\omega }\right)\to \mathrm{ran}Y\left(\mathrm{suc}A\right)=\mathrm{ran}i\left(Y\left(A\right)\right)$$
33	32	unieqd	$$⊢\left(\phi \wedge A\in \mathrm{\omega }\right)\to \bigcup \mathrm{ran}Y\left(\mathrm{suc}A\right)=\bigcup \mathrm{ran}i\left(Y\left(A\right)\right)$$
34	33	psseq1d	$$⊢\left(\phi \wedge A\in \mathrm{\omega }\right)\to \left(\bigcup \mathrm{ran}Y\left(\mathrm{suc}A\right)\subset \bigcup \mathrm{ran}Y\left(A\right)\leftrightarrow \bigcup \mathrm{ran}i\left(Y\left(A\right)\right)\subset \bigcup \mathrm{ran}Y\left(A\right)\right)$$
35	25 34	mpbird	$$⊢\left(\phi \wedge A\in \mathrm{\omega }\right)\to \bigcup \mathrm{ran}Y\left(\mathrm{suc}A\right)\subset \bigcup \mathrm{ran}Y\left(A\right)$$