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

Proof

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