This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )