Theorem r1pwss 9680

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 9662	. . . . . . 7 ⊢ (Fun 𝑅1 ∧ Lim dom 𝑅1)
2	1	simpri 485	. . . . . 6 ⊢ Lim dom 𝑅1
3		limord 6368	. . . . . 6 ⊢ (Lim dom 𝑅1 → Ord dom 𝑅1)
4	2, 3	ax-mp 5	. . . . 5 ⊢ Ord dom 𝑅1
5		ordsson 7719	. . . . 5 ⊢ (Ord dom 𝑅1 → dom 𝑅1 ⊆ On)
6	4, 5	ax-mp 5	. . . 4 ⊢ dom 𝑅1 ⊆ On
7		elfvdm 6857	. . . 4 ⊢ (𝐴 ∈ (𝑅1‘𝐵) → 𝐵 ∈ dom 𝑅1)
8	6, 7	sselid 3933	. . 3 ⊢ (𝐴 ∈ (𝑅1‘𝐵) → 𝐵 ∈ On)
9		onzsl 7779	. . 3 ⊢ (𝐵 ∈ On ↔ (𝐵 = ∅ ∨ ∃𝑥 ∈ On 𝐵 = suc 𝑥 ∨ (𝐵 ∈ V ∧ Lim 𝐵)))
10	8, 9	sylib 218	. 2 ⊢ (𝐴 ∈ (𝑅1‘𝐵) → (𝐵 = ∅ ∨ ∃𝑥 ∈ On 𝐵 = suc 𝑥 ∨ (𝐵 ∈ V ∧ Lim 𝐵)))
11		noel 4289	. . . . 5 ⊢ ¬ 𝐴 ∈ ∅
12		fveq2 6822	. . . . . . . 8 ⊢ (𝐵 = ∅ → (𝑅1‘𝐵) = (𝑅1‘∅))
13		r10 9664	. . . . . . . 8 ⊢ (𝑅1‘∅) = ∅
14	12, 13	eqtrdi 2780	. . . . . . 7 ⊢ (𝐵 = ∅ → (𝑅1‘𝐵) = ∅)
15	14	eleq2d 2814	. . . . . 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 2829	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ (𝑅1‘𝐵) ∧ 𝐵 = suc 𝑥) → suc 𝑥 ∈ dom 𝑅1)
24		limsuc 7782	. . . . . . . . . . . 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 9665	. . . . . . . . . 10 ⊢ (𝑥 ∈ dom 𝑅1 → (𝑅1‘suc 𝑥) = 𝒫 (𝑅1‘𝑥))
28	26, 27	syl 17	. . . . . . . . 9 ⊢ ((𝐴 ∈ (𝑅1‘𝐵) ∧ 𝐵 = suc 𝑥) → (𝑅1‘suc 𝑥) = 𝒫 (𝑅1‘𝑥))
29	21, 28	eqtrd 2764	. . . . . . . 8 ⊢ ((𝐴 ∈ (𝑅1‘𝐵) ∧ 𝐵 = suc 𝑥) → (𝑅1‘𝐵) = 𝒫 (𝑅1‘𝑥))
30	19, 29	eleqtrd 2830	. . . . . . 7 ⊢ ((𝐴 ∈ (𝑅1‘𝐵) ∧ 𝐵 = suc 𝑥) → 𝐴 ∈ 𝒫 (𝑅1‘𝑥))
31		elpwi 4558	. . . . . . 7 ⊢ (𝐴 ∈ 𝒫 (𝑅1‘𝑥) → 𝐴 ⊆ (𝑅1‘𝑥))
32		sspw 4562	. . . . . . 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 3135	. . 3 ⊢ (𝐴 ∈ (𝑅1‘𝐵) → (∃𝑥 ∈ On 𝐵 = suc 𝑥 → 𝒫 𝐴 ⊆ (𝑅1‘𝐵)))
37		r1tr 9672	. . . . . 6 ⊢ Tr (𝑅1‘𝐵)
38		simpl 482	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ (𝑅1‘𝐵) ∧ Lim 𝐵) → 𝐴 ∈ (𝑅1‘𝐵))
39		r1limg 9667	. . . . . . . . . . . 12 ⊢ ((𝐵 ∈ dom 𝑅1 ∧ Lim 𝐵) → (𝑅1‘𝐵) = ∪ 𝑥 ∈ 𝐵 (𝑅1‘𝑥))
40	7, 39	sylan 580	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ (𝑅1‘𝐵) ∧ Lim 𝐵) → (𝑅1‘𝐵) = ∪ 𝑥 ∈ 𝐵 (𝑅1‘𝑥))
41	38, 40	eleqtrd 2830	. . . . . . . . . 10 ⊢ ((𝐴 ∈ (𝑅1‘𝐵) ∧ Lim 𝐵) → 𝐴 ∈ ∪ 𝑥 ∈ 𝐵 (𝑅1‘𝑥))
42		eliun 4945	. . . . . . . . . 10 ⊢ (𝐴 ∈ ∪ 𝑥 ∈ 𝐵 (𝑅1‘𝑥) ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ (𝑅1‘𝑥))
43	41, 42	sylib 218	. . . . . . . . 9 ⊢ ((𝐴 ∈ (𝑅1‘𝐵) ∧ Lim 𝐵) → ∃𝑥 ∈ 𝐵 𝐴 ∈ (𝑅1‘𝑥))
44		simprl 770	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ (𝑅1‘𝐵) ∧ Lim 𝐵) ∧ (𝑥 ∈ 𝐵 ∧ 𝐴 ∈ (𝑅1‘𝑥))) → 𝑥 ∈ 𝐵)
45		limsuc 7782	. . . . . . . . . . . . 13 ⊢ (Lim 𝐵 → (𝑥 ∈ 𝐵 ↔ suc 𝑥 ∈ 𝐵))
46	45	ad2antlr 727	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ (𝑅1‘𝐵) ∧ Lim 𝐵) ∧ (𝑥 ∈ 𝐵 ∧ 𝐴 ∈ (𝑅1‘𝑥))) → (𝑥 ∈ 𝐵 ↔ suc 𝑥 ∈ 𝐵))
47	44, 46	mpbid 232	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ (𝑅1‘𝐵) ∧ Lim 𝐵) ∧ (𝑥 ∈ 𝐵 ∧ 𝐴 ∈ (𝑅1‘𝑥))) → suc 𝑥 ∈ 𝐵)
48		limsuc 7782	. . . . . . . . . . . 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 9672	. . . . . . . . . . . . . . 15 ⊢ Tr (𝑅1‘𝑥)
52		simprr 772	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ (𝑅1‘𝐵) ∧ Lim 𝐵) ∧ (𝑥 ∈ 𝐵 ∧ 𝐴 ∈ (𝑅1‘𝑥))) → 𝐴 ∈ (𝑅1‘𝑥))
53		trss 5209	. . . . . . . . . . . . . . 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 6351	. . . . . . . . . . . . . . . 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 3973	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ (𝑅1‘𝐵) ∧ Lim 𝐵) ∧ (𝑥 ∈ 𝐵 ∧ 𝐴 ∈ (𝑅1‘𝑥))) → 𝒫 𝐴 ⊆ (𝑅1‘suc 𝑥))
62		fvex 6835	. . . . . . . . . . . . 13 ⊢ (𝑅1‘suc 𝑥) ∈ V
63	62	elpw2 5273	. . . . . . . . . . . 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 9665	. . . . . . . . . . . 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 6822	. . . . . . . . . . . 12 ⊢ (𝑦 = suc suc 𝑥 → (𝑅1‘𝑦) = (𝑅1‘suc suc 𝑥))
70	69	eleq2d 2814	. . . . . . . . . . 11 ⊢ (𝑦 = suc suc 𝑥 → (𝒫 𝐴 ∈ (𝑅1‘𝑦) ↔ 𝒫 𝐴 ∈ (𝑅1‘suc suc 𝑥)))
71	70	rspcev 3577	. . . . . . . . . 10 ⊢ ((suc suc 𝑥 ∈ 𝐵 ∧ 𝒫 𝐴 ∈ (𝑅1‘suc suc 𝑥)) → ∃𝑦 ∈ 𝐵 𝒫 𝐴 ∈ (𝑅1‘𝑦))
72	50, 68, 71	syl2anc 584	. . . . . . . . 9 ⊢ (((𝐴 ∈ (𝑅1‘𝐵) ∧ Lim 𝐵) ∧ (𝑥 ∈ 𝐵 ∧ 𝐴 ∈ (𝑅1‘𝑥))) → ∃𝑦 ∈ 𝐵 𝒫 𝐴 ∈ (𝑅1‘𝑦))
73	43, 72	rexlimddv 3136	. . . . . . . 8 ⊢ ((𝐴 ∈ (𝑅1‘𝐵) ∧ Lim 𝐵) → ∃𝑦 ∈ 𝐵 𝒫 𝐴 ∈ (𝑅1‘𝑦))
74		eliun 4945	. . . . . . . 8 ⊢ (𝒫 𝐴 ∈ ∪ 𝑦 ∈ 𝐵 (𝑅1‘𝑦) ↔ ∃𝑦 ∈ 𝐵 𝒫 𝐴 ∈ (𝑅1‘𝑦))
75	73, 74	sylibr 234	. . . . . . 7 ⊢ ((𝐴 ∈ (𝑅1‘𝐵) ∧ Lim 𝐵) → 𝒫 𝐴 ∈ ∪ 𝑦 ∈ 𝐵 (𝑅1‘𝑦))
76		r1limg 9667	. . . . . . . 8 ⊢ ((𝐵 ∈ dom 𝑅1 ∧ Lim 𝐵) → (𝑅1‘𝐵) = ∪ 𝑦 ∈ 𝐵 (𝑅1‘𝑦))
77	7, 76	sylan 580	. . . . . . 7 ⊢ ((𝐴 ∈ (𝑅1‘𝐵) ∧ Lim 𝐵) → (𝑅1‘𝐵) = ∪ 𝑦 ∈ 𝐵 (𝑅1‘𝑦))
78	75, 77	eleqtrrd 2831	. . . . . 6 ⊢ ((𝐴 ∈ (𝑅1‘𝐵) ∧ Lim 𝐵) → 𝒫 𝐴 ∈ (𝑅1‘𝐵))
79		trss 5209	. . . . . 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 2109  ∃wrex 3053  Vcvv 3436   ⊆ wss 3903  ∅c0 4284  𝒫 cpw 4551  ∪ ciun 4941  Tr wtr 5199  dom cdm 5619  Ord word 6306  Oncon0 6307  Lim wlim 6308  suc csuc 6309  Fun wfun 6476  ‘cfv 6482  𝑅₁cr1 9658

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5235  ax-nul 5245  ax-pow 5304  ax-pr 5371  ax-un 7671

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 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-reu 3344  df-rab 3395  df-v 3438  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-iun 4943  df-br 5093  df-opab 5155  df-mpt 5174  df-tr 5200  df-id 5514  df-eprel 5519  df-po 5527  df-so 5528  df-fr 5572  df-we 5574  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-pred 6249  df-ord 6310  df-on 6311  df-lim 6312  df-suc 6313  df-iota 6438  df-fun 6484  df-fn 6485  df-f 6486  df-f1 6487  df-fo 6488  df-f1o 6489  df-fv 6490  df-ov 7352  df-om 7800  df-2nd 7925  df-frecs 8214  df-wrecs 8245  df-recs 8294  df-rdg 8332  df-r1 9660

This theorem is referenced by:  r1sscl  9681