Theorem oiexg

Description: The order isomorphism on a set is a set. (Contributed by Mario Carneiro, 25-Jun-2015)

	Ref	Expression
Hypothesis	oicl.1	|- F = OrdIso ( R , A )
Assertion	oiexg	|- ( A e. V -> F e. _V )

Proof

Step	Hyp	Ref	Expression
1		oicl.1	|- F = OrdIso ( R , A )
2	1	ordtype	|- ( ( R We A /\ R Se A ) -> F Isom _E , R ( dom F , A ) )
3		isof1o	|- ( F Isom _E , R ( dom F , A ) -> F : dom F -1-1-onto-> A )
4		f1of1	|- ( F : dom F -1-1-onto-> A -> F : dom F -1-1-> A )
5	2 3 4	3syl	|- ( ( R We A /\ R Se A ) -> F : dom F -1-1-> A )
6		f1f	|- ( F : dom F -1-1-> A -> F : dom F --> A )
7		f1dmex	|- ( ( F : dom F -1-1-> A /\ A e. V ) -> dom F e. _V )
8		fex	|- ( ( F : dom F --> A /\ dom F e. _V ) -> F e. _V )
9	6 7 8	syl2an2r	|- ( ( F : dom F -1-1-> A /\ A e. V ) -> F e. _V )
10	9	expcom	|- ( A e. V -> ( F : dom F -1-1-> A -> F e. _V ) )
11	5 10	syl5	|- ( A e. V -> ( ( R We A /\ R Se A ) -> F e. _V ) )
12	1	oi0	|- ( -. ( R We A /\ R Se A ) -> F = (/) )
13		0ex	|- (/) e. _V
14	12 13	eqeltrdi	|- ( -. ( R We A /\ R Se A ) -> F e. _V )
15	11 14	pm2.61d1	|- ( A e. V -> F e. _V )