Metamath Proof Explorer

Theorem r1pwss

Description: Each set of the cumulative hierarchy is closed under subsets. (Contributed by Mario Carneiro, 16-Nov-2014)

Ref Expression
Assertion r1pwss 
|- ( A e. ( R1 ` B ) -> ~P A C_ ( R1 ` B ) )

Proof

Step Hyp Ref Expression
1 r1funlim 
 |-  ( Fun R1 /\ Lim dom R1 )
2 1 simpri 
 |-  Lim dom R1
3 limord 
 |-  ( Lim dom R1 -> Ord dom R1 )
4 2 3 ax-mp 
 |-  Ord dom R1
5 ordsson 
 |-  ( Ord dom R1 -> dom R1 C_ On )
6 4 5 ax-mp 
 |-  dom R1 C_ On
7 elfvdm 
 |-  ( A e. ( R1 ` B ) -> B e. dom R1 )
8 6 7 sselid 
 |-  ( A e. ( R1 ` B ) -> B e. On )
9 onzsl 
 |-  ( B e. On <-> ( B = (/) \/ E. x e. On B = suc x \/ ( B e. _V /\ Lim B ) ) )
10 8 9 sylib 
 |-  ( A e. ( R1 ` B ) -> ( B = (/) \/ E. x e. On B = suc x \/ ( B e. _V /\ Lim B ) ) )
11 noel 
 |-  -. A e. (/)
12 fveq2 
 |-  ( B = (/) -> ( R1 ` B ) = ( R1 ` (/) ) )
13 r10 
 |-  ( R1 ` (/) ) = (/)
14 12 13 eqtrdi 
 |-  ( B = (/) -> ( R1 ` B ) = (/) )
15 14 eleq2d 
 |-  ( B = (/) -> ( A e. ( R1 ` B ) <-> A e. (/) ) )
16 15 biimpcd 
 |-  ( A e. ( R1 ` B ) -> ( B = (/) -> A e. (/) ) )
17 11 16 mtoi 
 |-  ( A e. ( R1 ` B ) -> -. B = (/) )
18 17 pm2.21d 
 |-  ( A e. ( R1 ` B ) -> ( B = (/) -> ~P A C_ ( R1 ` B ) ) )
