Metamath Proof Explorer


Theorem nfoi

Description: Hypothesis builder for ordinal isomorphism. (Contributed by Mario Carneiro, 23-May-2015) (Revised by Mario Carneiro, 15-Oct-2016)

Ref Expression
Hypotheses nfoi.1 _xR
nfoi.2 _xA
Assertion nfoi _xOrdIsoRA

Proof

Step Hyp Ref Expression
1 nfoi.1 _xR
2 nfoi.2 _xA
3 df-oi OrdIsoRA=ifRWeARSeArecshVιvwA|jranhjRw|uwA|jranhjRw¬uRvaOn|tAzrecshVιvwA|jranhjRw|uwA|jranhjRw¬uRvazRt
4 1 2 nfwe xRWeA
5 1 2 nfse xRSeA
6 4 5 nfan xRWeARSeA
7 nfcv _xV
8 nfcv _xranh
9 nfcv _xj
10 nfcv _xw
11 9 1 10 nfbr xjRw
12 8 11 nfralw xjranhjRw
13 12 2 nfrabw _xwA|jranhjRw
14 nfcv _xu
15 nfcv _xv
16 14 1 15 nfbr xuRv
17 16 nfn x¬uRv
18 13 17 nfralw xuwA|jranhjRw¬uRv
19 18 13 nfriota _xιvwA|jranhjRw|uwA|jranhjRw¬uRv
20 7 19 nfmpt _xhVιvwA|jranhjRw|uwA|jranhjRw¬uRv
21 20 nfrecs _xrecshVιvwA|jranhjRw|uwA|jranhjRw¬uRv
22 nfcv _xa
23 21 22 nfima _xrecshVιvwA|jranhjRw|uwA|jranhjRw¬uRva
24 nfcv _xz
25 nfcv _xt
26 24 1 25 nfbr xzRt
27 23 26 nfralw xzrecshVιvwA|jranhjRw|uwA|jranhjRw¬uRvazRt
28 2 27 nfrex xtAzrecshVιvwA|jranhjRw|uwA|jranhjRw¬uRvazRt
29 nfcv _xOn
30 28 29 nfrabw _xaOn|tAzrecshVιvwA|jranhjRw|uwA|jranhjRw¬uRvazRt
31 21 30 nfres _xrecshVιvwA|jranhjRw|uwA|jranhjRw¬uRvaOn|tAzrecshVιvwA|jranhjRw|uwA|jranhjRw¬uRvazRt
32 nfcv _x
33 6 31 32 nfif _xifRWeARSeArecshVιvwA|jranhjRw|uwA|jranhjRw¬uRvaOn|tAzrecshVιvwA|jranhjRw|uwA|jranhjRw¬uRvazRt
34 3 33 nfcxfr _xOrdIsoRA