Metamath Proof Explorer

Theorem oieq1

Description: Equality theorem for ordinal isomorphism. (Contributed by Mario Carneiro, 23-May-2015)

Ref Expression
Assertion oieq1 ⊢R=S→OrdIsoRA=OrdIsoSA

Proof

Step Hyp Ref Expression
1 weeq1 ⊢R=S→RWeA↔SWeA
2 seeq1 ⊢R=S→RSeA↔SSeA
3 1 2 anbi12d ⊢R=S→RWeA∧RSeA↔SWeA∧SSeA
4 breq ⊢R=S→jRw↔jSw
5 4 ralbidv ⊢R=S→∀j∈ran⁡hjRw↔∀j∈ran⁡hjSw
6 5 rabbidv ⊢R=S→w∈A|∀j∈ran⁡hjRw=w∈A|∀j∈ran⁡hjSw
7 breq ⊢R=S→uRv↔uSv
8 7 notbid ⊢R=S→¬uRv↔¬uSv
9 6 8 raleqbidv ⊢R=S→∀u∈w∈A|∀j∈ran⁡hjRw¬uRv↔∀u∈w∈A|∀j∈ran⁡hjSw¬uSv
10 6 9 riotaeqbidv ⊢R=S→ιv∈w∈A|∀j∈ran⁡hjRw|∀u∈w∈A|∀j∈ran⁡hjRw¬uRv=ιv∈w∈A|∀j∈ran⁡hjSw|∀u∈w∈A|∀j∈ran⁡hjSw¬uSv
11 10 mpteq2dv ⊢R=S→h∈V⟼ιv∈w∈A|∀j∈ran⁡hjRw|∀u∈w∈A|∀j∈ran⁡hjRw¬uRv=h∈V⟼ιv∈w∈A|∀j∈ran⁡hjSw|∀u∈w∈A|∀j∈ran⁡hjSw¬uSv
12 recseq ⊢h∈V⟼ιv∈w∈A|∀j∈ran⁡hjRw|∀u∈w∈A|∀j∈ran⁡hjRw¬uRv=h∈V⟼ιv∈w∈A|∀j∈ran⁡hjSw|∀u∈w∈A|∀j∈ran⁡hjSw¬uSv→recs⁡h∈V⟼ιv∈w∈A|∀j∈ran⁡hjRw|∀u∈w∈A|∀j∈ran⁡hjRw¬uRv=recs⁡h∈V⟼ιv∈w∈A|∀j∈ran⁡hjSw|∀u∈w∈A|∀j∈ran⁡hjSw¬uSv
13 11 12 syl ⊢R=S→recs⁡h∈V⟼ιv∈w∈A|∀j∈ran⁡hjRw|∀u∈w∈A|∀j∈ran⁡hjRw¬uRv=recs⁡h∈V⟼ιv∈w∈A|∀j∈ran⁡hjSw|∀u∈w∈A|∀j∈ran⁡hjSw¬uSv
14 13 imaeq1d ⊢R=S→recs⁡h∈V⟼ιv∈w∈A|∀j∈ran⁡hjRw|∀u∈w∈A|∀j∈ran⁡hjRw¬uRvx=recs⁡h∈V⟼ιv∈w∈A|∀j∈ran⁡hjSw|∀u∈w∈A|∀j∈ran⁡hjSw¬uSvx
15 breq ⊢R=S→zRt↔zSt
16 14 15 raleqbidv ⊢R=S→∀z∈recs⁡h∈V⟼ιv∈w∈A|∀j∈ran⁡hjRw|∀u∈w∈A|∀j∈ran⁡hjRw¬uRvxzRt↔∀z∈recs⁡h∈V⟼ιv∈w∈A|∀j∈ran⁡hjSw|∀u∈w∈A|∀j∈ran⁡hjSw¬uSvxzSt
17 16 rexbidv ⊢R=S→∃t∈A∀z∈recs⁡h∈V⟼ιv∈w∈A|∀j∈ran⁡hjRw|∀u∈w∈A|∀j∈ran⁡hjRw¬uRvxzRt↔∃t∈A∀z∈recs⁡h∈V⟼ιv∈w∈A|∀j∈ran⁡hjSw|∀u∈w∈A|∀j∈ran⁡hjSw¬uSvxzSt
18 17 rabbidv ⊢R=S→x∈On|∃t∈A∀z∈recs⁡h∈V⟼ιv∈w∈A|∀j∈ran⁡hjRw|∀u∈w∈A|∀j∈ran⁡hjRw¬uRvxzRt=x∈On|∃t∈A∀z∈recs⁡h∈V⟼ιv∈w∈A|∀j∈ran⁡hjSw|∀u∈w∈A|∀j∈ran⁡hjSw¬uSvxzSt
19 13 18 reseq12d ⊢R=S→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=recs⁡h∈V⟼ιv∈w∈A|∀j∈ran⁡hjSw|∀u∈w∈A|∀j∈ran⁡hjSw¬uSv↾x∈On|∃t∈A∀z∈recs⁡h∈V⟼ιv∈w∈A|∀j∈ran⁡hjSw|∀u∈w∈A|∀j∈ran⁡hjSw¬uSvxzSt
20 3 19 ifbieq1d ⊢R=S→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∅=ifSWeA∧SSeArecs⁡h∈V⟼ιv∈w∈A|∀j∈ran⁡hjSw|∀u∈w∈A|∀j∈ran⁡hjSw¬uSv↾x∈On|∃t∈A∀z∈recs⁡h∈V⟼ιv∈w∈A|∀j∈ran⁡hjSw|∀u∈w∈A|∀j∈ran⁡hjSw¬uSvxzSt∅
21 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∅
22 df-oi ⊢OrdIsoSA=ifSWeA∧SSeArecs⁡h∈V⟼ιv∈w∈A|∀j∈ran⁡hjSw|∀u∈w∈A|∀j∈ran⁡hjSw¬uSv↾x∈On|∃t∈A∀z∈recs⁡h∈V⟼ιv∈w∈A|∀j∈ran⁡hjSw|∀u∈w∈A|∀j∈ran⁡hjSw¬uSvxzSt∅
23 20 21 22 3eqtr4g ⊢R=S→OrdIsoRA=OrdIsoSA