Metamath Proof Explorer

Theorem oismo

Description: When A is a subclass of On , F is a strictly monotone ordinal functions, and it is also complete (it is an isomorphism onto all of A ). The proof avoids ax-rep (the second statement is trivial under ax-rep ). (Contributed by Mario Carneiro, 26-Jun-2015)

Ref Expression
Hypothesis oismo.1 
|- F = OrdIso ( _E , A )
Assertion oismo 
|- ( A C_ On -> ( Smo F /\ ran F = A ) )

Proof

Step Hyp Ref Expression
1 oismo.1 
 |-  F = OrdIso ( _E , A )
2 epweon 
 |-  _E We On
3 wess 
 |-  ( A C_ On -> ( _E We On -> _E We A ) )
4 2 3 mpi 
 |-  ( A C_ On -> _E We A )
5 epse 
 |-  _E Se A
6 1 oiiso2 
 |-  ( ( _E We A /\ _E Se A ) -> F Isom _E , _E ( dom F , ran F ) )
7 4 5 6 sylancl 
 |-  ( A C_ On -> F Isom _E , _E ( dom F , ran F ) )
8 1 oicl 
 |-  Ord dom F
9 1 oif 
 |-  F : dom F --> A
10 frn 
 |-  ( F : dom F --> A -> ran F C_ A )
11 9 10 ax-mp 
 |-  ran F C_ A
12 id 
 |-  ( A C_ On -> A C_ On )
13 11 12 sstrid 
 |-  ( A C_ On -> ran F C_ On )
14 smoiso2 
 |-  ( ( Ord dom F /\ ran F C_ On ) -> ( ( F : dom F -onto-> ran F /\ Smo F ) <-> F Isom _E , _E ( dom F , ran F ) ) )
15 8 13 14 sylancr 
 |-  ( A C_ On -> ( ( F : dom F -onto-> ran F /\ Smo F ) <-> F Isom _E , _E ( dom F , ran F ) ) )
16 7 15 mpbird 
 |-  ( A C_ On -> ( F : dom F -onto-> ran F /\ Smo F ) )
17 16 simprd 
 |-  ( A C_ On -> Smo F )
18 11 a1i 
 |-  ( A C_ On -> ran F C_ A )
19 simprl 
 |-  ( ( A C_ On /\ ( x e. A /\ -. x e. ran F ) ) -> x e. A )
20 4 adantr 
 |-  ( ( A C_ On /\ ( x e. A /\ -. x e. ran F ) ) -> _E We A )
21 5 a1i 
 |-  ( ( A C_ On /\ ( x e. A /\ -. x e. ran F ) ) -> _E Se A )
22 ffn 
 |-  ( F : dom F --> A -> F Fn dom F )
23 9 22 mp1i 
 |-  ( ( A C_ On /\ ( x e. A /\ -. x e. ran F ) ) -> F Fn dom F )
24 simplrr 
 |-  ( ( ( A C_ On /\ ( x e. A /\ -. x e. ran F ) ) /\ y e. dom F ) -> -. x e. ran F )
25 4 ad2antrr 
 |-  ( ( ( A C_ On /\ ( x e. A /\ -. x e. ran F ) ) /\ y e. dom F ) -> _E We A )
26 5 a1i 
 |-  ( ( ( A C_ On /\ ( x e. A /\ -. x e. ran F ) ) /\ y e. dom F ) -> _E Se A )
27 simplrl 
 |-  ( ( ( A C_ On /\ ( x e. A /\ -. x e. ran F ) ) /\ y e. dom F ) -> x e. A )
28 simpr 
 |-  ( ( ( A C_ On /\ ( x e. A /\ -. x e. ran F ) ) /\ y e. dom F ) -> y e. dom F )
29 1 oiiniseg 
 |-  ( ( ( _E We A /\ _E Se A ) /\ ( x e. A /\ y e. dom F ) ) -> ( ( F ` y ) _E x \/ x e. ran F ) )
30 25 26 27 28 29 syl22anc 
 |-  ( ( ( A C_ On /\ ( x e. A /\ -. x e. ran F ) ) /\ y e. dom F ) -> ( ( F ` y ) _E x \/ x e. ran F ) )
