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 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 On E We On E We A
4 2 3 mpi A 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 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 A
11 9 10 ax-mp ran F A
12 id A On A On
13 11 12 sstrid A On ran F On
14 smoiso2 Ord dom F ran F On F : dom F onto ran F Smo F F Isom E , E dom F ran F
15 8 13 14 sylancr A On F : dom F onto ran F Smo F F Isom E , E dom F ran F
16 7 15 mpbird A On F : dom F onto ran F Smo F
17 16 simprd A On Smo F
18 11 a1i A On ran F A
19 simprl A On x A ¬ x ran F x A
20 4 adantr A On x A ¬ x ran F E We A
21 5 a1i A On x A ¬ x ran F E Se A
22 ffn F : dom F A F Fn dom F
23 9 22 mp1i A On x A ¬ x ran F F Fn dom F
24 simplrr A On x A ¬ x ran F y dom F ¬ x ran F
25 4 ad2antrr A On x A ¬ x ran F y dom F E We A
26 5 a1i A On x A ¬ x ran F y dom F E Se A
27 simplrl A On x A ¬ x ran F y dom F x A
28 simpr A On x A ¬ x ran F y dom F y dom F
29 1 oiiniseg E We A E Se A x A y dom F F y E x x ran F
30 25 26 27 28 29 syl22anc A On x A ¬ x ran F y dom F F y E x x ran F
31 30 ord A On x A ¬ x ran F y dom F ¬ F y E x x ran F
32 24 31 mt3d A On x A ¬ x ran F y dom F F y E x
33 epel F y E x F y x
34 32 33 sylib A On x A ¬ x ran F y dom F F y x
35 34 ralrimiva A On x A ¬ x ran F y dom F F y x
36 ffnfv F : dom F x F Fn dom F y dom F F y x
37 23 35 36 sylanbrc A On x A ¬ x ran F F : dom F x
38 9 22 mp1i A On x A ¬ x ran F y dom F F Fn dom F
39 17 ad2antrr A On x A ¬ x ran F y dom F Smo F
40 smogt F Fn dom F Smo F y dom F y F y
41 38 39 28 40 syl3anc A On x A ¬ x ran F y dom F y F y
42 ordelon Ord dom F y dom F y On
43 8 28 42 sylancr A On x A ¬ x ran F y dom F y On
44 simpll A On x A ¬ x ran F y dom F A On
45 44 27 sseldd A On x A ¬ x ran F y dom F x On
46 ontr2 y On x On y F y F y x y x
47 43 45 46 syl2anc A On x A ¬ x ran F y dom F y F y F y x y x
48 41 34 47 mp2and A On x A ¬ x ran F y dom F y x
49 48 ex A On x A ¬ x ran F y dom F y x
50 49 ssrdv A On x A ¬ x ran F dom F x
51 19 50 ssexd A On x A ¬ x ran F dom F V
52 fex2 F : dom F x dom F V x A F V
53 37 51 19 52 syl3anc A On x A ¬ x ran F F V
54 1 ordtype2 E We A E Se A F V F Isom E , E dom F A
55 20 21 53 54 syl3anc A On x A ¬ x 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 On x A ¬ x ran F ran F = A
60 19 59 eleqtrrd A On x A ¬ x ran F x ran F
61 60 expr A On x A ¬ x ran F x ran F
62 61 pm2.18d A On x A x ran F
63 18 62 eqelssd A On ran F = A
64 17 63 jca A On Smo F ran F = A