Metamath Proof Explorer


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 )