Metamath Proof Explorer

Theorem r1pwss

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