Theorem ordtypelem1

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

	Ref	Expression
Hypotheses	ordtypelem.1	|- F = recs ( G )
	ordtypelem.2	|- C = { w e. A | A. j e. ran h j R w }
	ordtypelem.3	|- G = ( h e. _V |-> ( iota_ v e. C A. u e. C -. u R v ) )
	ordtypelem.5	|- T = { x e. On | E. t e. A A. z e. ( F " x ) z R t }
	ordtypelem.6	|- O = OrdIso ( R , A )
	ordtypelem.7	|- ( ph -> R We A )
	ordtypelem.8	|- ( ph -> R Se A )
Assertion	ordtypelem1	|- ( ph -> O = ( F |` T ) )

Proof

Step	Hyp	Ref	Expression
1		ordtypelem.1	|- F = recs ( G )
2		ordtypelem.2	|- C = { w e. A | A. j e. ran h j R w }
3		ordtypelem.3	|- G = ( h e. _V |-> ( iota_ v e. C A. u e. C -. u R v ) )
4		ordtypelem.5	|- T = { x e. On | E. t e. A A. z e. ( F " x ) z R t }
5		ordtypelem.6	|- O = OrdIso ( R , A )
6		ordtypelem.7	|- ( ph -> R We A )
7		ordtypelem.8	|- ( ph -> R Se A )
8		iftrue	|- ( ( R We A /\ R Se A ) -> if ( ( R We A /\ R Se A ) , ( F |` { x e. On | E. t e. A A. z e. ( F " x ) z R t } ) , (/) ) = ( F |` { x e. On | E. t e. A A. z e. ( F " x ) z R t } ) )
9	6 7 8	syl2anc	|- ( ph -> if ( ( R We A /\ R Se A ) , ( F |` { x e. On | E. t e. A A. z e. ( F " x ) z R t } ) , (/) ) = ( F |` { x e. On | E. t e. A A. z e. ( F " x ) z R t } ) )
10	2 3 1	dfoi	|- OrdIso ( R , A ) = if ( ( R We A /\ R Se A ) , ( F |` { x e. On | E. t e. A A. z e. ( F " x ) z R t } ) , (/) )
11	5 10	eqtri	|- O = if ( ( R We A /\ R Se A ) , ( F |` { x e. On | E. t e. A A. z e. ( F " x ) z R t } ) , (/) )
12	4	reseq2i	|- ( F |` T ) = ( F |` { x e. On | E. t e. A A. z e. ( F " x ) z R t } )
13	9 11 12	3eqtr4g	|- ( ph -> O = ( F |` T ) )