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 ( 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) → 𝒫 𝐴 ⊆ ( 𝑅1 ‘ 𝐵 ) )

Proof

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