Theorem r1pwss 9708

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 9690	. . . . . . 7 ⊢ (Fun 𝑅1 ∧ Lim dom 𝑅1)
2	1	simpri 485	. . . . . 6 ⊢ Lim dom 𝑅1
3		limord 6386	. . . . . 6 ⊢ (Lim dom 𝑅1 → Ord dom 𝑅1)
4	2, 3	ax-mp 5	. . . . 5 ⊢ Ord dom 𝑅1
5		ordsson 7738	. . . . 5 ⊢ (Ord dom 𝑅1 → dom 𝑅1 ⊆ On)
6	4, 5	ax-mp 5	. . . 4 ⊢ dom 𝑅1 ⊆ On
7		elfvdm 6876	. . . 4 ⊢ (𝐴 ∈ (𝑅1‘𝐵) → 𝐵 ∈ dom 𝑅1)
8	6, 7	sselid 3933	. . 3 ⊢ (𝐴 ∈ (𝑅1‘𝐵) → 𝐵 ∈ On)
9		onzsl 7798	. . 3 ⊢ (𝐵 ∈ On ↔ (𝐵 = ∅ ∨ ∃𝑥 ∈ On 𝐵 = suc 𝑥 ∨ (𝐵 ∈ V ∧ Lim 𝐵)))
10	8, 9	sylib 218	. 2 ⊢ (𝐴 ∈ (𝑅1‘𝐵) → (𝐵 = ∅ ∨ ∃𝑥 ∈ On 𝐵 = suc 𝑥 ∨ (𝐵 ∈ V ∧ Lim 𝐵)))
11		noel 4292	. . . . 5 ⊢ ¬ 𝐴 ∈ ∅
12		fveq2 6842	. . . . . . . 8 ⊢ (𝐵 = ∅ → (𝑅1‘𝐵) = (𝑅1‘∅))
13		r10 9692	. . . . . . . 8 ⊢ (𝑅1‘∅) = ∅
14	12, 13	eqtrdi 2788	. . . . . . 7 ⊢ (𝐵 = ∅ → (𝑅1‘𝐵) = ∅)
15	14	eleq2d 2823	. . . . . 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 6846	. . . . . . . . 9 ⊢ ((𝐴 ∈ (𝑅1‘𝐵) ∧ 𝐵 = suc 𝑥) → (𝑅1‘𝐵) = (𝑅1‘suc 𝑥))
22	7	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ (𝑅1‘𝐵) ∧ 𝐵 = suc 𝑥) → 𝐵 ∈ dom 𝑅1)
23	20, 22	eqeltrrd 2838	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ (𝑅1‘𝐵) ∧ 𝐵 = suc 𝑥) → suc 𝑥 ∈ dom 𝑅1)
24		limsuc 7801	. . . . . . . . . . . 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 9693	. . . . . . . . . 10 ⊢ (𝑥 ∈ dom 𝑅1 → (𝑅1‘suc 𝑥) = 𝒫 (𝑅1‘𝑥))
28	26, 27	syl 17	. . . . . . . . 9 ⊢ ((𝐴 ∈ (𝑅1‘𝐵) ∧ 𝐵 = suc 𝑥) → (𝑅1‘suc 𝑥) = 𝒫 (𝑅1‘𝑥))
29	21, 28	eqtrd 2772	. . . . . . . 8 ⊢ ((𝐴 ∈ (𝑅1‘𝐵) ∧ 𝐵 = suc 𝑥) → (𝑅1‘𝐵) = 𝒫 (𝑅1‘𝑥))
30	19, 29	eleqtrd 2839	. . . . . . 7 ⊢ ((𝐴 ∈ (𝑅1‘𝐵) ∧ 𝐵 = suc 𝑥) → 𝐴 ∈ 𝒫 (𝑅1‘𝑥))
31		elpwi 4563	. . . . . . 7 ⊢ (𝐴 ∈ 𝒫 (𝑅1‘𝑥) → 𝐴 ⊆ (𝑅1‘𝑥))
32		sspw 4567	. . . . . . 7 ⊢ (𝐴 ⊆ (𝑅1‘𝑥) → 𝒫 𝐴 ⊆ 𝒫 (𝑅1‘𝑥))
33	30, 31, 32	3syl 18	. . . . . 6 ⊢ ((𝐴 ∈ (𝑅1‘𝐵) ∧ 𝐵 = suc 𝑥) → 𝒫 𝐴 ⊆ 𝒫 (𝑅1‘𝑥))
34	33, 29	sseqtrrd 3973	. . . . 5 ⊢ ((𝐴 ∈ (𝑅1‘𝐵) ∧ 𝐵 = suc 𝑥) → 𝒫 𝐴 ⊆ (𝑅1‘𝐵))
35	34	ex 412	. . . 4 ⊢ (𝐴 ∈ (𝑅1‘𝐵) → (𝐵 = suc 𝑥 → 𝒫 𝐴 ⊆ (𝑅1‘𝐵)))
36	35	rexlimdvw 3144	. . 3 ⊢ (𝐴 ∈ (𝑅1‘𝐵) → (∃𝑥 ∈ On 𝐵 = suc 𝑥 → 𝒫 𝐴 ⊆ (𝑅1‘𝐵)))
37		r1tr 9700	. . . . . 6 ⊢ Tr (𝑅1‘𝐵)
38		simpl 482	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ (𝑅1‘𝐵) ∧ Lim 𝐵) → 𝐴 ∈ (𝑅1‘𝐵))
39		r1limg 9695	. . . . . . . . . . . 12 ⊢ ((𝐵 ∈ dom 𝑅1 ∧ Lim 𝐵) → (𝑅1‘𝐵) = ∪ 𝑥 ∈ 𝐵 (𝑅1‘𝑥))
40	7, 39	sylan 581	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ (𝑅1‘𝐵) ∧ Lim 𝐵) → (𝑅1‘𝐵) = ∪ 𝑥 ∈ 𝐵 (𝑅1‘𝑥))
41	38, 40	eleqtrd 2839	. . . . . . . . . 10 ⊢ ((𝐴 ∈ (𝑅1‘𝐵) ∧ Lim 𝐵) → 𝐴 ∈ ∪ 𝑥 ∈ 𝐵 (𝑅1‘𝑥))
42		eliun 4952	. . . . . . . . . 10 ⊢ (𝐴 ∈ ∪ 𝑥 ∈ 𝐵 (𝑅1‘𝑥) ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ (𝑅1‘𝑥))
43	41, 42	sylib 218	. . . . . . . . 9 ⊢ ((𝐴 ∈ (𝑅1‘𝐵) ∧ Lim 𝐵) → ∃𝑥 ∈ 𝐵 𝐴 ∈ (𝑅1‘𝑥))
44		simprl 771	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ (𝑅1‘𝐵) ∧ Lim 𝐵) ∧ (𝑥 ∈ 𝐵 ∧ 𝐴 ∈ (𝑅1‘𝑥))) → 𝑥 ∈ 𝐵)
45		limsuc 7801	. . . . . . . . . . . . 13 ⊢ (Lim 𝐵 → (𝑥 ∈ 𝐵 ↔ suc 𝑥 ∈ 𝐵))
46	45	ad2antlr 728	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ (𝑅1‘𝐵) ∧ Lim 𝐵) ∧ (𝑥 ∈ 𝐵 ∧ 𝐴 ∈ (𝑅1‘𝑥))) → (𝑥 ∈ 𝐵 ↔ suc 𝑥 ∈ 𝐵))
47	44, 46	mpbid 232	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ (𝑅1‘𝐵) ∧ Lim 𝐵) ∧ (𝑥 ∈ 𝐵 ∧ 𝐴 ∈ (𝑅1‘𝑥))) → suc 𝑥 ∈ 𝐵)
48		limsuc 7801	. . . . . . . . . . . 12 ⊢ (Lim 𝐵 → (suc 𝑥 ∈ 𝐵 ↔ suc suc 𝑥 ∈ 𝐵))
49	48	ad2antlr 728	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ (𝑅1‘𝐵) ∧ Lim 𝐵) ∧ (𝑥 ∈ 𝐵 ∧ 𝐴 ∈ (𝑅1‘𝑥))) → (suc 𝑥 ∈ 𝐵 ↔ suc suc 𝑥 ∈ 𝐵))
50	47, 49	mpbid 232	. . . . . . . . . 10 ⊢ (((𝐴 ∈ (𝑅1‘𝐵) ∧ Lim 𝐵) ∧ (𝑥 ∈ 𝐵 ∧ 𝐴 ∈ (𝑅1‘𝑥))) → suc suc 𝑥 ∈ 𝐵)
51		r1tr 9700	. . . . . . . . . . . . . . 15 ⊢ Tr (𝑅1‘𝑥)
52		simprr 773	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ (𝑅1‘𝐵) ∧ Lim 𝐵) ∧ (𝑥 ∈ 𝐵 ∧ 𝐴 ∈ (𝑅1‘𝑥))) → 𝐴 ∈ (𝑅1‘𝑥))
53		trss 5217	. . . . . . . . . . . . . . 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 727	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ (𝑅1‘𝐵) ∧ Lim 𝐵) ∧ (𝑥 ∈ 𝐵 ∧ 𝐴 ∈ (𝑅1‘𝑥))) → 𝐵 ∈ dom 𝑅1)
57		ordtr1 6369	. . . . . . . . . . . . . . . 16 ⊢ (Ord dom 𝑅1 → ((𝑥 ∈ 𝐵 ∧ 𝐵 ∈ dom 𝑅1) → 𝑥 ∈ dom 𝑅1))
58	4, 57	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ 𝐵 ∧ 𝐵 ∈ dom 𝑅1) → 𝑥 ∈ dom 𝑅1)
59	44, 56, 58	syl2anc 585	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ (𝑅1‘𝐵) ∧ Lim 𝐵) ∧ (𝑥 ∈ 𝐵 ∧ 𝐴 ∈ (𝑅1‘𝑥))) → 𝑥 ∈ dom 𝑅1)
60	59, 27	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ (𝑅1‘𝐵) ∧ Lim 𝐵) ∧ (𝑥 ∈ 𝐵 ∧ 𝐴 ∈ (𝑅1‘𝑥))) → (𝑅1‘suc 𝑥) = 𝒫 (𝑅1‘𝑥))
61	55, 60	sseqtrrd 3973	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ (𝑅1‘𝐵) ∧ Lim 𝐵) ∧ (𝑥 ∈ 𝐵 ∧ 𝐴 ∈ (𝑅1‘𝑥))) → 𝒫 𝐴 ⊆ (𝑅1‘suc 𝑥))
62		fvex 6855	. . . . . . . . . . . . 13 ⊢ (𝑅1‘suc 𝑥) ∈ V
63	62	elpw2 5281	. . . . . . . . . . . 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 9693	. . . . . . . . . . . 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 2840	. . . . . . . . . 10 ⊢ (((𝐴 ∈ (𝑅1‘𝐵) ∧ Lim 𝐵) ∧ (𝑥 ∈ 𝐵 ∧ 𝐴 ∈ (𝑅1‘𝑥))) → 𝒫 𝐴 ∈ (𝑅1‘suc suc 𝑥))
69		fveq2 6842	. . . . . . . . . . . 12 ⊢ (𝑦 = suc suc 𝑥 → (𝑅1‘𝑦) = (𝑅1‘suc suc 𝑥))
70	69	eleq2d 2823	. . . . . . . . . . 11 ⊢ (𝑦 = suc suc 𝑥 → (𝒫 𝐴 ∈ (𝑅1‘𝑦) ↔ 𝒫 𝐴 ∈ (𝑅1‘suc suc 𝑥)))
71	70	rspcev 3578	. . . . . . . . . 10 ⊢ ((suc suc 𝑥 ∈ 𝐵 ∧ 𝒫 𝐴 ∈ (𝑅1‘suc suc 𝑥)) → ∃𝑦 ∈ 𝐵 𝒫 𝐴 ∈ (𝑅1‘𝑦))
72	50, 68, 71	syl2anc 585	. . . . . . . . 9 ⊢ (((𝐴 ∈ (𝑅1‘𝐵) ∧ Lim 𝐵) ∧ (𝑥 ∈ 𝐵 ∧ 𝐴 ∈ (𝑅1‘𝑥))) → ∃𝑦 ∈ 𝐵 𝒫 𝐴 ∈ (𝑅1‘𝑦))
73	43, 72	rexlimddv 3145	. . . . . . . 8 ⊢ ((𝐴 ∈ (𝑅1‘𝐵) ∧ Lim 𝐵) → ∃𝑦 ∈ 𝐵 𝒫 𝐴 ∈ (𝑅1‘𝑦))
74		eliun 4952	. . . . . . . 8 ⊢ (𝒫 𝐴 ∈ ∪ 𝑦 ∈ 𝐵 (𝑅1‘𝑦) ↔ ∃𝑦 ∈ 𝐵 𝒫 𝐴 ∈ (𝑅1‘𝑦))
75	73, 74	sylibr 234	. . . . . . 7 ⊢ ((𝐴 ∈ (𝑅1‘𝐵) ∧ Lim 𝐵) → 𝒫 𝐴 ∈ ∪ 𝑦 ∈ 𝐵 (𝑅1‘𝑦))
76		r1limg 9695	. . . . . . . 8 ⊢ ((𝐵 ∈ dom 𝑅1 ∧ Lim 𝐵) → (𝑅1‘𝐵) = ∪ 𝑦 ∈ 𝐵 (𝑅1‘𝑦))
77	7, 76	sylan 581	. . . . . . 7 ⊢ ((𝐴 ∈ (𝑅1‘𝐵) ∧ Lim 𝐵) → (𝑅1‘𝐵) = ∪ 𝑦 ∈ 𝐵 (𝑅1‘𝑦))
78	75, 77	eleqtrrd 2840	. . . . . 6 ⊢ ((𝐴 ∈ (𝑅1‘𝐵) ∧ Lim 𝐵) → 𝒫 𝐴 ∈ (𝑅1‘𝐵))
79		trss 5217	. . . . . 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 1432	. 2 ⊢ (𝐴 ∈ (𝑅1‘𝐵) → ((𝐵 = ∅ ∨ ∃𝑥 ∈ On 𝐵 = suc 𝑥 ∨ (𝐵 ∈ V ∧ Lim 𝐵)) → 𝒫 𝐴 ⊆ (𝑅1‘𝐵)))
84	10, 83	mpd 15	1 ⊢ (𝐴 ∈ (𝑅1‘𝐵) → 𝒫 𝐴 ⊆ (𝑅1‘𝐵))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∨ w3o 1086   = wceq 1542   ∈ wcel 2114  ∃wrex 3062  Vcvv 3442   ⊆ wss 3903  ∅c0 4287  𝒫 cpw 4556  ∪ ciun 4948  Tr wtr 5207  dom cdm 5632  Ord word 6324  Oncon0 6325  Lim wlim 6326  suc csuc 6327  Fun wfun 6494  ‘cfv 6500  𝑅₁cr1 9686

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5243  ax-nul 5253  ax-pow 5312  ax-pr 5379  ax-un 7690

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-reu 3353  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-iun 4950  df-br 5101  df-opab 5163  df-mpt 5182  df-tr 5208  df-id 5527  df-eprel 5532  df-po 5540  df-so 5541  df-fr 5585  df-we 5587  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-pred 6267  df-ord 6328  df-on 6329  df-lim 6330  df-suc 6331  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-ov 7371  df-om 7819  df-2nd 7944  df-frecs 8233  df-wrecs 8264  df-recs 8313  df-rdg 8351  df-r1 9688

This theorem is referenced by:  r1sscl  9709  r1omfi  35282