Theorem ordtypelem5

Description: Lemma for ordtype . (Contributed by Mario Carneiro, 25-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	ordtypelem5	|- ( ph -> ( Ord dom O /\ O : dom O --> A ) )

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	1 2 3 4 5 6 7	ordtypelem2	|- ( ph -> Ord T )
9	1	tfr1a	|- ( Fun F /\ Lim dom F )
10	9	simpri	|- Lim dom F
11		limord	|- ( Lim dom F -> Ord dom F )
12	10 11	ax-mp	|- Ord dom F
13		ordin	|- ( ( Ord T /\ Ord dom F ) -> Ord ( T i^i dom F ) )
14	8 12 13	sylancl	|- ( ph -> Ord ( T i^i dom F ) )
15	1 2 3 4 5 6 7	ordtypelem4	|- ( ph -> O : ( T i^i dom F ) --> A )
16	15	fdmd	|- ( ph -> dom O = ( T i^i dom F ) )
17		ordeq	|- ( dom O = ( T i^i dom F ) -> ( Ord dom O <-> Ord ( T i^i dom F ) ) )
18	16 17	syl	|- ( ph -> ( Ord dom O <-> Ord ( T i^i dom F ) ) )
19	14 18	mpbird	|- ( ph -> Ord dom O )
20	15	ffdmd	|- ( ph -> O : dom O --> A )
21	19 20	jca	|- ( ph -> ( Ord dom O /\ O : dom O --> A ) )