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 | |
|
nfoi.2 | |
||
Assertion | nfoi | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfoi.1 | |
|
2 | nfoi.2 | |
|
3 | df-oi | |
|
4 | 1 2 | nfwe | |
5 | 1 2 | nfse | |
6 | 4 5 | nfan | |
7 | nfcv | |
|
8 | nfcv | |
|
9 | nfcv | |
|
10 | nfcv | |
|
11 | 9 1 10 | nfbr | |
12 | 8 11 | nfralw | |
13 | 12 2 | nfrabw | |
14 | nfcv | |
|
15 | nfcv | |
|
16 | 14 1 15 | nfbr | |
17 | 16 | nfn | |
18 | 13 17 | nfralw | |
19 | 18 13 | nfriota | |
20 | 7 19 | nfmpt | |
21 | 20 | nfrecs | |
22 | nfcv | |
|
23 | 21 22 | nfima | |
24 | nfcv | |
|
25 | nfcv | |
|
26 | 24 1 25 | nfbr | |
27 | 23 26 | nfralw | |
28 | 2 27 | nfrex | |
29 | nfcv | |
|
30 | 28 29 | nfrabw | |
31 | 21 30 | nfres | |
32 | nfcv | |
|
33 | 6 31 32 | nfif | |
34 | 3 33 | nfcxfr | |