Theorem 1stcrestlem

Description: Lemma for 1stcrest . (Contributed by Mario Carneiro, 21-Mar-2015) (Revised by Mario Carneiro, 30-Apr-2015)

	Ref	Expression
Assertion	1stcrestlem	|- ( B ~<_ _om -> ran ( x e. B |-> C ) ~<_ _om )

Proof

Step	Hyp	Ref	Expression
1		ordom	|- Ord _om
2		reldom	|- Rel ~<_
3	2	brrelex2i	|- ( B ~<_ _om -> _om e. _V )
4		elong	|- ( _om e. _V -> ( _om e. On <-> Ord _om ) )
5	3 4	syl	|- ( B ~<_ _om -> ( _om e. On <-> Ord _om ) )
6	1 5	mpbiri	|- ( B ~<_ _om -> _om e. On )
7		ondomen	|- ( ( _om e. On /\ B ~<_ _om ) -> B e. dom card )
8	6 7	mpancom	|- ( B ~<_ _om -> B e. dom card )
9		eqid	|- ( x e. B |-> C ) = ( x e. B |-> C )
10	9	dmmptss	|- dom ( x e. B |-> C ) C_ B
11		ssnum	|- ( ( B e. dom card /\ dom ( x e. B |-> C ) C_ B ) -> dom ( x e. B |-> C ) e. dom card )
12	8 10 11	sylancl	|- ( B ~<_ _om -> dom ( x e. B |-> C ) e. dom card )
13		funmpt	|- Fun ( x e. B |-> C )
14		funforn	|- ( Fun ( x e. B |-> C ) <-> ( x e. B |-> C ) : dom ( x e. B |-> C ) -onto-> ran ( x e. B |-> C ) )
15	13 14	mpbi	|- ( x e. B |-> C ) : dom ( x e. B |-> C ) -onto-> ran ( x e. B |-> C )
16		fodomnum	|- ( dom ( x e. B |-> C ) e. dom card -> ( ( x e. B |-> C ) : dom ( x e. B |-> C ) -onto-> ran ( x e. B |-> C ) -> ran ( x e. B |-> C ) ~<_ dom ( x e. B |-> C ) ) )
17	12 15 16	mpisyl	|- ( B ~<_ _om -> ran ( x e. B |-> C ) ~<_ dom ( x e. B |-> C ) )
18		ctex	|- ( B ~<_ _om -> B e. _V )
19		ssdomg	|- ( B e. _V -> ( dom ( x e. B |-> C ) C_ B -> dom ( x e. B |-> C ) ~<_ B ) )
20	18 10 19	mpisyl	|- ( B ~<_ _om -> dom ( x e. B |-> C ) ~<_ B )
21		domtr	|- ( ( dom ( x e. B |-> C ) ~<_ B /\ B ~<_ _om ) -> dom ( x e. B |-> C ) ~<_ _om )
22	20 21	mpancom	|- ( B ~<_ _om -> dom ( x e. B |-> C ) ~<_ _om )
23		domtr	|- ( ( ran ( x e. B |-> C ) ~<_ dom ( x e. B |-> C ) /\ dom ( x e. B |-> C ) ~<_ _om ) -> ran ( x e. B |-> C ) ~<_ _om )
24	17 22 23	syl2anc	|- ( B ~<_ _om -> ran ( x e. B |-> C ) ~<_ _om )