31 30 ord 
 |-  ( ( ( A C_ On /\ ( x e. A /\ -. x e. ran F ) ) /\ y e. dom F ) -> ( -. ( F ` y ) _E x -> x e. ran F ) )
32 24 31 mt3d 
 |-  ( ( ( A C_ On /\ ( x e. A /\ -. x e. ran F ) ) /\ y e. dom F ) -> ( F ` y ) _E x )
33 epel 
 |-  ( ( F ` y ) _E x <-> ( F ` y ) e. x )
34 32 33 sylib 
 |-  ( ( ( A C_ On /\ ( x e. A /\ -. x e. ran F ) ) /\ y e. dom F ) -> ( F ` y ) e. x )
35 34 ralrimiva 
 |-  ( ( A C_ On /\ ( x e. A /\ -. x e. ran F ) ) -> A. y e. dom F ( F ` y ) e. x )
36 ffnfv 
 |-  ( F : dom F --> x <-> ( F Fn dom F /\ A. y e. dom F ( F ` y ) e. x ) )
37 23 35 36 sylanbrc 
 |-  ( ( A C_ On /\ ( x e. A /\ -. x e. ran F ) ) -> F : dom F --> x )
38 9 22 mp1i 
 |-  ( ( ( A C_ On /\ ( x e. A /\ -. x e. ran F ) ) /\ y e. dom F ) -> F Fn dom F )
39 17 ad2antrr 
 |-  ( ( ( A C_ On /\ ( x e. A /\ -. x e. ran F ) ) /\ y e. dom F ) -> Smo F )
40 smogt 
 |-  ( ( F Fn dom F /\ Smo F /\ y e. dom F ) -> y C_ ( F ` y ) )
41 38 39 28 40 syl3anc 
 |-  ( ( ( A C_ On /\ ( x e. A /\ -. x e. ran F ) ) /\ y e. dom F ) -> y C_ ( F ` y ) )
42 ordelon 
 |-  ( ( Ord dom F /\ y e. dom F ) -> y e. On )
43 8 28 42 sylancr 
 |-  ( ( ( A C_ On /\ ( x e. A /\ -. x e. ran F ) ) /\ y e. dom F ) -> y e. On )
44 simpll 
 |-  ( ( ( A C_ On /\ ( x e. A /\ -. x e. ran F ) ) /\ y e. dom F ) -> A C_ On )
45 44 27 sseldd 
 |-  ( ( ( A C_ On /\ ( x e. A /\ -. x e. ran F ) ) /\ y e. dom F ) -> x e. On )
46 ontr2 
 |-  ( ( y e. On /\ x e. On ) -> ( ( y C_ ( F ` y ) /\ ( F ` y ) e. x ) -> y e. x ) )
47 43 45 46 syl2anc 
 |-  ( ( ( A C_ On /\ ( x e. A /\ -. x e. ran F ) ) /\ y e. dom F ) -> ( ( y C_ ( F ` y ) /\ ( F ` y ) e. x ) -> y e. x ) )
48 41 34 47 mp2and 
 |-  ( ( ( A C_ On /\ ( x e. A /\ -. x e. ran F ) ) /\ y e. dom F ) -> y e. x )
49 48 ex 
 |-  ( ( A C_ On /\ ( x e. A /\ -. x e. ran F ) ) -> ( y e. dom F -> y e. x ) )
50 49 ssrdv 
 |-  ( ( A C_ On /\ ( x e. A /\ -. x e. ran F ) ) -> dom F C_ x )
51 19 50 ssexd 
 |-  ( ( A C_ On /\ ( x e. A /\ -. x e. ran F ) ) -> dom F e. _V )
52 fex2 
 |-  ( ( F : dom F --> x /\ dom F e. _V /\ x e. A ) -> F e. _V )
53 37 51 19 52 syl3anc 
 |-  ( ( A C_ On /\ ( x e. A /\ -. x e. ran F ) ) -> F e. _V )
54 1 ordtype2 
 |-  ( ( _E We A /\ _E Se A /\ F e. _V ) -> F Isom _E , _E ( dom F , A ) )
55 20 21 53 54 syl3anc 
 |-  ( ( A C_ On /\ ( x e. A /\ -. x e. ran F ) ) -> F Isom _E , _E ( dom F , A ) )
56 isof1o 
 |-  ( F Isom _E , _E ( dom F , A ) -> F : dom F -1-1-onto-> A )
57 f1ofo 
 |-  ( F : dom F -1-1-onto-> A -> F : dom F -onto-> A )
58 forn 
 |-  ( F : dom F -onto-> A -> ran F = A )
59 55 56 57 58 4syl 
 |-  ( ( A C_ On /\ ( x e. A /\ -. x e. ran F ) ) -> ran F = A )
60 19 59 eleqtrrd 
 |-  ( ( A C_ On /\ ( x e. A /\ -. x e. ran F ) ) -> x e. ran F )
61 60 expr 
 |-  ( ( A C_ On /\ x e. A ) -> ( -. x e. ran F -> x e. ran F ) )
62 61 pm2.18d 
 |-  ( ( A C_ On /\ x e. A ) -> x e. ran F )
63 18 62 eqelssd 
 |-  ( A C_ On -> ran F = A )
64 17 63 jca 
 |-  ( A C_ On -> ( Smo F /\ ran F = A ) )