Description: The cumulative hierarchy of sets is transitive. Lemma 7T of Enderton p. 202. (Contributed by NM, 8-Sep-2003) (Revised by Mario Carneiro, 16-Nov-2014)
Ref | Expression | ||
---|---|---|---|
Assertion | r1tr | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | r1funlim | |
|
2 | 1 | simpri | |
3 | limord | |
|
4 | ordsson | |
|
5 | 2 3 4 | mp2b | |
6 | 5 | sseli | |
7 | fveq2 | |
|
8 | r10 | |
|
9 | 7 8 | eqtrdi | |
10 | treq | |
|
11 | 9 10 | syl | |
12 | fveq2 | |
|
13 | treq | |
|
14 | 12 13 | syl | |
15 | fveq2 | |
|
16 | treq | |
|
17 | 15 16 | syl | |
18 | fveq2 | |
|
19 | treq | |
|
20 | 18 19 | syl | |
21 | tr0 | |
|
22 | limsuc | |
|
23 | 2 22 | ax-mp | |
24 | simpr | |
|
25 | pwtr | |
|
26 | 24 25 | sylib | |
27 | r1sucg | |
|
28 | treq | |
|
29 | 27 28 | syl | |
30 | 26 29 | syl5ibrcom | |
31 | 23 30 | syl5bir | |
32 | ndmfv | |
|
33 | treq | |
|
34 | 32 33 | syl | |
35 | 21 34 | mpbiri | |
36 | 31 35 | pm2.61d1 | |
37 | 36 | ex | |
38 | triun | |
|
39 | r1limg | |
|
40 | 39 | ancoms | |
41 | treq | |
|
42 | 40 41 | syl | |
43 | 38 42 | syl5ibr | |
44 | 43 | impancom | |
45 | ndmfv | |
|
46 | 45 10 | syl | |
47 | 21 46 | mpbiri | |
48 | 44 47 | pm2.61d1 | |
49 | 48 | ex | |
50 | 11 14 17 20 21 37 49 | tfinds | |
51 | 6 50 | syl | |
52 | ndmfv | |
|
53 | treq | |
|
54 | 52 53 | syl | |
55 | 21 54 | mpbiri | |
56 | 51 55 | pm2.61i | |