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=OrdIsoRA
Assertion oif ⊢F:dom⁡F⟶A

Proof

Step Hyp Ref Expression
1 oicl.1 ⊢F=OrdIsoRA
2 eqid ⊢recs⁡h∈V⟼ιv∈w∈A|∀j∈ran⁡hjRw|∀u∈w∈A|∀j∈ran⁡hjRw¬uRv=recs⁡h∈V⟼ιv∈w∈A|∀j∈ran⁡hjRw|∀u∈w∈A|∀j∈ran⁡hjRw¬uRv
3 eqid ⊢w∈A|∀j∈ran⁡hjRw=w∈A|∀j∈ran⁡hjRw
4 eqid ⊢h∈V⟼ιv∈w∈A|∀j∈ran⁡hjRw|∀u∈w∈A|∀j∈ran⁡hjRw¬uRv=h∈V⟼ιv∈w∈A|∀j∈ran⁡hjRw|∀u∈w∈A|∀j∈ran⁡hjRw¬uRv
5 2 3 4 ordtypecbv ⊢recs⁡f∈V⟼ιs∈y∈A|∀i∈ran⁡fiRy|∀r∈y∈A|∀i∈ran⁡fiRy¬rRs=recs⁡h∈V⟼ιv∈w∈A|∀j∈ran⁡hjRw|∀u∈w∈A|∀j∈ran⁡hjRw¬uRv
6 eqid ⊢x∈On|∃t∈A∀z∈recs⁡f∈V⟼ιs∈y∈A|∀i∈ran⁡fiRy|∀r∈y∈A|∀i∈ran⁡fiRy¬rRsxzRt=x∈On|∃t∈A∀z∈recs⁡f∈V⟼ιs∈y∈A|∀i∈ran⁡fiRy|∀r∈y∈A|∀i∈ran⁡fiRy¬rRsxzRt
7 simpl ⊢RWeA∧RSeA→RWeA
8 simpr ⊢RWeA∧RSeA→RSeA
9 5 3 4 6 1 7 8 ordtypelem5 ⊢RWeA∧RSeA→Ord⁡dom⁡F∧F:dom⁡F⟶A
10 9 simprd ⊢RWeA∧RSeA→F:dom⁡F⟶A
11 f0 ⊢∅:∅⟶A
12 1 oi0 ⊢¬RWeA∧RSeA→F=∅
13 12 dmeqd ⊢¬RWeA∧RSeA→dom⁡F=dom⁡∅
14 dm0 ⊢dom⁡∅=∅
15 13 14 eqtrdi ⊢¬RWeA∧RSeA→dom⁡F=∅
16 12 15 feq12d ⊢¬RWeA∧RSeA→F:dom⁡F⟶A↔∅:∅⟶A
17 11 16 mpbiri ⊢¬RWeA∧RSeA→F:dom⁡F⟶A
18 10 17 pm2.61i ⊢F:dom⁡F⟶A