Metamath Proof Explorer


Theorem r1tr

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 TrR1A

Proof

Step Hyp Ref Expression
1 r1funlim FunR1LimdomR1
2 1 simpri LimdomR1
3 limord LimdomR1OrddomR1
4 ordsson OrddomR1domR1On
5 2 3 4 mp2b domR1On
6 5 sseli AdomR1AOn
7 fveq2 x=R1x=R1
8 r10 R1=
9 7 8 eqtrdi x=R1x=
10 treq R1x=TrR1xTr
11 9 10 syl x=TrR1xTr
12 fveq2 x=yR1x=R1y
13 treq R1x=R1yTrR1xTrR1y
14 12 13 syl x=yTrR1xTrR1y
15 fveq2 x=sucyR1x=R1sucy
16 treq R1x=R1sucyTrR1xTrR1sucy
17 15 16 syl x=sucyTrR1xTrR1sucy
18 fveq2 x=AR1x=R1A
19 treq R1x=R1ATrR1xTrR1A
20 18 19 syl x=ATrR1xTrR1A
21 tr0 Tr
22 limsuc LimdomR1ydomR1sucydomR1
23 2 22 ax-mp ydomR1sucydomR1
24 simpr yOnTrR1yTrR1y
25 pwtr TrR1yTr𝒫R1y
26 24 25 sylib yOnTrR1yTr𝒫R1y
27 r1sucg ydomR1R1sucy=𝒫R1y
28 treq R1sucy=𝒫R1yTrR1sucyTr𝒫R1y
29 27 28 syl ydomR1TrR1sucyTr𝒫R1y
30 26 29 syl5ibrcom yOnTrR1yydomR1TrR1sucy
31 23 30 syl5bir yOnTrR1ysucydomR1TrR1sucy
32 ndmfv ¬sucydomR1R1sucy=
33 treq R1sucy=TrR1sucyTr
34 32 33 syl ¬sucydomR1TrR1sucyTr
35 21 34 mpbiri ¬sucydomR1TrR1sucy
36 31 35 pm2.61d1 yOnTrR1yTrR1sucy
37 36 ex yOnTrR1yTrR1sucy
38 triun yxTrR1yTryxR1y
39 r1limg xdomR1LimxR1x=yxR1y
40 39 ancoms LimxxdomR1R1x=yxR1y
41 treq R1x=yxR1yTrR1xTryxR1y
42 40 41 syl LimxxdomR1TrR1xTryxR1y
43 38 42 syl5ibr LimxxdomR1yxTrR1yTrR1x
44 43 impancom LimxyxTrR1yxdomR1TrR1x
45 ndmfv ¬xdomR1R1x=
46 45 10 syl ¬xdomR1TrR1xTr
47 21 46 mpbiri ¬xdomR1TrR1x
48 44 47 pm2.61d1 LimxyxTrR1yTrR1x
49 48 ex LimxyxTrR1yTrR1x
50 11 14 17 20 21 37 49 tfinds AOnTrR1A
51 6 50 syl AdomR1TrR1A
52 ndmfv ¬AdomR1R1A=
53 treq R1A=TrR1ATr
54 52 53 syl ¬AdomR1TrR1ATr
55 21 54 mpbiri ¬AdomR1TrR1A
56 51 55 pm2.61i TrR1A