Metamath Proof Explorer


Theorem r1val1

Description: The value of the cumulative hierarchy of sets function expressed recursively. Theorem 7Q of Enderton p. 202. (Contributed by NM, 25-Nov-2003) (Revised by Mario Carneiro, 17-Nov-2014)

Ref Expression
Assertion r1val1 A dom R1 R1 A = x A 𝒫 R1 x

Proof

Step Hyp Ref Expression
1 simpr A dom R1 A = A =
2 1 fveq2d A dom R1 A = R1 A = R1
3 r10 R1 =
4 2 3 syl6eq A dom R1 A = R1 A =
5 0ss x A 𝒫 R1 x
6 5 a1i A dom R1 A = x A 𝒫 R1 x
7 4 6 eqsstrd A dom R1 A = R1 A x A 𝒫 R1 x
8 nfv x A dom R1
9 nfcv _ x R1 A
10 nfiu1 _ x x A 𝒫 R1 x
11 9 10 nfss x R1 A x A 𝒫 R1 x
12 simpr A dom R1 A = suc x A = suc x
13 12 fveq2d A dom R1 A = suc x R1 A = R1 suc x
14 eleq1 A = suc x A dom R1 suc x dom R1
15 14 biimpac A dom R1 A = suc x suc x dom R1
16 r1funlim Fun R1 Lim dom R1
17 16 simpri Lim dom R1
18 limsuc Lim dom R1 x dom R1 suc x dom R1
19 17 18 ax-mp x dom R1 suc x dom R1
20 15 19 sylibr A dom R1 A = suc x x dom R1
21 r1sucg x dom R1 R1 suc x = 𝒫 R1 x
22 20 21 syl A dom R1 A = suc x R1 suc x = 𝒫 R1 x
23 13 22 eqtrd A dom R1 A = suc x R1 A = 𝒫 R1 x
24 vex x V
25 24 sucid x suc x
26 25 12 eleqtrrid A dom R1 A = suc x x A
27 ssiun2 x A 𝒫 R1 x x A 𝒫 R1 x
28 26 27 syl A dom R1 A = suc x 𝒫 R1 x x A 𝒫 R1 x
29 23 28 eqsstrd A dom R1 A = suc x R1 A x A 𝒫 R1 x
30 29 ex A dom R1 A = suc x R1 A x A 𝒫 R1 x
31 30 a1d A dom R1 x On A = suc x R1 A x A 𝒫 R1 x
32 8 11 31 rexlimd A dom R1 x On A = suc x R1 A x A 𝒫 R1 x
33 32 imp A dom R1 x On A = suc x R1 A x A 𝒫 R1 x
34 r1limg A dom R1 Lim A R1 A = x A R1 x
35 r1tr Tr R1 x
36 dftr4 Tr R1 x R1 x 𝒫 R1 x
37 35 36 mpbi R1 x 𝒫 R1 x
38 37 a1i A dom R1 Lim A R1 x 𝒫 R1 x
39 38 ralrimivw A dom R1 Lim A x A R1 x 𝒫 R1 x
40 ss2iun x A R1 x 𝒫 R1 x x A R1 x x A 𝒫 R1 x
41 39 40 syl A dom R1 Lim A x A R1 x x A 𝒫 R1 x
42 34 41 eqsstrd A dom R1 Lim A R1 A x A 𝒫 R1 x
43 42 adantrl A dom R1 A V Lim A R1 A x A 𝒫 R1 x
44 limord Lim dom R1 Ord dom R1
45 17 44 ax-mp Ord dom R1
46 ordsson Ord dom R1 dom R1 On
47 45 46 ax-mp dom R1 On
48 47 sseli A dom R1 A On
49 onzsl A On A = x On A = suc x A V Lim A
50 48 49 sylib A dom R1 A = x On A = suc x A V Lim A
51 7 33 43 50 mpjao3dan A dom R1 R1 A x A 𝒫 R1 x
52 ordtr1 Ord dom R1 x A A dom R1 x dom R1
53 45 52 ax-mp x A A dom R1 x dom R1
54 53 ancoms A dom R1 x A x dom R1
55 54 21 syl A dom R1 x A R1 suc x = 𝒫 R1 x
56 simpr A dom R1 x A x A
57 ordelord Ord dom R1 A dom R1 Ord A
58 45 57 mpan A dom R1 Ord A
59 58 adantr A dom R1 x A Ord A
60 ordelsuc x A Ord A x A suc x A
61 56 59 60 syl2anc A dom R1 x A x A suc x A
62 56 61 mpbid A dom R1 x A suc x A
63 54 19 sylib A dom R1 x A suc x dom R1
64 simpl A dom R1 x A A dom R1
65 r1ord3g suc x dom R1 A dom R1 suc x A R1 suc x R1 A
66 63 64 65 syl2anc A dom R1 x A suc x A R1 suc x R1 A
67 62 66 mpd A dom R1 x A R1 suc x R1 A
68 55 67 eqsstrrd A dom R1 x A 𝒫 R1 x R1 A
69 68 ralrimiva A dom R1 x A 𝒫 R1 x R1 A
70 iunss x A 𝒫 R1 x R1 A x A 𝒫 R1 x R1 A
71 69 70 sylibr A dom R1 x A 𝒫 R1 x R1 A
72 51 71 eqssd A dom R1 R1 A = x A 𝒫 R1 x