Theorem ordtypelem1

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	ordtypelem1	$$⊢\phi \to O={F\upharpoonright }_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		iftrue	$$⊢\left(R\mathrm{We}A\wedge R\mathrm{Se}A\right)\to if\left(\left(R\mathrm{We}A\wedge R\mathrm{Se}A\right),{F\upharpoonright }_{\left\{x\in \mathrm{On}|\exists t\in A\forall z\in F\left[x\right]zRt\right\}},\varnothing \right)={F\upharpoonright }_{\left\{x\in \mathrm{On}|\exists t\in A\forall z\in F\left[x\right]zRt\right\}}$$
9	6 7 8	syl2anc	$$⊢\phi \to if\left(\left(R\mathrm{We}A\wedge R\mathrm{Se}A\right),{F\upharpoonright }_{\left\{x\in \mathrm{On}|\exists t\in A\forall z\in F\left[x\right]zRt\right\}},\varnothing \right)={F\upharpoonright }_{\left\{x\in \mathrm{On}|\exists t\in A\forall z\in F\left[x\right]zRt\right\}}$$
10	2 3 1	dfoi	$$⊢OrdIso\left(R,A\right)=if\left(\left(R\mathrm{We}A\wedge R\mathrm{Se}A\right),{F\upharpoonright }_{\left\{x\in \mathrm{On}|\exists t\in A\forall z\in F\left[x\right]zRt\right\}},\varnothing \right)$$
11	5 10	eqtri	$$⊢O=if\left(\left(R\mathrm{We}A\wedge R\mathrm{Se}A\right),{F\upharpoonright }_{\left\{x\in \mathrm{On}|\exists t\in A\forall z\in F\left[x\right]zRt\right\}},\varnothing \right)$$
12	4	reseq2i	$$⊢{F\upharpoonright }_T={F\upharpoonright }_{\left\{x\in \mathrm{On}|\exists t\in A\forall z\in F\left[x\right]zRt\right\}}$$
13	9 11 12	3eqtr4g	$$⊢\phi \to O={F\upharpoonright }_T$$