Theorem r1pwss 9801

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 9783	. . . . . . 7 ⊢ (Fun 𝑅1 ∧ Lim dom 𝑅1)
2	1	simpri 485	. . . . . 6 ⊢ Lim dom 𝑅1
3		limord 6423	. . . . . 6 ⊢ (Lim dom 𝑅1 → Ord dom 𝑅1)
4	2, 3	ax-mp 5	. . . . 5 ⊢ Ord dom 𝑅1
5		ordsson 7779	. . . . 5 ⊢ (Ord dom 𝑅1 → dom 𝑅1 ⊆ On)
6	4, 5	ax-mp 5	. . . 4 ⊢ dom 𝑅1 ⊆ On
7		elfvdm 6928	. . . 4 ⊢ (𝐴 ∈ (𝑅1‘𝐵) → 𝐵 ∈ dom 𝑅1)
8	6, 7	sselid 3976	. . 3 ⊢ (𝐴 ∈ (𝑅1‘𝐵) → 𝐵 ∈ On)
9		onzsl 7844	. . 3 ⊢ (𝐵 ∈ On ↔ (𝐵 = ∅ ∨ ∃𝑥 ∈ On 𝐵 = suc 𝑥 ∨ (𝐵 ∈ V ∧ Lim 𝐵)))
10	8, 9	sylib 217	. 2 ⊢ (𝐴 ∈ (𝑅1‘𝐵) → (𝐵 = ∅ ∨ ∃𝑥 ∈ On 𝐵 = suc 𝑥 ∨ (𝐵 ∈ V ∧ Lim 𝐵)))
11		noel 4326	. . . . 5 ⊢ ¬ 𝐴 ∈ ∅
12		fveq2 6891	. . . . . . . 8 ⊢ (𝐵 = ∅ → (𝑅1‘𝐵) = (𝑅1‘∅))
13		r10 9785	. . . . . . . 8 ⊢ (𝑅1‘∅) = ∅
14	12, 13	eqtrdi 2783	. . . . . . 7 ⊢ (𝐵 = ∅ → (𝑅1‘𝐵) = ∅)
15	14	eleq2d 2814	. . . . . 6 ⊢ (𝐵 = ∅ → (𝐴 ∈ (𝑅1‘𝐵) ↔ 𝐴 ∈ ∅))
16	15	biimpcd 248	. . . . 5 ⊢ (𝐴 ∈ (𝑅1‘𝐵) → (𝐵 = ∅ → 𝐴 ∈ ∅))
17	11, 16	mtoi 198	. . . 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 6895	. . . . . . . . 9 ⊢ ((𝐴 ∈ (𝑅1‘𝐵) ∧ 𝐵 = suc 𝑥) → (𝑅1‘𝐵) = (𝑅1‘suc 𝑥))
22	7	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ (𝑅1‘𝐵) ∧ 𝐵 = suc 𝑥) → 𝐵 ∈ dom 𝑅1)
23	20, 22	eqeltrrd 2829	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ (𝑅1‘𝐵) ∧ 𝐵 = suc 𝑥) → suc 𝑥 ∈ dom 𝑅1)
24		limsuc 7847	. . . . . . . . . . . 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 233	. . . . . . . . . 10 ⊢ ((𝐴 ∈ (𝑅1‘𝐵) ∧ 𝐵 = suc 𝑥) → 𝑥 ∈ dom 𝑅1)
27		r1sucg 9786	. . . . . . . . . 10 ⊢ (𝑥 ∈ dom 𝑅1 → (𝑅1‘suc 𝑥) = 𝒫 (𝑅1‘𝑥))
28	26, 27	syl 17	. . . . . . . . 9 ⊢ ((𝐴 ∈ (𝑅1‘𝐵) ∧ 𝐵 = suc 𝑥) → (𝑅1‘suc 𝑥) = 𝒫 (𝑅1‘𝑥))
29	21, 28	eqtrd 2767	. . . . . . . 8 ⊢ ((𝐴 ∈ (𝑅1‘𝐵) ∧ 𝐵 = suc 𝑥) → (𝑅1‘𝐵) = 𝒫 (𝑅1‘𝑥))
30	19, 29	eleqtrd 2830	. . . . . . 7 ⊢ ((𝐴 ∈ (𝑅1‘𝐵) ∧ 𝐵 = suc 𝑥) → 𝐴 ∈ 𝒫 (𝑅1‘𝑥))
31		elpwi 4605	. . . . . . 7 ⊢ (𝐴 ∈ 𝒫 (𝑅1‘𝑥) → 𝐴 ⊆ (𝑅1‘𝑥))
32		sspw 4609	. . . . . . 7 ⊢ (𝐴 ⊆ (𝑅1‘𝑥) → 𝒫 𝐴 ⊆ 𝒫 (𝑅1‘𝑥))
33	30, 31, 32	3syl 18	. . . . . 6 ⊢ ((𝐴 ∈ (𝑅1‘𝐵) ∧ 𝐵 = suc 𝑥) → 𝒫 𝐴 ⊆ 𝒫 (𝑅1‘𝑥))
34	33, 29	sseqtrrd 4019	. . . . 5 ⊢ ((𝐴 ∈ (𝑅1‘𝐵) ∧ 𝐵 = suc 𝑥) → 𝒫 𝐴 ⊆ (𝑅1‘𝐵))
35	34	ex 412	. . . 4 ⊢ (𝐴 ∈ (𝑅1‘𝐵) → (𝐵 = suc 𝑥 → 𝒫 𝐴 ⊆ (𝑅1‘𝐵)))
36	35	rexlimdvw 3155	. . 3 ⊢ (𝐴 ∈ (𝑅1‘𝐵) → (∃𝑥 ∈ On 𝐵 = suc 𝑥 → 𝒫 𝐴 ⊆ (𝑅1‘𝐵)))
37		r1tr 9793	. . . . . 6 ⊢ Tr (𝑅1‘𝐵)
38		simpl 482	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ (𝑅1‘𝐵) ∧ Lim 𝐵) → 𝐴 ∈ (𝑅1‘𝐵))
39		r1limg 9788	. . . . . . . . . . . 12 ⊢ ((𝐵 ∈ dom 𝑅1 ∧ Lim 𝐵) → (𝑅1‘𝐵) = ∪ 𝑥 ∈ 𝐵 (𝑅1‘𝑥))
40	7, 39	sylan 579	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ (𝑅1‘𝐵) ∧ Lim 𝐵) → (𝑅1‘𝐵) = ∪ 𝑥 ∈ 𝐵 (𝑅1‘𝑥))
41	38, 40	eleqtrd 2830	. . . . . . . . . 10 ⊢ ((𝐴 ∈ (𝑅1‘𝐵) ∧ Lim 𝐵) → 𝐴 ∈ ∪ 𝑥 ∈ 𝐵 (𝑅1‘𝑥))
42		eliun 4995	. . . . . . . . . 10 ⊢ (𝐴 ∈ ∪ 𝑥 ∈ 𝐵 (𝑅1‘𝑥) ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ (𝑅1‘𝑥))
43	41, 42	sylib 217	. . . . . . . . 9 ⊢ ((𝐴 ∈ (𝑅1‘𝐵) ∧ Lim 𝐵) → ∃𝑥 ∈ 𝐵 𝐴 ∈ (𝑅1‘𝑥))
44		simprl 770	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ (𝑅1‘𝐵) ∧ Lim 𝐵) ∧ (𝑥 ∈ 𝐵 ∧ 𝐴 ∈ (𝑅1‘𝑥))) → 𝑥 ∈ 𝐵)
45		limsuc 7847	. . . . . . . . . . . . 13 ⊢ (Lim 𝐵 → (𝑥 ∈ 𝐵 ↔ suc 𝑥 ∈ 𝐵))
46	45	ad2antlr 726	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ (𝑅1‘𝐵) ∧ Lim 𝐵) ∧ (𝑥 ∈ 𝐵 ∧ 𝐴 ∈ (𝑅1‘𝑥))) → (𝑥 ∈ 𝐵 ↔ suc 𝑥 ∈ 𝐵))
47	44, 46	mpbid 231	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ (𝑅1‘𝐵) ∧ Lim 𝐵) ∧ (𝑥 ∈ 𝐵 ∧ 𝐴 ∈ (𝑅1‘𝑥))) → suc 𝑥 ∈ 𝐵)
48		limsuc 7847	. . . . . . . . . . . 12 ⊢ (Lim 𝐵 → (suc 𝑥 ∈ 𝐵 ↔ suc suc 𝑥 ∈ 𝐵))
49	48	ad2antlr 726	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ (𝑅1‘𝐵) ∧ Lim 𝐵) ∧ (𝑥 ∈ 𝐵 ∧ 𝐴 ∈ (𝑅1‘𝑥))) → (suc 𝑥 ∈ 𝐵 ↔ suc suc 𝑥 ∈ 𝐵))
50	47, 49	mpbid 231	. . . . . . . . . 10 ⊢ (((𝐴 ∈ (𝑅1‘𝐵) ∧ Lim 𝐵) ∧ (𝑥 ∈ 𝐵 ∧ 𝐴 ∈ (𝑅1‘𝑥))) → suc suc 𝑥 ∈ 𝐵)
51		r1tr 9793	. . . . . . . . . . . . . . 15 ⊢ Tr (𝑅1‘𝑥)
52		simprr 772	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ (𝑅1‘𝐵) ∧ Lim 𝐵) ∧ (𝑥 ∈ 𝐵 ∧ 𝐴 ∈ (𝑅1‘𝑥))) → 𝐴 ∈ (𝑅1‘𝑥))
53		trss 5270	. . . . . . . . . . . . . . 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 725	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ (𝑅1‘𝐵) ∧ Lim 𝐵) ∧ (𝑥 ∈ 𝐵 ∧ 𝐴 ∈ (𝑅1‘𝑥))) → 𝐵 ∈ dom 𝑅1)
57		ordtr1 6406	. . . . . . . . . . . . . . . 16 ⊢ (Ord dom 𝑅1 → ((𝑥 ∈ 𝐵 ∧ 𝐵 ∈ dom 𝑅1) → 𝑥 ∈ dom 𝑅1))
58	4, 57	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ 𝐵 ∧ 𝐵 ∈ dom 𝑅1) → 𝑥 ∈ dom 𝑅1)
59	44, 56, 58	syl2anc 583	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ (𝑅1‘𝐵) ∧ Lim 𝐵) ∧ (𝑥 ∈ 𝐵 ∧ 𝐴 ∈ (𝑅1‘𝑥))) → 𝑥 ∈ dom 𝑅1)
60	59, 27	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ (𝑅1‘𝐵) ∧ Lim 𝐵) ∧ (𝑥 ∈ 𝐵 ∧ 𝐴 ∈ (𝑅1‘𝑥))) → (𝑅1‘suc 𝑥) = 𝒫 (𝑅1‘𝑥))
61	55, 60	sseqtrrd 4019	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ (𝑅1‘𝐵) ∧ Lim 𝐵) ∧ (𝑥 ∈ 𝐵 ∧ 𝐴 ∈ (𝑅1‘𝑥))) → 𝒫 𝐴 ⊆ (𝑅1‘suc 𝑥))
62		fvex 6904	. . . . . . . . . . . . 13 ⊢ (𝑅1‘suc 𝑥) ∈ V
63	62	elpw2 5341	. . . . . . . . . . . 12 ⊢ (𝒫 𝐴 ∈ 𝒫 (𝑅1‘suc 𝑥) ↔ 𝒫 𝐴 ⊆ (𝑅1‘suc 𝑥))
64	61, 63	sylibr 233	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ (𝑅1‘𝐵) ∧ Lim 𝐵) ∧ (𝑥 ∈ 𝐵 ∧ 𝐴 ∈ (𝑅1‘𝑥))) → 𝒫 𝐴 ∈ 𝒫 (𝑅1‘suc 𝑥))
65	59, 25	sylib 217	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ (𝑅1‘𝐵) ∧ Lim 𝐵) ∧ (𝑥 ∈ 𝐵 ∧ 𝐴 ∈ (𝑅1‘𝑥))) → suc 𝑥 ∈ dom 𝑅1)
66		r1sucg 9786	. . . . . . . . . . . 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 2831	. . . . . . . . . 10 ⊢ (((𝐴 ∈ (𝑅1‘𝐵) ∧ Lim 𝐵) ∧ (𝑥 ∈ 𝐵 ∧ 𝐴 ∈ (𝑅1‘𝑥))) → 𝒫 𝐴 ∈ (𝑅1‘suc suc 𝑥))
69		fveq2 6891	. . . . . . . . . . . 12 ⊢ (𝑦 = suc suc 𝑥 → (𝑅1‘𝑦) = (𝑅1‘suc suc 𝑥))
70	69	eleq2d 2814	. . . . . . . . . . 11 ⊢ (𝑦 = suc suc 𝑥 → (𝒫 𝐴 ∈ (𝑅1‘𝑦) ↔ 𝒫 𝐴 ∈ (𝑅1‘suc suc 𝑥)))
71	70	rspcev 3607	. . . . . . . . . 10 ⊢ ((suc suc 𝑥 ∈ 𝐵 ∧ 𝒫 𝐴 ∈ (𝑅1‘suc suc 𝑥)) → ∃𝑦 ∈ 𝐵 𝒫 𝐴 ∈ (𝑅1‘𝑦))
72	50, 68, 71	syl2anc 583	. . . . . . . . 9 ⊢ (((𝐴 ∈ (𝑅1‘𝐵) ∧ Lim 𝐵) ∧ (𝑥 ∈ 𝐵 ∧ 𝐴 ∈ (𝑅1‘𝑥))) → ∃𝑦 ∈ 𝐵 𝒫 𝐴 ∈ (𝑅1‘𝑦))
73	43, 72	rexlimddv 3156	. . . . . . . 8 ⊢ ((𝐴 ∈ (𝑅1‘𝐵) ∧ Lim 𝐵) → ∃𝑦 ∈ 𝐵 𝒫 𝐴 ∈ (𝑅1‘𝑦))
74		eliun 4995	. . . . . . . 8 ⊢ (𝒫 𝐴 ∈ ∪ 𝑦 ∈ 𝐵 (𝑅1‘𝑦) ↔ ∃𝑦 ∈ 𝐵 𝒫 𝐴 ∈ (𝑅1‘𝑦))
75	73, 74	sylibr 233	. . . . . . 7 ⊢ ((𝐴 ∈ (𝑅1‘𝐵) ∧ Lim 𝐵) → 𝒫 𝐴 ∈ ∪ 𝑦 ∈ 𝐵 (𝑅1‘𝑦))
76		r1limg 9788	. . . . . . . 8 ⊢ ((𝐵 ∈ dom 𝑅1 ∧ Lim 𝐵) → (𝑅1‘𝐵) = ∪ 𝑦 ∈ 𝐵 (𝑅1‘𝑦))
77	7, 76	sylan 579	. . . . . . 7 ⊢ ((𝐴 ∈ (𝑅1‘𝐵) ∧ Lim 𝐵) → (𝑅1‘𝐵) = ∪ 𝑦 ∈ 𝐵 (𝑅1‘𝑦))
78	75, 77	eleqtrrd 2831	. . . . . 6 ⊢ ((𝐴 ∈ (𝑅1‘𝐵) ∧ Lim 𝐵) → 𝒫 𝐴 ∈ (𝑅1‘𝐵))
79		trss 5270	. . . . . 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 1426	. 2 ⊢ (𝐴 ∈ (𝑅1‘𝐵) → ((𝐵 = ∅ ∨ ∃𝑥 ∈ On 𝐵 = suc 𝑥 ∨ (𝐵 ∈ V ∧ Lim 𝐵)) → 𝒫 𝐴 ⊆ (𝑅1‘𝐵)))
84	10, 83	mpd 15	1 ⊢ (𝐴 ∈ (𝑅1‘𝐵) → 𝒫 𝐴 ⊆ (𝑅1‘𝐵))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   ∨ w3o 1084   = wceq 1534   ∈ wcel 2099  ∃wrex 3065  Vcvv 3469   ⊆ wss 3944  ∅c0 4318  𝒫 cpw 4598  ∪ ciun 4991  Tr wtr 5259  dom cdm 5672  Ord word 6362  Oncon0 6363  Lim wlim 6364  suc csuc 6365  Fun wfun 6536  ‘cfv 6542  𝑅₁cr1 9779

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2164  ax-ext 2698  ax-sep 5293  ax-nul 5300  ax-pow 5359  ax-pr 5423  ax-un 7734

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2705  df-cleq 2719  df-clel 2805  df-nfc 2880  df-ne 2936  df-ral 3057  df-rex 3066  df-reu 3372  df-rab 3428  df-v 3471  df-sbc 3775  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3963  df-nul 4319  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4904  df-iun 4993  df-br 5143  df-opab 5205  df-mpt 5226  df-tr 5260  df-id 5570  df-eprel 5576  df-po 5584  df-so 5585  df-fr 5627  df-we 5629  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-pred 6299  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-ov 7417  df-om 7865  df-2nd 7988  df-frecs 8280  df-wrecs 8311  df-recs 8385  df-rdg 8424  df-r1 9781

This theorem is referenced by:  r1sscl  9802