Theorem r1pwss 9798

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

Assertion

Ref	Expression
r1pwss	⊢ (𝐴 ∈ (𝑅1‘𝐵) → 𝒫 𝐴 ⊆ (𝑅1‘𝐵))

Proof of Theorem r1pwss

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		r1funlim 9780	. . . . . . 7 ⊢ (Fun 𝑅1 ∧ Lim dom 𝑅1)
2	1	simpri 485	. . . . . 6 ⊢ Lim dom 𝑅1
3		limord 6413	. . . . . 6 ⊢ (Lim dom 𝑅1 → Ord dom 𝑅1)
4	2, 3	ax-mp 5	. . . . 5 ⊢ Ord dom 𝑅1
5		ordsson 7777	. . . . 5 ⊢ (Ord dom 𝑅1 → dom 𝑅1 ⊆ On)
6	4, 5	ax-mp 5	. . . 4 ⊢ dom 𝑅1 ⊆ On
7		elfvdm 6913	. . . 4 ⊢ (𝐴 ∈ (𝑅1‘𝐵) → 𝐵 ∈ dom 𝑅1)
8	6, 7	sselid 3956	. . 3 ⊢ (𝐴 ∈ (𝑅1‘𝐵) → 𝐵 ∈ On)
9		onzsl 7841	. . 3 ⊢ (𝐵 ∈ On ↔ (𝐵 = ∅ ∨ ∃𝑥 ∈ On 𝐵 = suc 𝑥 ∨ (𝐵 ∈ V ∧ Lim 𝐵)))
10	8, 9	sylib 218	. 2 ⊢ (𝐴 ∈ (𝑅1‘𝐵) → (𝐵 = ∅ ∨ ∃𝑥 ∈ On 𝐵 = suc 𝑥 ∨ (𝐵 ∈ V ∧ Lim 𝐵)))
11		noel 4313	. . . . 5 ⊢ ¬ 𝐴 ∈ ∅
12		fveq2 6876	. . . . . . . 8 ⊢ (𝐵 = ∅ → (𝑅1‘𝐵) = (𝑅1‘∅))
13		r10 9782	. . . . . . . 8 ⊢ (𝑅1‘∅) = ∅
14	12, 13	eqtrdi 2786	. . . . . . 7 ⊢ (𝐵 = ∅ → (𝑅1‘𝐵) = ∅)
15	14	eleq2d 2820	. . . . . 6 ⊢ (𝐵 = ∅ → (𝐴 ∈ (𝑅1‘𝐵) ↔ 𝐴 ∈ ∅))
16	15	biimpcd 249	. . . . 5 ⊢ (𝐴 ∈ (𝑅1‘𝐵) → (𝐵 = ∅ → 𝐴 ∈ ∅))
17	11, 16	mtoi 199	. . . 4 ⊢ (𝐴 ∈ (𝑅1‘𝐵) → ¬ 𝐵 = ∅)
18	17	pm2.21d 121	. . 3 ⊢ (𝐴 ∈ (𝑅1‘𝐵) → (𝐵 = ∅ → 𝒫 𝐴 ⊆ (𝑅1‘𝐵)))
19		simpl 482	. . . . . . . 8 ⊢ ((𝐴 ∈ (𝑅1‘𝐵) ∧ 𝐵 = suc 𝑥) → 𝐴 ∈ (𝑅1‘𝐵))
20		simpr 484	. . . . . . . . . 10 ⊢ ((𝐴 ∈ (𝑅1‘𝐵) ∧ 𝐵 = suc 𝑥) → 𝐵 = suc 𝑥)
21	20	fveq2d 6880	. . . . . . . . 9 ⊢ ((𝐴 ∈ (𝑅1‘𝐵) ∧ 𝐵 = suc 𝑥) → (𝑅1‘𝐵) = (𝑅1‘suc 𝑥))
22	7	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ (𝑅1‘𝐵) ∧ 𝐵 = suc 𝑥) → 𝐵 ∈ dom 𝑅1)
23	20, 22	eqeltrrd 2835	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ (𝑅1‘𝐵) ∧ 𝐵 = suc 𝑥) → suc 𝑥 ∈ dom 𝑅1)
24		limsuc 7844	. . . . . . . . . . . 12 ⊢ (Lim dom 𝑅1 → (𝑥 ∈ dom 𝑅1 ↔ suc 𝑥 ∈ dom 𝑅1))
25	2, 24	ax-mp 5	. . . . . . . . . . 11 ⊢ (𝑥 ∈ dom 𝑅1 ↔ suc 𝑥 ∈ dom 𝑅1)
26	23, 25	sylibr 234	. . . . . . . . . 10 ⊢ ((𝐴 ∈ (𝑅1‘𝐵) ∧ 𝐵 = suc 𝑥) → 𝑥 ∈ dom 𝑅1)
27		r1sucg 9783	. . . . . . . . . 10 ⊢ (𝑥 ∈ dom 𝑅1 → (𝑅1‘suc 𝑥) = 𝒫 (𝑅1‘𝑥))
28	26, 27	syl 17	. . . . . . . . 9 ⊢ ((𝐴 ∈ (𝑅1‘𝐵) ∧ 𝐵 = suc 𝑥) → (𝑅1‘suc 𝑥) = 𝒫 (𝑅1‘𝑥))
29	21, 28	eqtrd 2770	. . . . . . . 8 ⊢ ((𝐴 ∈ (𝑅1‘𝐵) ∧ 𝐵 = suc 𝑥) → (𝑅1‘𝐵) = 𝒫 (𝑅1‘𝑥))
30	19, 29	eleqtrd 2836	. . . . . . 7 ⊢ ((𝐴 ∈ (𝑅1‘𝐵) ∧ 𝐵 = suc 𝑥) → 𝐴 ∈ 𝒫 (𝑅1‘𝑥))
31		elpwi 4582	. . . . . . 7 ⊢ (𝐴 ∈ 𝒫 (𝑅1‘𝑥) → 𝐴 ⊆ (𝑅1‘𝑥))
32		sspw 4586	. . . . . . 7 ⊢ (𝐴 ⊆ (𝑅1‘𝑥) → 𝒫 𝐴 ⊆ 𝒫 (𝑅1‘𝑥))
33	30, 31, 32	3syl 18	. . . . . 6 ⊢ ((𝐴 ∈ (𝑅1‘𝐵) ∧ 𝐵 = suc 𝑥) → 𝒫 𝐴 ⊆ 𝒫 (𝑅1‘𝑥))
34	33, 29	sseqtrrd 3996	. . . . 5 ⊢ ((𝐴 ∈ (𝑅1‘𝐵) ∧ 𝐵 = suc 𝑥) → 𝒫 𝐴 ⊆ (𝑅1‘𝐵))
35	34	ex 412	. . . 4 ⊢ (𝐴 ∈ (𝑅1‘𝐵) → (𝐵 = suc 𝑥 → 𝒫 𝐴 ⊆ (𝑅1‘𝐵)))
36	35	rexlimdvw 3146	. . 3 ⊢ (𝐴 ∈ (𝑅1‘𝐵) → (∃𝑥 ∈ On 𝐵 = suc 𝑥 → 𝒫 𝐴 ⊆ (𝑅1‘𝐵)))
37		r1tr 9790	. . . . . 6 ⊢ Tr (𝑅1‘𝐵)
38		simpl 482	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ (𝑅1‘𝐵) ∧ Lim 𝐵) → 𝐴 ∈ (𝑅1‘𝐵))
39		r1limg 9785	. . . . . . . . . . . 12 ⊢ ((𝐵 ∈ dom 𝑅1 ∧ Lim 𝐵) → (𝑅1‘𝐵) = ∪ 𝑥 ∈ 𝐵 (𝑅1‘𝑥))
40	7, 39	sylan 580	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ (𝑅1‘𝐵) ∧ Lim 𝐵) → (𝑅1‘𝐵) = ∪ 𝑥 ∈ 𝐵 (𝑅1‘𝑥))
41	38, 40	eleqtrd 2836	. . . . . . . . . 10 ⊢ ((𝐴 ∈ (𝑅1‘𝐵) ∧ Lim 𝐵) → 𝐴 ∈ ∪ 𝑥 ∈ 𝐵 (𝑅1‘𝑥))
42		eliun 4971	. . . . . . . . . 10 ⊢ (𝐴 ∈ ∪ 𝑥 ∈ 𝐵 (𝑅1‘𝑥) ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ (𝑅1‘𝑥))
43	41, 42	sylib 218	. . . . . . . . 9 ⊢ ((𝐴 ∈ (𝑅1‘𝐵) ∧ Lim 𝐵) → ∃𝑥 ∈ 𝐵 𝐴 ∈ (𝑅1‘𝑥))
44		simprl 770	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ (𝑅1‘𝐵) ∧ Lim 𝐵) ∧ (𝑥 ∈ 𝐵 ∧ 𝐴 ∈ (𝑅1‘𝑥))) → 𝑥 ∈ 𝐵)
45		limsuc 7844	. . . . . . . . . . . . 13 ⊢ (Lim 𝐵 → (𝑥 ∈ 𝐵 ↔ suc 𝑥 ∈ 𝐵))
46	45	ad2antlr 727	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ (𝑅1‘𝐵) ∧ Lim 𝐵) ∧ (𝑥 ∈ 𝐵 ∧ 𝐴 ∈ (𝑅1‘𝑥))) → (𝑥 ∈ 𝐵 ↔ suc 𝑥 ∈ 𝐵))
47	44, 46	mpbid 232	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ (𝑅1‘𝐵) ∧ Lim 𝐵) ∧ (𝑥 ∈ 𝐵 ∧ 𝐴 ∈ (𝑅1‘𝑥))) → suc 𝑥 ∈ 𝐵)
48		limsuc 7844	. . . . . . . . . . . 12 ⊢ (Lim 𝐵 → (suc 𝑥 ∈ 𝐵 ↔ suc suc 𝑥 ∈ 𝐵))
49	48	ad2antlr 727	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ (𝑅1‘𝐵) ∧ Lim 𝐵) ∧ (𝑥 ∈ 𝐵 ∧ 𝐴 ∈ (𝑅1‘𝑥))) → (suc 𝑥 ∈ 𝐵 ↔ suc suc 𝑥 ∈ 𝐵))
50	47, 49	mpbid 232	. . . . . . . . . 10 ⊢ (((𝐴 ∈ (𝑅1‘𝐵) ∧ Lim 𝐵) ∧ (𝑥 ∈ 𝐵 ∧ 𝐴 ∈ (𝑅1‘𝑥))) → suc suc 𝑥 ∈ 𝐵)
51		r1tr 9790	. . . . . . . . . . . . . . 15 ⊢ Tr (𝑅1‘𝑥)
52		simprr 772	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ (𝑅1‘𝐵) ∧ Lim 𝐵) ∧ (𝑥 ∈ 𝐵 ∧ 𝐴 ∈ (𝑅1‘𝑥))) → 𝐴 ∈ (𝑅1‘𝑥))
53		trss 5240	. . . . . . . . . . . . . . 15 ⊢ (Tr (𝑅1‘𝑥) → (𝐴 ∈ (𝑅1‘𝑥) → 𝐴 ⊆ (𝑅1‘𝑥)))
54	51, 52, 53	mpsyl 68	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ (𝑅1‘𝐵) ∧ Lim 𝐵) ∧ (𝑥 ∈ 𝐵 ∧ 𝐴 ∈ (𝑅1‘𝑥))) → 𝐴 ⊆ (𝑅1‘𝑥))
55	54, 32	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ (𝑅1‘𝐵) ∧ Lim 𝐵) ∧ (𝑥 ∈ 𝐵 ∧ 𝐴 ∈ (𝑅1‘𝑥))) → 𝒫 𝐴 ⊆ 𝒫 (𝑅1‘𝑥))
56	7	ad2antrr 726	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ (𝑅1‘𝐵) ∧ Lim 𝐵) ∧ (𝑥 ∈ 𝐵 ∧ 𝐴 ∈ (𝑅1‘𝑥))) → 𝐵 ∈ dom 𝑅1)
57		ordtr1 6396	. . . . . . . . . . . . . . . 16 ⊢ (Ord dom 𝑅1 → ((𝑥 ∈ 𝐵 ∧ 𝐵 ∈ dom 𝑅1) → 𝑥 ∈ dom 𝑅1))
58	4, 57	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ 𝐵 ∧ 𝐵 ∈ dom 𝑅1) → 𝑥 ∈ dom 𝑅1)
59	44, 56, 58	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ (𝑅1‘𝐵) ∧ Lim 𝐵) ∧ (𝑥 ∈ 𝐵 ∧ 𝐴 ∈ (𝑅1‘𝑥))) → 𝑥 ∈ dom 𝑅1)
60	59, 27	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ (𝑅1‘𝐵) ∧ Lim 𝐵) ∧ (𝑥 ∈ 𝐵 ∧ 𝐴 ∈ (𝑅1‘𝑥))) → (𝑅1‘suc 𝑥) = 𝒫 (𝑅1‘𝑥))
61	55, 60	sseqtrrd 3996	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ (𝑅1‘𝐵) ∧ Lim 𝐵) ∧ (𝑥 ∈ 𝐵 ∧ 𝐴 ∈ (𝑅1‘𝑥))) → 𝒫 𝐴 ⊆ (𝑅1‘suc 𝑥))
62		fvex 6889	. . . . . . . . . . . . 13 ⊢ (𝑅1‘suc 𝑥) ∈ V
63	62	elpw2 5304	. . . . . . . . . . . 12 ⊢ (𝒫 𝐴 ∈ 𝒫 (𝑅1‘suc 𝑥) ↔ 𝒫 𝐴 ⊆ (𝑅1‘suc 𝑥))
64	61, 63	sylibr 234	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ (𝑅1‘𝐵) ∧ Lim 𝐵) ∧ (𝑥 ∈ 𝐵 ∧ 𝐴 ∈ (𝑅1‘𝑥))) → 𝒫 𝐴 ∈ 𝒫 (𝑅1‘suc 𝑥))
65	59, 25	sylib 218	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ (𝑅1‘𝐵) ∧ Lim 𝐵) ∧ (𝑥 ∈ 𝐵 ∧ 𝐴 ∈ (𝑅1‘𝑥))) → suc 𝑥 ∈ dom 𝑅1)
66		r1sucg 9783	. . . . . . . . . . . 12 ⊢ (suc 𝑥 ∈ dom 𝑅1 → (𝑅1‘suc suc 𝑥) = 𝒫 (𝑅1‘suc 𝑥))
67	65, 66	syl 17	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ (𝑅1‘𝐵) ∧ Lim 𝐵) ∧ (𝑥 ∈ 𝐵 ∧ 𝐴 ∈ (𝑅1‘𝑥))) → (𝑅1‘suc suc 𝑥) = 𝒫 (𝑅1‘suc 𝑥))
68	64, 67	eleqtrrd 2837	. . . . . . . . . 10 ⊢ (((𝐴 ∈ (𝑅1‘𝐵) ∧ Lim 𝐵) ∧ (𝑥 ∈ 𝐵 ∧ 𝐴 ∈ (𝑅1‘𝑥))) → 𝒫 𝐴 ∈ (𝑅1‘suc suc 𝑥))
69		fveq2 6876	. . . . . . . . . . . 12 ⊢ (𝑦 = suc suc 𝑥 → (𝑅1‘𝑦) = (𝑅1‘suc suc 𝑥))
70	69	eleq2d 2820	. . . . . . . . . . 11 ⊢ (𝑦 = suc suc 𝑥 → (𝒫 𝐴 ∈ (𝑅1‘𝑦) ↔ 𝒫 𝐴 ∈ (𝑅1‘suc suc 𝑥)))
71	70	rspcev 3601	. . . . . . . . . 10 ⊢ ((suc suc 𝑥 ∈ 𝐵 ∧ 𝒫 𝐴 ∈ (𝑅1‘suc suc 𝑥)) → ∃𝑦 ∈ 𝐵 𝒫 𝐴 ∈ (𝑅1‘𝑦))
72	50, 68, 71	syl2anc 584	. . . . . . . . 9 ⊢ (((𝐴 ∈ (𝑅1‘𝐵) ∧ Lim 𝐵) ∧ (𝑥 ∈ 𝐵 ∧ 𝐴 ∈ (𝑅1‘𝑥))) → ∃𝑦 ∈ 𝐵 𝒫 𝐴 ∈ (𝑅1‘𝑦))
73	43, 72	rexlimddv 3147	. . . . . . . 8 ⊢ ((𝐴 ∈ (𝑅1‘𝐵) ∧ Lim 𝐵) → ∃𝑦 ∈ 𝐵 𝒫 𝐴 ∈ (𝑅1‘𝑦))
74		eliun 4971	. . . . . . . 8 ⊢ (𝒫 𝐴 ∈ ∪ 𝑦 ∈ 𝐵 (𝑅1‘𝑦) ↔ ∃𝑦 ∈ 𝐵 𝒫 𝐴 ∈ (𝑅1‘𝑦))
75	73, 74	sylibr 234	. . . . . . 7 ⊢ ((𝐴 ∈ (𝑅1‘𝐵) ∧ Lim 𝐵) → 𝒫 𝐴 ∈ ∪ 𝑦 ∈ 𝐵 (𝑅1‘𝑦))
76		r1limg 9785	. . . . . . . 8 ⊢ ((𝐵 ∈ dom 𝑅1 ∧ Lim 𝐵) → (𝑅1‘𝐵) = ∪ 𝑦 ∈ 𝐵 (𝑅1‘𝑦))
77	7, 76	sylan 580	. . . . . . 7 ⊢ ((𝐴 ∈ (𝑅1‘𝐵) ∧ Lim 𝐵) → (𝑅1‘𝐵) = ∪ 𝑦 ∈ 𝐵 (𝑅1‘𝑦))
78	75, 77	eleqtrrd 2837	. . . . . 6 ⊢ ((𝐴 ∈ (𝑅1‘𝐵) ∧ Lim 𝐵) → 𝒫 𝐴 ∈ (𝑅1‘𝐵))
79		trss 5240	. . . . . 6 ⊢ (Tr (𝑅1‘𝐵) → (𝒫 𝐴 ∈ (𝑅1‘𝐵) → 𝒫 𝐴 ⊆ (𝑅1‘𝐵)))
80	37, 78, 79	mpsyl 68	. . . . 5 ⊢ ((𝐴 ∈ (𝑅1‘𝐵) ∧ Lim 𝐵) → 𝒫 𝐴 ⊆ (𝑅1‘𝐵))
81	80	ex 412	. . . 4 ⊢ (𝐴 ∈ (𝑅1‘𝐵) → (Lim 𝐵 → 𝒫 𝐴 ⊆ (𝑅1‘𝐵)))
82	81	adantld 490	. . 3 ⊢ (𝐴 ∈ (𝑅1‘𝐵) → ((𝐵 ∈ V ∧ Lim 𝐵) → 𝒫 𝐴 ⊆ (𝑅1‘𝐵)))
83	18, 36, 82	3jaod 1431	. 2 ⊢ (𝐴 ∈ (𝑅1‘𝐵) → ((𝐵 = ∅ ∨ ∃𝑥 ∈ On 𝐵 = suc 𝑥 ∨ (𝐵 ∈ V ∧ Lim 𝐵)) → 𝒫 𝐴 ⊆ (𝑅1‘𝐵)))
84	10, 83	mpd 15	1 ⊢ (𝐴 ∈ (𝑅1‘𝐵) → 𝒫 𝐴 ⊆ (𝑅1‘𝐵))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∨ w3o 1085   = wceq 1540   ∈ wcel 2108  ∃wrex 3060  Vcvv 3459   ⊆ wss 3926  ∅c0 4308  𝒫 cpw 4575  ∪ ciun 4967  Tr wtr 5229  dom cdm 5654  Ord word 6351  Oncon0 6352  Lim wlim 6353  suc csuc 6354  Fun wfun 6525  ‘cfv 6531  𝑅₁cr1 9776

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pow 5335  ax-pr 5402  ax-un 7729

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-reu 3360  df-rab 3416  df-v 3461  df-sbc 3766  df-csb 3875  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-pss 3946  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-iun 4969  df-br 5120  df-opab 5182  df-mpt 5202  df-tr 5230  df-id 5548  df-eprel 5553  df-po 5561  df-so 5562  df-fr 5606  df-we 5608  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-pred 6290  df-ord 6355  df-on 6356  df-lim 6357  df-suc 6358  df-iota 6484  df-fun 6533  df-fn 6534  df-f 6535  df-f1 6536  df-fo 6537  df-f1o 6538  df-fv 6539  df-ov 7408  df-om 7862  df-2nd 7989  df-frecs 8280  df-wrecs 8311  df-recs 8385  df-rdg 8424  df-r1 9778

This theorem is referenced by:  r1sscl  9799