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 r1funlim 
 |-  ( Fun R1 /\ Lim dom R1 )
17 16 simpri 
 |-  Lim dom R1
18 limsuc 
 |-  ( Lim dom R1 -> ( x e. dom R1 <-> suc x e. dom R1 ) )
19 17 18 ax-mp 
 |-  ( x e. dom R1 <-> suc x e. dom R1 )
20 15 19 sylibr 
 |-  ( ( A e. dom R1 /\ A = suc x ) -> x e. dom R1 )
21 r1sucg 
 |-  ( x e. dom R1 -> ( R1 ` suc x ) = ~P ( R1 ` x ) )
22 20 21 syl 
 |-  ( ( A e. dom R1 /\ A = suc x ) -> ( R1 ` suc x ) = ~P ( R1 ` x ) )
23 13 22 eqtrd 
 |-  ( ( A e. dom R1 /\ A = suc x ) -> ( R1 ` A ) = ~P ( R1 ` x ) )
24 vex 
 |-  x e. _V
25 24 sucid 
 |-  x e. suc x
26 25 12 eleqtrrid 
 |-  ( ( A e. dom R1 /\ A = suc x ) -> x e. A )
27 ssiun2 
 |-  ( x e. A -> ~P ( R1 ` x ) C_ U_ x e. A ~P ( R1 ` x ) )
28 26 27 syl 
 |-  ( ( A e. dom R1 /\ A = suc x ) -> ~P ( R1 ` x ) C_ U_ x e. A ~P ( R1 ` x ) )
29 23 28 eqsstrd 
 |-  ( ( A e. dom R1 /\ A = suc x ) -> ( R1 ` A ) C_ U_ x e. A ~P ( R1 ` x ) )
30 29 ex 
 |-  ( A e. dom R1 -> ( A = suc x -> ( R1 ` A ) C_ U_ x e. A ~P ( R1 ` x ) ) )
31 30 a1d 
 |-  ( A e. dom R1 -> ( x e. On -> ( A = suc x -> ( R1 ` A ) C_ U_ x e. A ~P ( R1 ` x ) ) ) )
32 8 11 31 rexlimd 
 |-  ( A e. dom R1 -> ( E. x e. On A = suc x -> ( R1 ` A ) C_ U_ x e. A ~P ( R1 ` x ) ) )
33 32 imp 
 |-  ( ( A e. dom R1 /\ E. x e. On A = suc x ) -> ( R1 ` A ) C_ U_ x e. A ~P ( R1 ` x ) )
34 r1limg 
 |-  ( ( A e. dom R1 /\ Lim A ) -> ( R1 ` A ) = U_ x e. A ( R1 ` x ) )
35 r1tr 
 |-  Tr ( R1 ` x )
36 dftr4 
 |-  ( Tr ( R1 ` x ) <-> ( R1 ` x ) C_ ~P ( R1 ` x ) )
37 35 36 mpbi 
 |-  ( R1 ` x ) C_ ~P ( R1 ` x )
38 37 a1i 
 |-  ( ( A e. dom R1 /\ Lim A ) -> ( R1 ` x ) C_ ~P ( R1 ` x ) )
39 38 ralrimivw 
 |-  ( ( A e. dom R1 /\ Lim A ) -> A. x e. A ( R1 ` x ) C_ ~P ( R1 ` x ) )
40 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 ) )
41 39 40 syl 
 |-  ( ( A e. dom R1 /\ Lim A ) -> U_ x e. A ( R1 ` x ) C_ U_ x e. A ~P ( R1 ` x ) )
42 34 41 eqsstrd 
 |-  ( ( A e. dom R1 /\ Lim A ) -> ( R1 ` A ) C_ U_ x e. A ~P ( R1 ` x ) )
43 42 adantrl 
 |-  ( ( A e. dom R1 /\ ( A e. _V /\ Lim A ) ) -> ( R1 ` A ) C_ U_ x e. A ~P ( 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 C_ On )
47 45 46 ax-mp 
 |-  dom R1 C_ On
48 47 sseli 
 |-  ( A e. dom R1 -> A e. On )
49 onzsl 
 |-  ( A e. On <-> ( A = (/) \/ E. x e. On A = suc x \/ ( A e. _V /\ Lim A ) ) )
50 48 49 sylib 
 |-  ( A e. dom R1 -> ( A = (/) \/ E. x e. On A = suc x \/ ( A e. _V /\ Lim A ) ) )
51 7 33 43 50 mpjao3dan 
 |-  ( A e. dom R1 -> ( R1 ` A ) C_ U_ x e. A ~P ( R1 ` x ) )
52 ordtr1 
 |-  ( Ord dom R1 -> ( ( x e. A /\ A e. dom R1 ) -> x e. dom R1 ) )
53 45 52 ax-mp 
 |-  ( ( x e. A /\ A e. dom R1 ) -> x e. dom R1 )
54 53 ancoms 
 |-  ( ( A e. dom R1 /\ x e. A ) -> x e. dom R1 )
55 54 21 syl 
 |-  ( ( A e. dom R1 /\ x e. A ) -> ( R1 ` suc x ) = ~P ( R1 ` x ) )
56 simpr 
 |-  ( ( A e. dom R1 /\ x e. A ) -> x e. A )
57 ordelord 
 |-  ( ( Ord dom R1 /\ A e. dom R1 ) -> Ord A )
58 45 57 mpan 
 |-  ( A e. dom R1 -> Ord A )
59 58 adantr 
 |-  ( ( A e. dom R1 /\ x e. A ) -> Ord A )
60 ordelsuc 
 |-  ( ( x e. A /\ Ord A ) -> ( x e. A <-> suc x C_ A ) )
61 56 59 60 syl2anc 
 |-  ( ( A e. dom R1 /\ x e. A ) -> ( x e. A <-> suc x C_ A ) )
62 56 61 mpbid 
 |-  ( ( A e. dom R1 /\ x e. A ) -> suc x C_ A )
63 54 19 sylib 
 |-  ( ( A e. dom R1 /\ x e. A ) -> suc x e. dom R1 )
64 simpl 
 |-  ( ( A e. dom R1 /\ x e. A ) -> A e. dom R1 )
65 r1ord3g 
 |-  ( ( suc x e. dom R1 /\ A e. dom R1 ) -> ( suc x C_ A -> ( R1 ` suc x ) C_ ( R1 ` A ) ) )
66 63 64 65 syl2anc 
 |-  ( ( A e. dom R1 /\ x e. A ) -> ( suc x C_ A -> ( R1 ` suc x ) C_ ( R1 ` A ) ) )
67 62 66 mpd 
 |-  ( ( A e. dom R1 /\ x e. A ) -> ( R1 ` suc x ) C_ ( R1 ` A ) )
68 55 67 eqsstrrd 
 |-  ( ( A e. dom R1 /\ x e. A ) -> ~P ( R1 ` x ) C_ ( R1 ` A ) )
69 68 ralrimiva 
 |-  ( A e. dom R1 -> A. x e. A ~P ( R1 ` x ) C_ ( R1 ` A ) )
70 iunss 
 |-  ( U_ x e. A ~P ( R1 ` x ) C_ ( R1 ` A ) <-> A. x e. A ~P ( R1 ` x ) C_ ( R1 ` A ) )
71 69 70 sylibr 
 |-  ( A e. dom R1 -> U_ x e. A ~P ( R1 ` x ) C_ ( R1 ` A ) )
72 51 71 eqssd 
 |-  ( A e. dom R1 -> ( R1 ` A ) = U_ x e. A ~P ( R1 ` x ) )