Metamath Proof Explorer

Theorem dfoi

Description: Rewrite df-oi with abbreviations. (Contributed by Mario Carneiro, 24-Jun-2015)

Ref Expression
Hypotheses dfoi.1 ⊢C=w∈A|∀j∈ran⁡hjRw
dfoi.2 ⊢G=h∈V⟼ιv∈C|∀u∈C¬uRv
dfoi.3 ⊢F=recs⁡G
Assertion dfoi ⊢OrdIsoRA=ifRWeA∧RSeAF↾x∈On|∃t∈A∀z∈FxzRt∅

Proof

Step Hyp Ref Expression
1 dfoi.1 ⊢C=w∈A|∀j∈ran⁡hjRw
2 dfoi.2 ⊢G=h∈V⟼ιv∈C|∀u∈C¬uRv
3 dfoi.3 ⊢F=recs⁡G
4 df-oi ⊢OrdIsoRA=ifRWeA∧RSeArecs⁡h∈V⟼ιv∈w∈A|∀j∈ran⁡hjRw|∀u∈w∈A|∀j∈ran⁡hjRw¬uRv↾x∈On|∃t∈A∀z∈recs⁡h∈V⟼ιv∈w∈A|∀j∈ran⁡hjRw|∀u∈w∈A|∀j∈ran⁡hjRw¬uRvxzRt∅
5 1 a1i ⊢h∈V→C=w∈A|∀j∈ran⁡hjRw
6 5 raleqdv ⊢h∈V→∀u∈C¬uRv↔∀u∈w∈A|∀j∈ran⁡hjRw¬uRv
7 5 6 riotaeqbidv ⊢h∈V→ιv∈C|∀u∈C¬uRv=ιv∈w∈A|∀j∈ran⁡hjRw|∀u∈w∈A|∀j∈ran⁡hjRw¬uRv
8 7 mpteq2ia ⊢h∈V⟼ιv∈C|∀u∈C¬uRv=h∈V⟼ιv∈w∈A|∀j∈ran⁡hjRw|∀u∈w∈A|∀j∈ran⁡hjRw¬uRv
9 2 8 eqtri ⊢G=h∈V⟼ιv∈w∈A|∀j∈ran⁡hjRw|∀u∈w∈A|∀j∈ran⁡hjRw¬uRv
10 recseq ⊢G=h∈V⟼ιv∈w∈A|∀j∈ran⁡hjRw|∀u∈w∈A|∀j∈ran⁡hjRw¬uRv→recs⁡G=recs⁡h∈V⟼ιv∈w∈A|∀j∈ran⁡hjRw|∀u∈w∈A|∀j∈ran⁡hjRw¬uRv
11 9 10 ax-mp ⊢recs⁡G=recs⁡h∈V⟼ιv∈w∈A|∀j∈ran⁡hjRw|∀u∈w∈A|∀j∈ran⁡hjRw¬uRv
12 3 11 eqtri ⊢F=recs⁡h∈V⟼ιv∈w∈A|∀j∈ran⁡hjRw|∀u∈w∈A|∀j∈ran⁡hjRw¬uRv
13 12 imaeq1i ⊢Fx=recs⁡h∈V⟼ιv∈w∈A|∀j∈ran⁡hjRw|∀u∈w∈A|∀j∈ran⁡hjRw¬uRvx
14 13 raleqi ⊢∀z∈FxzRt↔∀z∈recs⁡h∈V⟼ιv∈w∈A|∀j∈ran⁡hjRw|∀u∈w∈A|∀j∈ran⁡hjRw¬uRvxzRt
15 14 rexbii ⊢∃t∈A∀z∈FxzRt↔∃t∈A∀z∈recs⁡h∈V⟼ιv∈w∈A|∀j∈ran⁡hjRw|∀u∈w∈A|∀j∈ran⁡hjRw¬uRvxzRt
16 15 rabbii ⊢x∈On|∃t∈A∀z∈FxzRt=x∈On|∃t∈A∀z∈recs⁡h∈V⟼ιv∈w∈A|∀j∈ran⁡hjRw|∀u∈w∈A|∀j∈ran⁡hjRw¬uRvxzRt
17 12 16 reseq12i ⊢F↾x∈On|∃t∈A∀z∈FxzRt=recs⁡h∈V⟼ιv∈w∈A|∀j∈ran⁡hjRw|∀u∈w∈A|∀j∈ran⁡hjRw¬uRv↾x∈On|∃t∈A∀z∈recs⁡h∈V⟼ιv∈w∈A|∀j∈ran⁡hjRw|∀u∈w∈A|∀j∈ran⁡hjRw¬uRvxzRt
18 ifeq1 ⊢F↾x∈On|∃t∈A∀z∈FxzRt=recs⁡h∈V⟼ιv∈w∈A|∀j∈ran⁡hjRw|∀u∈w∈A|∀j∈ran⁡hjRw¬uRv↾x∈On|∃t∈A∀z∈recs⁡h∈V⟼ιv∈w∈A|∀j∈ran⁡hjRw|∀u∈w∈A|∀j∈ran⁡hjRw¬uRvxzRt→ifRWeA∧RSeAF↾x∈On|∃t∈A∀z∈FxzRt∅=ifRWeA∧RSeArecs⁡h∈V⟼ιv∈w∈A|∀j∈ran⁡hjRw|∀u∈w∈A|∀j∈ran⁡hjRw¬uRv↾x∈On|∃t∈A∀z∈recs⁡h∈V⟼ιv∈w∈A|∀j∈ran⁡hjRw|∀u∈w∈A|∀j∈ran⁡hjRw¬uRvxzRt∅
19 17 18 ax-mp ⊢ifRWeA∧RSeAF↾x∈On|∃t∈A∀z∈FxzRt∅=ifRWeA∧RSeArecs⁡h∈V⟼ιv∈w∈A|∀j∈ran⁡hjRw|∀u∈w∈A|∀j∈ran⁡hjRw¬uRv↾x∈On|∃t∈A∀z∈recs⁡h∈V⟼ιv∈w∈A|∀j∈ran⁡hjRw|∀u∈w∈A|∀j∈ran⁡hjRw¬uRvxzRt∅
20 4 19 eqtr4i ⊢OrdIsoRA=ifRWeA∧RSeAF↾x∈On|∃t∈A∀z∈FxzRt∅