Theorem r1pwss 9677

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 9659	. . . . . . 7 ⊢ (Fun 𝑅1 ∧ Lim dom 𝑅1)
2	1	simpri 485	. . . . . 6 ⊢ Lim dom 𝑅1
3		limord 6367	. . . . . 6 ⊢ (Lim dom 𝑅1 → Ord dom 𝑅1)
4	2, 3	ax-mp 5	. . . . 5 ⊢ Ord dom 𝑅1
5		ordsson 7716	. . . . 5 ⊢ (Ord dom 𝑅1 → dom 𝑅1 ⊆ On)
6	4, 5	ax-mp 5	. . . 4 ⊢ dom 𝑅1 ⊆ On
7		elfvdm 6856	. . . 4 ⊢ (𝐴 ∈ (𝑅1‘𝐵) → 𝐵 ∈ dom 𝑅1)
8	6, 7	sselid 3927	. . 3 ⊢ (𝐴 ∈ (𝑅1‘𝐵) → 𝐵 ∈ On)
9		onzsl 7776	. . 3 ⊢ (𝐵 ∈ On ↔ (𝐵 = ∅ ∨ ∃𝑥 ∈ On 𝐵 = suc 𝑥 ∨ (𝐵 ∈ V ∧ Lim 𝐵)))
10	8, 9	sylib 218	. 2 ⊢ (𝐴 ∈ (𝑅1‘𝐵) → (𝐵 = ∅ ∨ ∃𝑥 ∈ On 𝐵 = suc 𝑥 ∨ (𝐵 ∈ V ∧ Lim 𝐵)))
11		noel 4285	. . . . 5 ⊢ ¬ 𝐴 ∈ ∅
12		fveq2 6822	. . . . . . . 8 ⊢ (𝐵 = ∅ → (𝑅1‘𝐵) = (𝑅1‘∅))
13		r10 9661	. . . . . . . 8 ⊢ (𝑅1‘∅) = ∅
14	12, 13	eqtrdi 2782	. . . . . . 7 ⊢ (𝐵 = ∅ → (𝑅1‘𝐵) = ∅)
15	14	eleq2d 2817	. . . . . 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 6826	. . . . . . . . 9 ⊢ ((𝐴 ∈ (𝑅1‘𝐵) ∧ 𝐵 = suc 𝑥) → (𝑅1‘𝐵) = (𝑅1‘suc 𝑥))
22	7	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ (𝑅1‘𝐵) ∧ 𝐵 = suc 𝑥) → 𝐵 ∈ dom 𝑅1)
23	20, 22	eqeltrrd 2832	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ (𝑅1‘𝐵) ∧ 𝐵 = suc 𝑥) → suc 𝑥 ∈ dom 𝑅1)
24		limsuc 7779	. . . . . . . . . . . 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 9662	. . . . . . . . . 10 ⊢ (𝑥 ∈ dom 𝑅1 → (𝑅1‘suc 𝑥) = 𝒫 (𝑅1‘𝑥))
28	26, 27	syl 17	. . . . . . . . 9 ⊢ ((𝐴 ∈ (𝑅1‘𝐵) ∧ 𝐵 = suc 𝑥) → (𝑅1‘suc 𝑥) = 𝒫 (𝑅1‘𝑥))
29	21, 28	eqtrd 2766	. . . . . . . 8 ⊢ ((𝐴 ∈ (𝑅1‘𝐵) ∧ 𝐵 = suc 𝑥) → (𝑅1‘𝐵) = 𝒫 (𝑅1‘𝑥))
30	19, 29	eleqtrd 2833	. . . . . . 7 ⊢ ((𝐴 ∈ (𝑅1‘𝐵) ∧ 𝐵 = suc 𝑥) → 𝐴 ∈ 𝒫 (𝑅1‘𝑥))
31		elpwi 4554	. . . . . . 7 ⊢ (𝐴 ∈ 𝒫 (𝑅1‘𝑥) → 𝐴 ⊆ (𝑅1‘𝑥))
32		sspw 4558	. . . . . . 7 ⊢ (𝐴 ⊆ (𝑅1‘𝑥) → 𝒫 𝐴 ⊆ 𝒫 (𝑅1‘𝑥))
33	30, 31, 32	3syl 18	. . . . . 6 ⊢ ((𝐴 ∈ (𝑅1‘𝐵) ∧ 𝐵 = suc 𝑥) → 𝒫 𝐴 ⊆ 𝒫 (𝑅1‘𝑥))
34	33, 29	sseqtrrd 3967	. . . . 5 ⊢ ((𝐴 ∈ (𝑅1‘𝐵) ∧ 𝐵 = suc 𝑥) → 𝒫 𝐴 ⊆ (𝑅1‘𝐵))
35	34	ex 412	. . . 4 ⊢ (𝐴 ∈ (𝑅1‘𝐵) → (𝐵 = suc 𝑥 → 𝒫 𝐴 ⊆ (𝑅1‘𝐵)))
36	35	rexlimdvw 3138	. . 3 ⊢ (𝐴 ∈ (𝑅1‘𝐵) → (∃𝑥 ∈ On 𝐵 = suc 𝑥 → 𝒫 𝐴 ⊆ (𝑅1‘𝐵)))
37		r1tr 9669	. . . . . 6 ⊢ Tr (𝑅1‘𝐵)
38		simpl 482	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ (𝑅1‘𝐵) ∧ Lim 𝐵) → 𝐴 ∈ (𝑅1‘𝐵))
39		r1limg 9664	. . . . . . . . . . . 12 ⊢ ((𝐵 ∈ dom 𝑅1 ∧ Lim 𝐵) → (𝑅1‘𝐵) = ∪ 𝑥 ∈ 𝐵 (𝑅1‘𝑥))
40	7, 39	sylan 580	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ (𝑅1‘𝐵) ∧ Lim 𝐵) → (𝑅1‘𝐵) = ∪ 𝑥 ∈ 𝐵 (𝑅1‘𝑥))
41	38, 40	eleqtrd 2833	. . . . . . . . . 10 ⊢ ((𝐴 ∈ (𝑅1‘𝐵) ∧ Lim 𝐵) → 𝐴 ∈ ∪ 𝑥 ∈ 𝐵 (𝑅1‘𝑥))
42		eliun 4943	. . . . . . . . . 10 ⊢ (𝐴 ∈ ∪ 𝑥 ∈ 𝐵 (𝑅1‘𝑥) ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ (𝑅1‘𝑥))
43	41, 42	sylib 218	. . . . . . . . 9 ⊢ ((𝐴 ∈ (𝑅1‘𝐵) ∧ Lim 𝐵) → ∃𝑥 ∈ 𝐵 𝐴 ∈ (𝑅1‘𝑥))
44		simprl 770	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ (𝑅1‘𝐵) ∧ Lim 𝐵) ∧ (𝑥 ∈ 𝐵 ∧ 𝐴 ∈ (𝑅1‘𝑥))) → 𝑥 ∈ 𝐵)
45		limsuc 7779	. . . . . . . . . . . . 13 ⊢ (Lim 𝐵 → (𝑥 ∈ 𝐵 ↔ suc 𝑥 ∈ 𝐵))
46	45	ad2antlr 727	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ (𝑅1‘𝐵) ∧ Lim 𝐵) ∧ (𝑥 ∈ 𝐵 ∧ 𝐴 ∈ (𝑅1‘𝑥))) → (𝑥 ∈ 𝐵 ↔ suc 𝑥 ∈ 𝐵))
47	44, 46	mpbid 232	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ (𝑅1‘𝐵) ∧ Lim 𝐵) ∧ (𝑥 ∈ 𝐵 ∧ 𝐴 ∈ (𝑅1‘𝑥))) → suc 𝑥 ∈ 𝐵)
48		limsuc 7779	. . . . . . . . . . . 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 9669	. . . . . . . . . . . . . . 15 ⊢ Tr (𝑅1‘𝑥)
52		simprr 772	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ (𝑅1‘𝐵) ∧ Lim 𝐵) ∧ (𝑥 ∈ 𝐵 ∧ 𝐴 ∈ (𝑅1‘𝑥))) → 𝐴 ∈ (𝑅1‘𝑥))
53		trss 5206	. . . . . . . . . . . . . . 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 6350	. . . . . . . . . . . . . . . 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 3967	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ (𝑅1‘𝐵) ∧ Lim 𝐵) ∧ (𝑥 ∈ 𝐵 ∧ 𝐴 ∈ (𝑅1‘𝑥))) → 𝒫 𝐴 ⊆ (𝑅1‘suc 𝑥))
62		fvex 6835	. . . . . . . . . . . . 13 ⊢ (𝑅1‘suc 𝑥) ∈ V
63	62	elpw2 5270	. . . . . . . . . . . 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 9662	. . . . . . . . . . . 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 2834	. . . . . . . . . 10 ⊢ (((𝐴 ∈ (𝑅1‘𝐵) ∧ Lim 𝐵) ∧ (𝑥 ∈ 𝐵 ∧ 𝐴 ∈ (𝑅1‘𝑥))) → 𝒫 𝐴 ∈ (𝑅1‘suc suc 𝑥))
69		fveq2 6822	. . . . . . . . . . . 12 ⊢ (𝑦 = suc suc 𝑥 → (𝑅1‘𝑦) = (𝑅1‘suc suc 𝑥))
70	69	eleq2d 2817	. . . . . . . . . . 11 ⊢ (𝑦 = suc suc 𝑥 → (𝒫 𝐴 ∈ (𝑅1‘𝑦) ↔ 𝒫 𝐴 ∈ (𝑅1‘suc suc 𝑥)))
71	70	rspcev 3572	. . . . . . . . . 10 ⊢ ((suc suc 𝑥 ∈ 𝐵 ∧ 𝒫 𝐴 ∈ (𝑅1‘suc suc 𝑥)) → ∃𝑦 ∈ 𝐵 𝒫 𝐴 ∈ (𝑅1‘𝑦))
72	50, 68, 71	syl2anc 584	. . . . . . . . 9 ⊢ (((𝐴 ∈ (𝑅1‘𝐵) ∧ Lim 𝐵) ∧ (𝑥 ∈ 𝐵 ∧ 𝐴 ∈ (𝑅1‘𝑥))) → ∃𝑦 ∈ 𝐵 𝒫 𝐴 ∈ (𝑅1‘𝑦))
73	43, 72	rexlimddv 3139	. . . . . . . 8 ⊢ ((𝐴 ∈ (𝑅1‘𝐵) ∧ Lim 𝐵) → ∃𝑦 ∈ 𝐵 𝒫 𝐴 ∈ (𝑅1‘𝑦))
74		eliun 4943	. . . . . . . 8 ⊢ (𝒫 𝐴 ∈ ∪ 𝑦 ∈ 𝐵 (𝑅1‘𝑦) ↔ ∃𝑦 ∈ 𝐵 𝒫 𝐴 ∈ (𝑅1‘𝑦))
75	73, 74	sylibr 234	. . . . . . 7 ⊢ ((𝐴 ∈ (𝑅1‘𝐵) ∧ Lim 𝐵) → 𝒫 𝐴 ∈ ∪ 𝑦 ∈ 𝐵 (𝑅1‘𝑦))
76		r1limg 9664	. . . . . . . 8 ⊢ ((𝐵 ∈ dom 𝑅1 ∧ Lim 𝐵) → (𝑅1‘𝐵) = ∪ 𝑦 ∈ 𝐵 (𝑅1‘𝑦))
77	7, 76	sylan 580	. . . . . . 7 ⊢ ((𝐴 ∈ (𝑅1‘𝐵) ∧ Lim 𝐵) → (𝑅1‘𝐵) = ∪ 𝑦 ∈ 𝐵 (𝑅1‘𝑦))
78	75, 77	eleqtrrd 2834	. . . . . 6 ⊢ ((𝐴 ∈ (𝑅1‘𝐵) ∧ Lim 𝐵) → 𝒫 𝐴 ∈ (𝑅1‘𝐵))
79		trss 5206	. . . . . 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 1541   ∈ wcel 2111  ∃wrex 3056  Vcvv 3436   ⊆ wss 3897  ∅c0 4280  𝒫 cpw 4547  ∪ ciun 4939  Tr wtr 5196  dom cdm 5614  Ord word 6305  Oncon0 6306  Lim wlim 6307  suc csuc 6308  Fun wfun 6475  ‘cfv 6481  𝑅₁cr1 9655

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5232  ax-nul 5242  ax-pow 5301  ax-pr 5368  ax-un 7668

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-ral 3048  df-rex 3057  df-reu 3347  df-rab 3396  df-v 3438  df-sbc 3737  df-csb 3846  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-pss 3917  df-nul 4281  df-if 4473  df-pw 4549  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4857  df-iun 4941  df-br 5090  df-opab 5152  df-mpt 5171  df-tr 5197  df-id 5509  df-eprel 5514  df-po 5522  df-so 5523  df-fr 5567  df-we 5569  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-rn 5625  df-res 5626  df-ima 5627  df-pred 6248  df-ord 6309  df-on 6310  df-lim 6311  df-suc 6312  df-iota 6437  df-fun 6483  df-fn 6484  df-f 6485  df-f1 6486  df-fo 6487  df-f1o 6488  df-fv 6489  df-ov 7349  df-om 7797  df-2nd 7922  df-frecs 8211  df-wrecs 8242  df-recs 8291  df-rdg 8329  df-r1 9657

This theorem is referenced by:  r1sscl  9678  r1omfi  35116