MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  r1pwss Structured version   Visualization version   GIF version

Theorem r1pwss 8632
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.
StepHypRef Expression
1 r1funlim 8614 . . . . . . 7 (Fun 𝑅1 ∧ Lim dom 𝑅1)
21simpri 478 . . . . . 6 Lim dom 𝑅1
3 limord 5772 . . . . . 6 (Lim dom 𝑅1 → Ord dom 𝑅1)
42, 3ax-mp 5 . . . . 5 Ord dom 𝑅1
5 ordsson 6974 . . . . 5 (Ord dom 𝑅1 → dom 𝑅1 ⊆ On)
64, 5ax-mp 5 . . . 4 dom 𝑅1 ⊆ On
7 elfvdm 6207 . . . 4 (𝐴 ∈ (𝑅1𝐵) → 𝐵 ∈ dom 𝑅1)
86, 7sseldi 3593 . . 3 (𝐴 ∈ (𝑅1𝐵) → 𝐵 ∈ On)
9 onzsl 7031 . . 3 (𝐵 ∈ On ↔ (𝐵 = ∅ ∨ ∃𝑥 ∈ On 𝐵 = suc 𝑥 ∨ (𝐵 ∈ V ∧ Lim 𝐵)))
108, 9sylib 208 . 2 (𝐴 ∈ (𝑅1𝐵) → (𝐵 = ∅ ∨ ∃𝑥 ∈ On 𝐵 = suc 𝑥 ∨ (𝐵 ∈ V ∧ Lim 𝐵)))
11 noel 3911 . . . . 5 ¬ 𝐴 ∈ ∅
12 fveq2 6178 . . . . . . . 8 (𝐵 = ∅ → (𝑅1𝐵) = (𝑅1‘∅))
13 r10 8616 . . . . . . . 8 (𝑅1‘∅) = ∅
1412, 13syl6eq 2670 . . . . . . 7 (𝐵 = ∅ → (𝑅1𝐵) = ∅)
1514eleq2d 2685 . . . . . 6 (𝐵 = ∅ → (𝐴 ∈ (𝑅1𝐵) ↔ 𝐴 ∈ ∅))
1615biimpcd 239 . . . . 5 (𝐴 ∈ (𝑅1𝐵) → (𝐵 = ∅ → 𝐴 ∈ ∅))
1711, 16mtoi 190 . . . 4 (𝐴 ∈ (𝑅1𝐵) → ¬ 𝐵 = ∅)
1817pm2.21d 118 . . 3 (𝐴 ∈ (𝑅1𝐵) → (𝐵 = ∅ → 𝒫 𝐴 ⊆ (𝑅1𝐵)))
19 simpl 473 . . . . . . . 8 ((𝐴 ∈ (𝑅1𝐵) ∧ 𝐵 = suc 𝑥) → 𝐴 ∈ (𝑅1𝐵))
20 simpr 477 . . . . . . . . . 10 ((𝐴 ∈ (𝑅1𝐵) ∧ 𝐵 = suc 𝑥) → 𝐵 = suc 𝑥)
2120fveq2d 6182 . . . . . . . . 9 ((𝐴 ∈ (𝑅1𝐵) ∧ 𝐵 = suc 𝑥) → (𝑅1𝐵) = (𝑅1‘suc 𝑥))
227adantr 481 . . . . . . . . . . . 12 ((𝐴 ∈ (𝑅1𝐵) ∧ 𝐵 = suc 𝑥) → 𝐵 ∈ dom 𝑅1)
2320, 22eqeltrrd 2700 . . . . . . . . . . 11 ((𝐴 ∈ (𝑅1𝐵) ∧ 𝐵 = suc 𝑥) → suc 𝑥 ∈ dom 𝑅1)
24 limsuc 7034 . . . . . . . . . . . 12 (Lim dom 𝑅1 → (𝑥 ∈ dom 𝑅1 ↔ suc 𝑥 ∈ dom 𝑅1))
252, 24ax-mp 5 . . . . . . . . . . 11 (𝑥 ∈ dom 𝑅1 ↔ suc 𝑥 ∈ dom 𝑅1)
2623, 25sylibr 224 . . . . . . . . . 10 ((𝐴 ∈ (𝑅1𝐵) ∧ 𝐵 = suc 𝑥) → 𝑥 ∈ dom 𝑅1)
27 r1sucg 8617 . . . . . . . . . 10 (𝑥 ∈ dom 𝑅1 → (𝑅1‘suc 𝑥) = 𝒫 (𝑅1𝑥))
2826, 27syl 17 . . . . . . . . 9 ((𝐴 ∈ (𝑅1𝐵) ∧ 𝐵 = suc 𝑥) → (𝑅1‘suc 𝑥) = 𝒫 (𝑅1𝑥))
2921, 28eqtrd 2654 . . . . . . . 8 ((𝐴 ∈ (𝑅1𝐵) ∧ 𝐵 = suc 𝑥) → (𝑅1𝐵) = 𝒫 (𝑅1𝑥))
3019, 29eleqtrd 2701 . . . . . . 7 ((𝐴 ∈ (𝑅1𝐵) ∧ 𝐵 = suc 𝑥) → 𝐴 ∈ 𝒫 (𝑅1𝑥))
31 elpwi 4159 . . . . . . . 8 (𝐴 ∈ 𝒫 (𝑅1𝑥) → 𝐴 ⊆ (𝑅1𝑥))
32 sspwb 4908 . . . . . . . 8 (𝐴 ⊆ (𝑅1𝑥) ↔ 𝒫 𝐴 ⊆ 𝒫 (𝑅1𝑥))
3331, 32sylib 208 . . . . . . 7 (𝐴 ∈ 𝒫 (𝑅1𝑥) → 𝒫 𝐴 ⊆ 𝒫 (𝑅1𝑥))
3430, 33syl 17 . . . . . 6 ((𝐴 ∈ (𝑅1𝐵) ∧ 𝐵 = suc 𝑥) → 𝒫 𝐴 ⊆ 𝒫 (𝑅1𝑥))
3534, 29sseqtr4d 3634 . . . . 5 ((𝐴 ∈ (𝑅1𝐵) ∧ 𝐵 = suc 𝑥) → 𝒫 𝐴 ⊆ (𝑅1𝐵))
3635ex 450 . . . 4 (𝐴 ∈ (𝑅1𝐵) → (𝐵 = suc 𝑥 → 𝒫 𝐴 ⊆ (𝑅1𝐵)))
3736rexlimdvw 3030 . . 3 (𝐴 ∈ (𝑅1𝐵) → (∃𝑥 ∈ On 𝐵 = suc 𝑥 → 𝒫 𝐴 ⊆ (𝑅1𝐵)))
38 r1tr 8624 . . . . . 6 Tr (𝑅1𝐵)
39 simpl 473 . . . . . . . . . . 11 ((𝐴 ∈ (𝑅1𝐵) ∧ Lim 𝐵) → 𝐴 ∈ (𝑅1𝐵))
40 r1limg 8619 . . . . . . . . . . . 12 ((𝐵 ∈ dom 𝑅1 ∧ Lim 𝐵) → (𝑅1𝐵) = 𝑥𝐵 (𝑅1𝑥))
417, 40sylan 488 . . . . . . . . . . 11 ((𝐴 ∈ (𝑅1𝐵) ∧ Lim 𝐵) → (𝑅1𝐵) = 𝑥𝐵 (𝑅1𝑥))
4239, 41eleqtrd 2701 . . . . . . . . . 10 ((𝐴 ∈ (𝑅1𝐵) ∧ Lim 𝐵) → 𝐴 𝑥𝐵 (𝑅1𝑥))
43 eliun 4515 . . . . . . . . . 10 (𝐴 𝑥𝐵 (𝑅1𝑥) ↔ ∃𝑥𝐵 𝐴 ∈ (𝑅1𝑥))
4442, 43sylib 208 . . . . . . . . 9 ((𝐴 ∈ (𝑅1𝐵) ∧ Lim 𝐵) → ∃𝑥𝐵 𝐴 ∈ (𝑅1𝑥))
45 simprl 793 . . . . . . . . . . . 12 (((𝐴 ∈ (𝑅1𝐵) ∧ Lim 𝐵) ∧ (𝑥𝐵𝐴 ∈ (𝑅1𝑥))) → 𝑥𝐵)
46 limsuc 7034 . . . . . . . . . . . . 13 (Lim 𝐵 → (𝑥𝐵 ↔ suc 𝑥𝐵))
4746ad2antlr 762 . . . . . . . . . . . 12 (((𝐴 ∈ (𝑅1𝐵) ∧ Lim 𝐵) ∧ (𝑥𝐵𝐴 ∈ (𝑅1𝑥))) → (𝑥𝐵 ↔ suc 𝑥𝐵))
4845, 47mpbid 222 . . . . . . . . . . 11 (((𝐴 ∈ (𝑅1𝐵) ∧ Lim 𝐵) ∧ (𝑥𝐵𝐴 ∈ (𝑅1𝑥))) → suc 𝑥𝐵)
49 limsuc 7034 . . . . . . . . . . . 12 (Lim 𝐵 → (suc 𝑥𝐵 ↔ suc suc 𝑥𝐵))
5049ad2antlr 762 . . . . . . . . . . 11 (((𝐴 ∈ (𝑅1𝐵) ∧ Lim 𝐵) ∧ (𝑥𝐵𝐴 ∈ (𝑅1𝑥))) → (suc 𝑥𝐵 ↔ suc suc 𝑥𝐵))
5148, 50mpbid 222 . . . . . . . . . 10 (((𝐴 ∈ (𝑅1𝐵) ∧ Lim 𝐵) ∧ (𝑥𝐵𝐴 ∈ (𝑅1𝑥))) → suc suc 𝑥𝐵)
52 r1tr 8624 . . . . . . . . . . . . . . 15 Tr (𝑅1𝑥)
53 simprr 795 . . . . . . . . . . . . . . 15 (((𝐴 ∈ (𝑅1𝐵) ∧ Lim 𝐵) ∧ (𝑥𝐵𝐴 ∈ (𝑅1𝑥))) → 𝐴 ∈ (𝑅1𝑥))
54 trss 4752 . . . . . . . . . . . . . . 15 (Tr (𝑅1𝑥) → (𝐴 ∈ (𝑅1𝑥) → 𝐴 ⊆ (𝑅1𝑥)))
5552, 53, 54mpsyl 68 . . . . . . . . . . . . . 14 (((𝐴 ∈ (𝑅1𝐵) ∧ Lim 𝐵) ∧ (𝑥𝐵𝐴 ∈ (𝑅1𝑥))) → 𝐴 ⊆ (𝑅1𝑥))
5655, 32sylib 208 . . . . . . . . . . . . 13 (((𝐴 ∈ (𝑅1𝐵) ∧ Lim 𝐵) ∧ (𝑥𝐵𝐴 ∈ (𝑅1𝑥))) → 𝒫 𝐴 ⊆ 𝒫 (𝑅1𝑥))
577ad2antrr 761 . . . . . . . . . . . . . . 15 (((𝐴 ∈ (𝑅1𝐵) ∧ Lim 𝐵) ∧ (𝑥𝐵𝐴 ∈ (𝑅1𝑥))) → 𝐵 ∈ dom 𝑅1)
58 ordtr1 5755 . . . . . . . . . . . . . . . 16 (Ord dom 𝑅1 → ((𝑥𝐵𝐵 ∈ dom 𝑅1) → 𝑥 ∈ dom 𝑅1))
594, 58ax-mp 5 . . . . . . . . . . . . . . 15 ((𝑥𝐵𝐵 ∈ dom 𝑅1) → 𝑥 ∈ dom 𝑅1)
6045, 57, 59syl2anc 692 . . . . . . . . . . . . . 14 (((𝐴 ∈ (𝑅1𝐵) ∧ Lim 𝐵) ∧ (𝑥𝐵𝐴 ∈ (𝑅1𝑥))) → 𝑥 ∈ dom 𝑅1)
6160, 27syl 17 . . . . . . . . . . . . 13 (((𝐴 ∈ (𝑅1𝐵) ∧ Lim 𝐵) ∧ (𝑥𝐵𝐴 ∈ (𝑅1𝑥))) → (𝑅1‘suc 𝑥) = 𝒫 (𝑅1𝑥))
6256, 61sseqtr4d 3634 . . . . . . . . . . . 12 (((𝐴 ∈ (𝑅1𝐵) ∧ Lim 𝐵) ∧ (𝑥𝐵𝐴 ∈ (𝑅1𝑥))) → 𝒫 𝐴 ⊆ (𝑅1‘suc 𝑥))
63 fvex 6188 . . . . . . . . . . . . 13 (𝑅1‘suc 𝑥) ∈ V
6463elpw2 4819 . . . . . . . . . . . 12 (𝒫 𝐴 ∈ 𝒫 (𝑅1‘suc 𝑥) ↔ 𝒫 𝐴 ⊆ (𝑅1‘suc 𝑥))
6562, 64sylibr 224 . . . . . . . . . . 11 (((𝐴 ∈ (𝑅1𝐵) ∧ Lim 𝐵) ∧ (𝑥𝐵𝐴 ∈ (𝑅1𝑥))) → 𝒫 𝐴 ∈ 𝒫 (𝑅1‘suc 𝑥))
6660, 25sylib 208 . . . . . . . . . . . 12 (((𝐴 ∈ (𝑅1𝐵) ∧ Lim 𝐵) ∧ (𝑥𝐵𝐴 ∈ (𝑅1𝑥))) → suc 𝑥 ∈ dom 𝑅1)
67 r1sucg 8617 . . . . . . . . . . . 12 (suc 𝑥 ∈ dom 𝑅1 → (𝑅1‘suc suc 𝑥) = 𝒫 (𝑅1‘suc 𝑥))
6866, 67syl 17 . . . . . . . . . . 11 (((𝐴 ∈ (𝑅1𝐵) ∧ Lim 𝐵) ∧ (𝑥𝐵𝐴 ∈ (𝑅1𝑥))) → (𝑅1‘suc suc 𝑥) = 𝒫 (𝑅1‘suc 𝑥))
6965, 68eleqtrrd 2702 . . . . . . . . . 10 (((𝐴 ∈ (𝑅1𝐵) ∧ Lim 𝐵) ∧ (𝑥𝐵𝐴 ∈ (𝑅1𝑥))) → 𝒫 𝐴 ∈ (𝑅1‘suc suc 𝑥))
70 fveq2 6178 . . . . . . . . . . . 12 (𝑦 = suc suc 𝑥 → (𝑅1𝑦) = (𝑅1‘suc suc 𝑥))
7170eleq2d 2685 . . . . . . . . . . 11 (𝑦 = suc suc 𝑥 → (𝒫 𝐴 ∈ (𝑅1𝑦) ↔ 𝒫 𝐴 ∈ (𝑅1‘suc suc 𝑥)))
7271rspcev 3304 . . . . . . . . . 10 ((suc suc 𝑥𝐵 ∧ 𝒫 𝐴 ∈ (𝑅1‘suc suc 𝑥)) → ∃𝑦𝐵 𝒫 𝐴 ∈ (𝑅1𝑦))
7351, 69, 72syl2anc 692 . . . . . . . . 9 (((𝐴 ∈ (𝑅1𝐵) ∧ Lim 𝐵) ∧ (𝑥𝐵𝐴 ∈ (𝑅1𝑥))) → ∃𝑦𝐵 𝒫 𝐴 ∈ (𝑅1𝑦))
7444, 73rexlimddv 3031 . . . . . . . 8 ((𝐴 ∈ (𝑅1𝐵) ∧ Lim 𝐵) → ∃𝑦𝐵 𝒫 𝐴 ∈ (𝑅1𝑦))
75 eliun 4515 . . . . . . . 8 (𝒫 𝐴 𝑦𝐵 (𝑅1𝑦) ↔ ∃𝑦𝐵 𝒫 𝐴 ∈ (𝑅1𝑦))
7674, 75sylibr 224 . . . . . . 7 ((𝐴 ∈ (𝑅1𝐵) ∧ Lim 𝐵) → 𝒫 𝐴 𝑦𝐵 (𝑅1𝑦))
77 r1limg 8619 . . . . . . . 8 ((𝐵 ∈ dom 𝑅1 ∧ Lim 𝐵) → (𝑅1𝐵) = 𝑦𝐵 (𝑅1𝑦))
787, 77sylan 488 . . . . . . 7 ((𝐴 ∈ (𝑅1𝐵) ∧ Lim 𝐵) → (𝑅1𝐵) = 𝑦𝐵 (𝑅1𝑦))
7976, 78eleqtrrd 2702 . . . . . 6 ((𝐴 ∈ (𝑅1𝐵) ∧ Lim 𝐵) → 𝒫 𝐴 ∈ (𝑅1𝐵))
80 trss 4752 . . . . . 6 (Tr (𝑅1𝐵) → (𝒫 𝐴 ∈ (𝑅1𝐵) → 𝒫 𝐴 ⊆ (𝑅1𝐵)))
8138, 79, 80mpsyl 68 . . . . 5 ((𝐴 ∈ (𝑅1𝐵) ∧ Lim 𝐵) → 𝒫 𝐴 ⊆ (𝑅1𝐵))
8281ex 450 . . . 4 (𝐴 ∈ (𝑅1𝐵) → (Lim 𝐵 → 𝒫 𝐴 ⊆ (𝑅1𝐵)))
8382adantld 483 . . 3 (𝐴 ∈ (𝑅1𝐵) → ((𝐵 ∈ V ∧ Lim 𝐵) → 𝒫 𝐴 ⊆ (𝑅1𝐵)))
8418, 37, 833jaod 1390 . 2 (𝐴 ∈ (𝑅1𝐵) → ((𝐵 = ∅ ∨ ∃𝑥 ∈ On 𝐵 = suc 𝑥 ∨ (𝐵 ∈ V ∧ Lim 𝐵)) → 𝒫 𝐴 ⊆ (𝑅1𝐵)))
8510, 84mpd 15 1 (𝐴 ∈ (𝑅1𝐵) → 𝒫 𝐴 ⊆ (𝑅1𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384  w3o 1035   = wceq 1481  wcel 1988  wrex 2910  Vcvv 3195  wss 3567  c0 3907  𝒫 cpw 4149   ciun 4511  Tr wtr 4743  dom cdm 5104  Ord word 5710  Oncon0 5711  Lim wlim 5712  suc csuc 5713  Fun wfun 5870  cfv 5876  𝑅1cr1 8610
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-8 1990  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-sep 4772  ax-nul 4780  ax-pow 4834  ax-pr 4897  ax-un 6934
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-eu 2472  df-mo 2473  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ne 2792  df-ral 2914  df-rex 2915  df-reu 2916  df-rab 2918  df-v 3197  df-sbc 3430  df-csb 3527  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-pss 3583  df-nul 3908  df-if 4078  df-pw 4151  df-sn 4169  df-pr 4171  df-tp 4173  df-op 4175  df-uni 4428  df-iun 4513  df-br 4645  df-opab 4704  df-mpt 4721  df-tr 4744  df-id 5014  df-eprel 5019  df-po 5025  df-so 5026  df-fr 5063  df-we 5065  df-xp 5110  df-rel 5111  df-cnv 5112  df-co 5113  df-dm 5114  df-rn 5115  df-res 5116  df-ima 5117  df-pred 5668  df-ord 5714  df-on 5715  df-lim 5716  df-suc 5717  df-iota 5839  df-fun 5878  df-fn 5879  df-f 5880  df-f1 5881  df-fo 5882  df-f1o 5883  df-fv 5884  df-om 7051  df-wrecs 7392  df-recs 7453  df-rdg 7491  df-r1 8612
This theorem is referenced by:  r1sscl  8633
  Copyright terms: Public domain W3C validator