19 simpl 
 |-  ( ( A e. ( R1 ` B ) /\ B = suc x ) -> A e. ( R1 ` B ) )
20 simpr 
 |-  ( ( A e. ( R1 ` B ) /\ B = suc x ) -> B = suc x )
21 20 fveq2d 
 |-  ( ( A e. ( R1 ` B ) /\ B = suc x ) -> ( R1 ` B ) = ( R1 ` suc x ) )
22 7 adantr 
 |-  ( ( A e. ( R1 ` B ) /\ B = suc x ) -> B e. dom R1 )
23 20 22 eqeltrrd 
 |-  ( ( A e. ( R1 ` B ) /\ B = suc x ) -> suc x e. dom R1 )
24 limsuc 
 |-  ( Lim dom R1 -> ( x e. dom R1 <-> suc x e. dom R1 ) )
25 2 24 ax-mp 
 |-  ( x e. dom R1 <-> suc x e. dom R1 )
26 23 25 sylibr 
 |-  ( ( A e. ( R1 ` B ) /\ B = suc x ) -> x e. dom R1 )
27 r1sucg 
 |-  ( x e. dom R1 -> ( R1 ` suc x ) = ~P ( R1 ` x ) )
28 26 27 syl 
 |-  ( ( A e. ( R1 ` B ) /\ B = suc x ) -> ( R1 ` suc x ) = ~P ( R1 ` x ) )
29 21 28 eqtrd 
 |-  ( ( A e. ( R1 ` B ) /\ B = suc x ) -> ( R1 ` B ) = ~P ( R1 ` x ) )
30 19 29 eleqtrd 
 |-  ( ( A e. ( R1 ` B ) /\ B = suc x ) -> A e. ~P ( R1 ` x ) )
31 elpwi 
 |-  ( A e. ~P ( R1 ` x ) -> A C_ ( R1 ` x ) )
32 sspw 
 |-  ( A C_ ( R1 ` x ) -> ~P A C_ ~P ( R1 ` x ) )
33 30 31 32 3syl 
 |-  ( ( A e. ( R1 ` B ) /\ B = suc x ) -> ~P A C_ ~P ( R1 ` x ) )
34 33 29 sseqtrrd 
 |-  ( ( A e. ( R1 ` B ) /\ B = suc x ) -> ~P A C_ ( R1 ` B ) )
35 34 ex 
 |-  ( A e. ( R1 ` B ) -> ( B = suc x -> ~P A C_ ( R1 ` B ) ) )
36 35 rexlimdvw 
 |-  ( A e. ( R1 ` B ) -> ( E. x e. On B = suc x -> ~P A C_ ( R1 ` B ) ) )
37 r1tr 
 |-  Tr ( R1 ` B )
38 simpl 
 |-  ( ( A e. ( R1 ` B ) /\ Lim B ) -> A e. ( R1 ` B ) )
39 r1limg 
 |-  ( ( B e. dom R1 /\ Lim B ) -> ( R1 ` B ) = U_ x e. B ( R1 ` x ) )
40 7 39 sylan 
 |-  ( ( A e. ( R1 ` B ) /\ Lim B ) -> ( R1 ` B ) = U_ x e. B ( R1 ` x ) )
41 38 40 eleqtrd 
 |-  ( ( A e. ( R1 ` B ) /\ Lim B ) -> A e. U_ x e. B ( R1 ` x ) )
42 eliun 
 |-  ( A e. U_ x e. B ( R1 ` x ) <-> E. x e. B A e. ( R1 ` x ) )
43 41 42 sylib 
 |-  ( ( A e. ( R1 ` B ) /\ Lim B ) -> E. x e. B A e. ( R1 ` x ) )
44 simprl 
 |-  ( ( ( A e. ( R1 ` B ) /\ Lim B ) /\ ( x e. B /\ A e. ( R1 ` x ) ) ) -> x e. B )
45 limsuc 
 |-  ( Lim B -> ( x e. B <-> suc x e. B ) )
46 45 ad2antlr 
 |-  ( ( ( A e. ( R1 ` B ) /\ Lim B ) /\ ( x e. B /\ A e. ( R1 ` x ) ) ) -> ( x e. B <-> suc x e. B ) )
47 44 46 mpbid 
 |-  ( ( ( A e. ( R1 ` B ) /\ Lim B ) /\ ( x e. B /\ A e. ( R1 ` x ) ) ) -> suc x e. B )
48 limsuc 
 |-  ( Lim B -> ( suc x e. B <-> suc suc x e. B ) )
49 48 ad2antlr 
 |-  ( ( ( A e. ( R1 ` B ) /\ Lim B ) /\ ( x e. B /\ A e. ( R1 ` x ) ) ) -> ( suc x e. B <-> suc suc x e. B ) )
50 47 49 mpbid 
 |-  ( ( ( A e. ( R1 ` B ) /\ Lim B ) /\ ( x e. B /\ A e. ( R1 ` x ) ) ) -> suc suc x e. B )
51 r1tr 
 |-  Tr ( R1 ` x )
52 simprr 
 |-  ( ( ( A e. ( R1 ` B ) /\ Lim B ) /\ ( x e. B /\ A e. ( R1 ` x ) ) ) -> A e. ( R1 ` x ) )
53 trss 
 |-  ( Tr ( R1 ` x ) -> ( A e. ( R1 ` x ) -> A C_ ( R1 ` x ) ) )
54 51 52 53 mpsyl 
 |-  ( ( ( A e. ( R1 ` B ) /\ Lim B ) /\ ( x e. B /\ A e. ( R1 ` x ) ) ) -> A C_ ( R1 ` x ) )
55 54 32 syl 
 |-  ( ( ( A e. ( R1 ` B ) /\ Lim B ) /\ ( x e. B /\ A e. ( R1 ` x ) ) ) -> ~P A C_ ~P ( R1 ` x ) )
56 7 ad2antrr 
 |-  ( ( ( A e. ( R1 ` B ) /\ Lim B ) /\ ( x e. B /\ A e. ( R1 ` x ) ) ) -> B e. dom R1 )
57 ordtr1 
 |-  ( Ord dom R1 -> ( ( x e. B /\ B e. dom R1 ) -> x e. dom R1 ) )
58 4 57 ax-mp 
 |-  ( ( x e. B /\ B e. dom R1 ) -> x e. dom R1 )
59 44 56 58 syl2anc 
 |-  ( ( ( A e. ( R1 ` B ) /\ Lim B ) /\ ( x e. B /\ A e. ( R1 ` x ) ) ) -> x e. dom R1 )
60 59 27 syl 
 |-  ( ( ( A e. ( R1 ` B ) /\ Lim B ) /\ ( x e. B /\ A e. ( R1 ` x ) ) ) -> ( R1 ` suc x ) = ~P ( R1 ` x ) )
61 55 60 sseqtrrd 
 |-  ( ( ( A e. ( R1 ` B ) /\ Lim B ) /\ ( x e. B /\ A e. ( R1 ` x ) ) ) -> ~P A C_ ( R1 ` suc x ) )
62 fvex 
 |-  ( R1 ` suc x ) e. _V
63 62 elpw2 
 |-  ( ~P A e. ~P ( R1 ` suc x ) <-> ~P A C_ ( R1 ` suc x ) )
64 61 63 sylibr 
 |-  ( ( ( A e. ( R1 ` B ) /\ Lim B ) /\ ( x e. B /\ A e. ( R1 ` x ) ) ) -> ~P A e. ~P ( R1 ` suc x ) )
65 59 25 sylib 
 |-  ( ( ( A e. ( R1 ` B ) /\ Lim B ) /\ ( x e. B /\ A e. ( R1 ` x ) ) ) -> suc x e. dom R1 )
66 r1sucg 
 |-  ( suc x e. dom R1 -> ( R1 ` suc suc x ) = ~P ( R1 ` suc x ) )
67 65 66 syl 
 |-  ( ( ( A e. ( R1 ` B ) /\ Lim B ) /\ ( x e. B /\ A e. ( R1 ` x ) ) ) -> ( R1 ` suc suc x ) = ~P ( R1 ` suc x ) )
68 64 67 eleqtrrd 
 |-  ( ( ( A e. ( R1 ` B ) /\ Lim B ) /\ ( x e. B /\ A e. ( R1 ` x ) ) ) -> ~P A e. ( R1 ` suc suc x ) )
69 fveq2 
 |-  ( y = suc suc x -> ( R1 ` y ) = ( R1 ` suc suc x ) )
70 69 eleq2d 
 |-  ( y = suc suc x -> ( ~P A e. ( R1 ` y ) <-> ~P A e. ( R1 ` suc suc x ) ) )
71 70 rspcev 
 |-  ( ( suc suc x e. B /\ ~P A e. ( R1 ` suc suc x ) ) -> E. y e. B ~P A e. ( R1 ` y ) )
72 50 68 71 syl2anc 
 |-  ( ( ( A e. ( R1 ` B ) /\ Lim B ) /\ ( x e. B /\ A e. ( R1 ` x ) ) ) -> E. y e. B ~P A e. ( R1 ` y ) )
73 43 72 rexlimddv 
 |-  ( ( A e. ( R1 ` B ) /\ Lim B ) -> E. y e. B ~P A e. ( R1 ` y ) )
74 eliun 
 |-  ( ~P A e. U_ y e. B ( R1 ` y ) <-> E. y e. B ~P A e. ( R1 ` y ) )
75 73 74 sylibr 
 |-  ( ( A e. ( R1 ` B ) /\ Lim B ) -> ~P A e. U_ y e. B ( R1 ` y ) )
76 r1limg 
 |-  ( ( B e. dom R1 /\ Lim B ) -> ( R1 ` B ) = U_ y e. B ( R1 ` y ) )
77 7 76 sylan 
 |-  ( ( A e. ( R1 ` B ) /\ Lim B ) -> ( R1 ` B ) = U_ y e. B ( R1 ` y ) )
78 75 77 eleqtrrd 
 |-  ( ( A e. ( R1 ` B ) /\ Lim B ) -> ~P A e. ( R1 ` B ) )
79 trss 
 |-  ( Tr ( R1 ` B ) -> ( ~P A e. ( R1 ` B ) -> ~P A C_ ( R1 ` B ) ) )
80 37 78 79 mpsyl 
 |-  ( ( A e. ( R1 ` B ) /\ Lim B ) -> ~P A C_ ( R1 ` B ) )
81 80 ex 
 |-  ( A e. ( R1 ` B ) -> ( Lim B -> ~P A C_ ( R1 ` B ) ) )
82 81 adantld 
 |-  ( A e. ( R1 ` B ) -> ( ( B e. _V /\ Lim B ) -> ~P A C_ ( R1 ` B ) ) )
83 18 36 82 3jaod 
 |-  ( A e. ( R1 ` B ) -> ( ( B = (/) \/ E. x e. On B = suc x \/ ( B e. _V /\ Lim B ) ) -> ~P A C_ ( R1 ` B ) ) )
84 10 83 mpd 
 |-  ( A e. ( R1 ` B ) -> ~P A C_ ( R1 ` B ) )