Description: The value of the rank function expressed recursively: the rank of a set is the smallest ordinal number containing the ranks of all members of the set. Proposition 9.17 of TakeutiZaring p. 79. (Contributed by Mario Carneiro, 8-Jun-2013)
Ref | Expression | ||
---|---|---|---|
Assertion | rankuni2b | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | uniwf | |
|
2 | rankval3b | |
|
3 | 1 2 | sylbi | |
4 | eleq2 | |
|
5 | 4 | ralbidv | |
6 | iuneq1 | |
|
7 | 6 | eleq1d | |
8 | vex | |
|
9 | rankon | |
|
10 | 9 | rgenw | |
11 | iunon | |
|
12 | 8 10 11 | mp2an | |
13 | 7 12 | vtoclg | |
14 | eluni2 | |
|
15 | nfv | |
|
16 | nfiu1 | |
|
17 | 16 | nfel2 | |
18 | r1elssi | |
|
19 | 18 | sseld | |
20 | rankelb | |
|
21 | 19 20 | syl6 | |
22 | ssiun2 | |
|
23 | 22 | sseld | |
24 | 23 | a1i | |
25 | 21 24 | syldd | |
26 | 15 17 25 | rexlimd | |
27 | 14 26 | syl5bi | |
28 | 27 | ralrimiv | |
29 | 5 13 28 | elrabd | |
30 | intss1 | |
|
31 | 29 30 | syl | |
32 | 3 31 | eqsstrd | |
33 | 1 | biimpi | |
34 | elssuni | |
|
35 | rankssb | |
|
36 | 33 34 35 | syl2im | |
37 | 36 | ralrimiv | |
38 | iunss | |
|
39 | 37 38 | sylibr | |
40 | 32 39 | eqssd | |