Theorem ordtypelem2

Description: Lemma for ordtype . (Contributed by Mario Carneiro, 24-Jun-2015)

	Ref	Expression
Hypotheses	ordtypelem.1	$$⊢F=\mathrm{recs}\left(G\right)$$
	ordtypelem.2	$$⊢C=\left\{w\in A|\forall j\in \mathrm{ran}hjRw\right\}$$
	ordtypelem.3	$$⊢G=\left(h\in \mathrm{V}⟼\left(\iota v\in C|\forall u\in C\neg uRv\right)\right)$$
	ordtypelem.5	$$⊢T=\left\{x\in \mathrm{On}|\exists t\in A\forall z\in F\left[x\right]zRt\right\}$$
	ordtypelem.6	$$⊢O=OrdIso\left(R,A\right)$$
	ordtypelem.7	$$⊢\phi \to R\mathrm{We}A$$
	ordtypelem.8	$$⊢\phi \to R\mathrm{Se}A$$
Assertion	ordtypelem2	$$⊢\phi \to \mathrm{Ord}T$$

Proof

Step	Hyp	Ref	Expression
1		ordtypelem.1	$$⊢F=\mathrm{recs}\left(G\right)$$
2		ordtypelem.2	$$⊢C=\left\{w\in A|\forall j\in \mathrm{ran}hjRw\right\}$$
3		ordtypelem.3	$$⊢G=\left(h\in \mathrm{V}⟼\left(\iota v\in C|\forall u\in C\neg uRv\right)\right)$$
4		ordtypelem.5	$$⊢T=\left\{x\in \mathrm{On}|\exists t\in A\forall z\in F\left[x\right]zRt\right\}$$
5		ordtypelem.6	$$⊢O=OrdIso\left(R,A\right)$$
6		ordtypelem.7	$$⊢\phi \to R\mathrm{We}A$$
7		ordtypelem.8	$$⊢\phi \to R\mathrm{Se}A$$
8	4	ssrab3	$$⊢T\subseteq \mathrm{On}$$
9	8	a1i	$$⊢\phi \to T\subseteq \mathrm{On}$$
10	9	sselda	$$⊢\left(\phi \wedge a\in T\right)\to a\in \mathrm{On}$$
11		onss	$$⊢a\in \mathrm{On}\to a\subseteq \mathrm{On}$$
12	10 11	syl	$$⊢\left(\phi \wedge a\in T\right)\to a\subseteq \mathrm{On}$$
13		eloni	$$⊢a\in \mathrm{On}\to \mathrm{Ord}a$$
14	10 13	syl	$$⊢\left(\phi \wedge a\in T\right)\to \mathrm{Ord}a$$
15		imaeq2	$$⊢x=a\to F\left[x\right]=F\left[a\right]$$
16	15	raleqdv	$$⊢x=a\to \left(\forall z\in F\left[x\right]zRt\leftrightarrow \forall z\in F\left[a\right]zRt\right)$$
17	16	rexbidv	$$⊢x=a\to \left(\exists t\in A\forall z\in F\left[x\right]zRt\leftrightarrow \exists t\in A\forall z\in F\left[a\right]zRt\right)$$
18	17 4	elrab2	$$⊢a\in T\leftrightarrow \left(a\in \mathrm{On}\wedge \exists t\in A\forall z\in F\left[a\right]zRt\right)$$
19	18	simprbi	$$⊢a\in T\to \exists t\in A\forall z\in F\left[a\right]zRt$$
20	19	adantl	$$⊢\left(\phi \wedge a\in T\right)\to \exists t\in A\forall z\in F\left[a\right]zRt$$
21		ordelss	$$⊢\left(\mathrm{Ord}a\wedge x\in a\right)\to x\subseteq a$$
22		imass2	$$⊢x\subseteq a\to F\left[x\right]\subseteq F\left[a\right]$$
23		ssralv	$$⊢F\left[x\right]\subseteq F\left[a\right]\to \left(\forall z\in F\left[a\right]zRt\to \forall z\in F\left[x\right]zRt\right)$$
24	23	reximdv	$$⊢F\left[x\right]\subseteq F\left[a\right]\to \left(\exists t\in A\forall z\in F\left[a\right]zRt\to \exists t\in A\forall z\in F\left[x\right]zRt\right)$$
25	21 22 24	3syl	$$⊢\left(\mathrm{Ord}a\wedge x\in a\right)\to \left(\exists t\in A\forall z\in F\left[a\right]zRt\to \exists t\in A\forall z\in F\left[x\right]zRt\right)$$
26	25	ralrimdva	$$⊢\mathrm{Ord}a\to \left(\exists t\in A\forall z\in F\left[a\right]zRt\to \forall x\in a\exists t\in A\forall z\in F\left[x\right]zRt\right)$$
27	14 20 26	sylc	$$⊢\left(\phi \wedge a\in T\right)\to \forall x\in a\exists t\in A\forall z\in F\left[x\right]zRt$$
28		ssrab	$$⊢a\subseteq \left\{x\in \mathrm{On}|\exists t\in A\forall z\in F\left[x\right]zRt\right\}\leftrightarrow \left(a\subseteq \mathrm{On}\wedge \forall x\in a\exists t\in A\forall z\in F\left[x\right]zRt\right)$$
29	12 27 28	sylanbrc	$$⊢\left(\phi \wedge a\in T\right)\to a\subseteq \left\{x\in \mathrm{On}|\exists t\in A\forall z\in F\left[x\right]zRt\right\}$$
30	29 4	sseqtrrdi	$$⊢\left(\phi \wedge a\in T\right)\to a\subseteq T$$
31	30	ralrimiva	$$⊢\phi \to \forall a\in Ta\subseteq T$$
32		dftr3	$$⊢\mathrm{Tr}T\leftrightarrow \forall a\in Ta\subseteq T$$
33	31 32	sylibr	$$⊢\phi \to \mathrm{Tr}T$$
34		ordon	$$⊢\mathrm{Ord}\mathrm{On}$$
35		trssord	$$⊢\left(\mathrm{Tr}T\wedge T\subseteq \mathrm{On}\wedge \mathrm{Ord}\mathrm{On}\right)\to \mathrm{Ord}T$$
36	8 34 35	mp3an23	$$⊢\mathrm{Tr}T\to \mathrm{Ord}T$$
37	33 36	syl	$$⊢\phi \to \mathrm{Ord}T$$