Metamath Proof Explorer


Theorem oif

Description: The order isomorphism of the well-order R on A is a function. (Contributed by Mario Carneiro, 23-May-2015)

Ref Expression
Hypothesis oicl.1 F = OrdIso R A
Assertion oif F : dom F A

Proof

Step Hyp Ref Expression
1 oicl.1 F = OrdIso R A
2 eqid recs h V ι v w A | j ran h j R w | u w A | j ran h j R w ¬ u R v = recs h V ι v w A | j ran h j R w | u w A | j ran h j R w ¬ u R v
3 eqid w A | j ran h j R w = w A | j ran h j R w
4 eqid h V ι v w A | j ran h j R w | u w A | j ran h j R w ¬ u R v = h V ι v w A | j ran h j R w | u w A | j ran h j R w ¬ u R v
5 2 3 4 ordtypecbv recs f V ι s y A | i ran f i R y | r y A | i ran f i R y ¬ r R s = recs h V ι v w A | j ran h j R w | u w A | j ran h j R w ¬ u R v
6 eqid x On | t A z recs f V ι s y A | i ran f i R y | r y A | i ran f i R y ¬ r R s x z R t = x On | t A z recs f V ι s y A | i ran f i R y | r y A | i ran f i R y ¬ r R s x z R t
7 simpl R We A R Se A R We A
8 simpr R We A R Se A R Se A
9 5 3 4 6 1 7 8 ordtypelem5 R We A R Se A Ord dom F F : dom F A
10 9 simprd R We A R Se A F : dom F A
11 f0 : A
12 1 oi0 ¬ R We A R Se A F =
13 12 dmeqd ¬ R We A R Se A dom F = dom
14 dm0 dom =
15 13 14 eqtrdi ¬ R We A R Se A dom F =
16 12 15 feq12d ¬ R We A R Se A F : dom F A : A
17 11 16 mpbiri ¬ R We A R Se A F : dom F A
18 10 17 pm2.61i F : dom F A