Metamath Proof Explorer


Theorem oieq2

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

Ref Expression
Assertion oieq2 A=BOrdIsoRA=OrdIsoRB

Proof

Step Hyp Ref Expression
1 weeq2 A=BRWeARWeB
2 seeq2 A=BRSeARSeB
3 1 2 anbi12d A=BRWeARSeARWeBRSeB
4 rabeq A=BwA|jranhjRw=wB|jranhjRw
5 4 raleqdv A=BuwA|jranhjRw¬uRvuwB|jranhjRw¬uRv
6 4 5 riotaeqbidv A=BιvwA|jranhjRw|uwA|jranhjRw¬uRv=ιvwB|jranhjRw|uwB|jranhjRw¬uRv
7 6 mpteq2dv A=BhVιvwA|jranhjRw|uwA|jranhjRw¬uRv=hVιvwB|jranhjRw|uwB|jranhjRw¬uRv
8 recseq hVιvwA|jranhjRw|uwA|jranhjRw¬uRv=hVιvwB|jranhjRw|uwB|jranhjRw¬uRvrecshVιvwA|jranhjRw|uwA|jranhjRw¬uRv=recshVιvwB|jranhjRw|uwB|jranhjRw¬uRv
9 7 8 syl A=BrecshVιvwA|jranhjRw|uwA|jranhjRw¬uRv=recshVιvwB|jranhjRw|uwB|jranhjRw¬uRv
10 9 imaeq1d A=BrecshVιvwA|jranhjRw|uwA|jranhjRw¬uRvx=recshVιvwB|jranhjRw|uwB|jranhjRw¬uRvx
11 10 raleqdv A=BzrecshVιvwA|jranhjRw|uwA|jranhjRw¬uRvxzRtzrecshVιvwB|jranhjRw|uwB|jranhjRw¬uRvxzRt
12 11 rexeqbi1dv A=BtAzrecshVιvwA|jranhjRw|uwA|jranhjRw¬uRvxzRttBzrecshVιvwB|jranhjRw|uwB|jranhjRw¬uRvxzRt
13 12 rabbidv A=BxOn|tAzrecshVιvwA|jranhjRw|uwA|jranhjRw¬uRvxzRt=xOn|tBzrecshVιvwB|jranhjRw|uwB|jranhjRw¬uRvxzRt
14 9 13 reseq12d A=BrecshVιvwA|jranhjRw|uwA|jranhjRw¬uRvxOn|tAzrecshVιvwA|jranhjRw|uwA|jranhjRw¬uRvxzRt=recshVιvwB|jranhjRw|uwB|jranhjRw¬uRvxOn|tBzrecshVιvwB|jranhjRw|uwB|jranhjRw¬uRvxzRt
15 3 14 ifbieq1d A=BifRWeARSeArecshVιvwA|jranhjRw|uwA|jranhjRw¬uRvxOn|tAzrecshVιvwA|jranhjRw|uwA|jranhjRw¬uRvxzRt=ifRWeBRSeBrecshVιvwB|jranhjRw|uwB|jranhjRw¬uRvxOn|tBzrecshVιvwB|jranhjRw|uwB|jranhjRw¬uRvxzRt
16 df-oi OrdIsoRA=ifRWeARSeArecshVιvwA|jranhjRw|uwA|jranhjRw¬uRvxOn|tAzrecshVιvwA|jranhjRw|uwA|jranhjRw¬uRvxzRt
17 df-oi OrdIsoRB=ifRWeBRSeBrecshVιvwB|jranhjRw|uwB|jranhjRw¬uRvxOn|tBzrecshVιvwB|jranhjRw|uwB|jranhjRw¬uRvxzRt
18 15 16 17 3eqtr4g A=BOrdIsoRA=OrdIsoRB