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 e. dom R1 -> ( R1 ` A ) = U_ x e. A ~P ( R1 ` x ) )

Proof

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