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

Theorem r1val1 9544
Description: The value of the cumulative hierarchy of sets function expressed recursively. Theorem 7Q of [Enderton] p. 202. (Contributed by NM, 25-Nov-2003.) (Revised by Mario Carneiro, 17-Nov-2014.)
Assertion
Ref Expression
r1val1 (𝐴 ∈ dom 𝑅1 → (𝑅1𝐴) = 𝑥𝐴 𝒫 (𝑅1𝑥))
Distinct variable group:   𝑥,𝐴

Proof of Theorem r1val1
StepHypRef Expression
1 simpr 485 . . . . . 6 ((𝐴 ∈ dom 𝑅1𝐴 = ∅) → 𝐴 = ∅)
21fveq2d 6778 . . . . 5 ((𝐴 ∈ dom 𝑅1𝐴 = ∅) → (𝑅1𝐴) = (𝑅1‘∅))
3 r10 9526 . . . . 5 (𝑅1‘∅) = ∅
42, 3eqtrdi 2794 . . . 4 ((𝐴 ∈ dom 𝑅1𝐴 = ∅) → (𝑅1𝐴) = ∅)
5 0ss 4330 . . . . 5 ∅ ⊆ 𝑥𝐴 𝒫 (𝑅1𝑥)
65a1i 11 . . . 4 ((𝐴 ∈ dom 𝑅1𝐴 = ∅) → ∅ ⊆ 𝑥𝐴 𝒫 (𝑅1𝑥))
74, 6eqsstrd 3959 . . 3 ((𝐴 ∈ dom 𝑅1𝐴 = ∅) → (𝑅1𝐴) ⊆ 𝑥𝐴 𝒫 (𝑅1𝑥))
8 nfv 1917 . . . . 5 𝑥 𝐴 ∈ dom 𝑅1
9 nfcv 2907 . . . . . 6 𝑥(𝑅1𝐴)
10 nfiu1 4958 . . . . . 6 𝑥 𝑥𝐴 𝒫 (𝑅1𝑥)
119, 10nfss 3913 . . . . 5 𝑥(𝑅1𝐴) ⊆ 𝑥𝐴 𝒫 (𝑅1𝑥)
12 simpr 485 . . . . . . . . . 10 ((𝐴 ∈ dom 𝑅1𝐴 = suc 𝑥) → 𝐴 = suc 𝑥)
1312fveq2d 6778 . . . . . . . . 9 ((𝐴 ∈ dom 𝑅1𝐴 = suc 𝑥) → (𝑅1𝐴) = (𝑅1‘suc 𝑥))
14 eleq1 2826 . . . . . . . . . . . 12 (𝐴 = suc 𝑥 → (𝐴 ∈ dom 𝑅1 ↔ suc 𝑥 ∈ dom 𝑅1))
1514biimpac 479 . . . . . . . . . . 11 ((𝐴 ∈ dom 𝑅1𝐴 = suc 𝑥) → suc 𝑥 ∈ dom 𝑅1)
16 r1funlim 9524 . . . . . . . . . . . . 13 (Fun 𝑅1 ∧ Lim dom 𝑅1)
1716simpri 486 . . . . . . . . . . . 12 Lim dom 𝑅1
18 limsuc 7696 . . . . . . . . . . . 12 (Lim dom 𝑅1 → (𝑥 ∈ dom 𝑅1 ↔ suc 𝑥 ∈ dom 𝑅1))
1917, 18ax-mp 5 . . . . . . . . . . 11 (𝑥 ∈ dom 𝑅1 ↔ suc 𝑥 ∈ dom 𝑅1)
2015, 19sylibr 233 . . . . . . . . . 10 ((𝐴 ∈ dom 𝑅1𝐴 = suc 𝑥) → 𝑥 ∈ dom 𝑅1)
21 r1sucg 9527 . . . . . . . . . 10 (𝑥 ∈ dom 𝑅1 → (𝑅1‘suc 𝑥) = 𝒫 (𝑅1𝑥))
2220, 21syl 17 . . . . . . . . 9 ((𝐴 ∈ dom 𝑅1𝐴 = suc 𝑥) → (𝑅1‘suc 𝑥) = 𝒫 (𝑅1𝑥))
2313, 22eqtrd 2778 . . . . . . . 8 ((𝐴 ∈ dom 𝑅1𝐴 = suc 𝑥) → (𝑅1𝐴) = 𝒫 (𝑅1𝑥))
24 vex 3436 . . . . . . . . . . 11 𝑥 ∈ V
2524sucid 6345 . . . . . . . . . 10 𝑥 ∈ suc 𝑥
2625, 12eleqtrrid 2846 . . . . . . . . 9 ((𝐴 ∈ dom 𝑅1𝐴 = suc 𝑥) → 𝑥𝐴)
27 ssiun2 4977 . . . . . . . . 9 (𝑥𝐴 → 𝒫 (𝑅1𝑥) ⊆ 𝑥𝐴 𝒫 (𝑅1𝑥))
2826, 27syl 17 . . . . . . . 8 ((𝐴 ∈ dom 𝑅1𝐴 = suc 𝑥) → 𝒫 (𝑅1𝑥) ⊆ 𝑥𝐴 𝒫 (𝑅1𝑥))
2923, 28eqsstrd 3959 . . . . . . 7 ((𝐴 ∈ dom 𝑅1𝐴 = suc 𝑥) → (𝑅1𝐴) ⊆ 𝑥𝐴 𝒫 (𝑅1𝑥))
3029ex 413 . . . . . 6 (𝐴 ∈ dom 𝑅1 → (𝐴 = suc 𝑥 → (𝑅1𝐴) ⊆ 𝑥𝐴 𝒫 (𝑅1𝑥)))
3130a1d 25 . . . . 5 (𝐴 ∈ dom 𝑅1 → (𝑥 ∈ On → (𝐴 = suc 𝑥 → (𝑅1𝐴) ⊆ 𝑥𝐴 𝒫 (𝑅1𝑥))))
328, 11, 31rexlimd 3250 . . . 4 (𝐴 ∈ dom 𝑅1 → (∃𝑥 ∈ On 𝐴 = suc 𝑥 → (𝑅1𝐴) ⊆ 𝑥𝐴 𝒫 (𝑅1𝑥)))
3332imp 407 . . 3 ((𝐴 ∈ dom 𝑅1 ∧ ∃𝑥 ∈ On 𝐴 = suc 𝑥) → (𝑅1𝐴) ⊆ 𝑥𝐴 𝒫 (𝑅1𝑥))
34 r1limg 9529 . . . . 5 ((𝐴 ∈ dom 𝑅1 ∧ Lim 𝐴) → (𝑅1𝐴) = 𝑥𝐴 (𝑅1𝑥))
35 r1tr 9534 . . . . . . . . 9 Tr (𝑅1𝑥)
36 dftr4 5196 . . . . . . . . 9 (Tr (𝑅1𝑥) ↔ (𝑅1𝑥) ⊆ 𝒫 (𝑅1𝑥))
3735, 36mpbi 229 . . . . . . . 8 (𝑅1𝑥) ⊆ 𝒫 (𝑅1𝑥)
3837a1i 11 . . . . . . 7 ((𝐴 ∈ dom 𝑅1 ∧ Lim 𝐴) → (𝑅1𝑥) ⊆ 𝒫 (𝑅1𝑥))
3938ralrimivw 3104 . . . . . 6 ((𝐴 ∈ dom 𝑅1 ∧ Lim 𝐴) → ∀𝑥𝐴 (𝑅1𝑥) ⊆ 𝒫 (𝑅1𝑥))
40 ss2iun 4942 . . . . . 6 (∀𝑥𝐴 (𝑅1𝑥) ⊆ 𝒫 (𝑅1𝑥) → 𝑥𝐴 (𝑅1𝑥) ⊆ 𝑥𝐴 𝒫 (𝑅1𝑥))
4139, 40syl 17 . . . . 5 ((𝐴 ∈ dom 𝑅1 ∧ Lim 𝐴) → 𝑥𝐴 (𝑅1𝑥) ⊆ 𝑥𝐴 𝒫 (𝑅1𝑥))
4234, 41eqsstrd 3959 . . . 4 ((𝐴 ∈ dom 𝑅1 ∧ Lim 𝐴) → (𝑅1𝐴) ⊆ 𝑥𝐴 𝒫 (𝑅1𝑥))
4342adantrl 713 . . 3 ((𝐴 ∈ dom 𝑅1 ∧ (𝐴 ∈ V ∧ Lim 𝐴)) → (𝑅1𝐴) ⊆ 𝑥𝐴 𝒫 (𝑅1𝑥))
44 limord 6325 . . . . . . 7 (Lim dom 𝑅1 → Ord dom 𝑅1)
4517, 44ax-mp 5 . . . . . 6 Ord dom 𝑅1
46 ordsson 7633 . . . . . 6 (Ord dom 𝑅1 → dom 𝑅1 ⊆ On)
4745, 46ax-mp 5 . . . . 5 dom 𝑅1 ⊆ On
4847sseli 3917 . . . 4 (𝐴 ∈ dom 𝑅1𝐴 ∈ On)
49 onzsl 7693 . . . 4 (𝐴 ∈ On ↔ (𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥 ∨ (𝐴 ∈ V ∧ Lim 𝐴)))
5048, 49sylib 217 . . 3 (𝐴 ∈ dom 𝑅1 → (𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥 ∨ (𝐴 ∈ V ∧ Lim 𝐴)))
517, 33, 43, 50mpjao3dan 1430 . 2 (𝐴 ∈ dom 𝑅1 → (𝑅1𝐴) ⊆ 𝑥𝐴 𝒫 (𝑅1𝑥))
52 ordtr1 6309 . . . . . . . 8 (Ord dom 𝑅1 → ((𝑥𝐴𝐴 ∈ dom 𝑅1) → 𝑥 ∈ dom 𝑅1))
5345, 52ax-mp 5 . . . . . . 7 ((𝑥𝐴𝐴 ∈ dom 𝑅1) → 𝑥 ∈ dom 𝑅1)
5453ancoms 459 . . . . . 6 ((𝐴 ∈ dom 𝑅1𝑥𝐴) → 𝑥 ∈ dom 𝑅1)
5554, 21syl 17 . . . . 5 ((𝐴 ∈ dom 𝑅1𝑥𝐴) → (𝑅1‘suc 𝑥) = 𝒫 (𝑅1𝑥))
56 simpr 485 . . . . . . 7 ((𝐴 ∈ dom 𝑅1𝑥𝐴) → 𝑥𝐴)
57 ordelord 6288 . . . . . . . . . 10 ((Ord dom 𝑅1𝐴 ∈ dom 𝑅1) → Ord 𝐴)
5845, 57mpan 687 . . . . . . . . 9 (𝐴 ∈ dom 𝑅1 → Ord 𝐴)
5958adantr 481 . . . . . . . 8 ((𝐴 ∈ dom 𝑅1𝑥𝐴) → Ord 𝐴)
60 ordelsuc 7667 . . . . . . . 8 ((𝑥𝐴 ∧ Ord 𝐴) → (𝑥𝐴 ↔ suc 𝑥𝐴))
6156, 59, 60syl2anc 584 . . . . . . 7 ((𝐴 ∈ dom 𝑅1𝑥𝐴) → (𝑥𝐴 ↔ suc 𝑥𝐴))
6256, 61mpbid 231 . . . . . 6 ((𝐴 ∈ dom 𝑅1𝑥𝐴) → suc 𝑥𝐴)
6354, 19sylib 217 . . . . . . 7 ((𝐴 ∈ dom 𝑅1𝑥𝐴) → suc 𝑥 ∈ dom 𝑅1)
64 simpl 483 . . . . . . 7 ((𝐴 ∈ dom 𝑅1𝑥𝐴) → 𝐴 ∈ dom 𝑅1)
65 r1ord3g 9537 . . . . . . 7 ((suc 𝑥 ∈ dom 𝑅1𝐴 ∈ dom 𝑅1) → (suc 𝑥𝐴 → (𝑅1‘suc 𝑥) ⊆ (𝑅1𝐴)))
6663, 64, 65syl2anc 584 . . . . . 6 ((𝐴 ∈ dom 𝑅1𝑥𝐴) → (suc 𝑥𝐴 → (𝑅1‘suc 𝑥) ⊆ (𝑅1𝐴)))
6762, 66mpd 15 . . . . 5 ((𝐴 ∈ dom 𝑅1𝑥𝐴) → (𝑅1‘suc 𝑥) ⊆ (𝑅1𝐴))
6855, 67eqsstrrd 3960 . . . 4 ((𝐴 ∈ dom 𝑅1𝑥𝐴) → 𝒫 (𝑅1𝑥) ⊆ (𝑅1𝐴))
6968ralrimiva 3103 . . 3 (𝐴 ∈ dom 𝑅1 → ∀𝑥𝐴 𝒫 (𝑅1𝑥) ⊆ (𝑅1𝐴))
70 iunss 4975 . . 3 ( 𝑥𝐴 𝒫 (𝑅1𝑥) ⊆ (𝑅1𝐴) ↔ ∀𝑥𝐴 𝒫 (𝑅1𝑥) ⊆ (𝑅1𝐴))
7169, 70sylibr 233 . 2 (𝐴 ∈ dom 𝑅1 𝑥𝐴 𝒫 (𝑅1𝑥) ⊆ (𝑅1𝐴))
7251, 71eqssd 3938 1 (𝐴 ∈ dom 𝑅1 → (𝑅1𝐴) = 𝑥𝐴 𝒫 (𝑅1𝑥))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396  w3o 1085   = wceq 1539  wcel 2106  wral 3064  wrex 3065  Vcvv 3432  wss 3887  c0 4256  𝒫 cpw 4533   ciun 4924  Tr wtr 5191  dom cdm 5589  Ord word 6265  Oncon0 6266  Lim wlim 6267  suc csuc 6268  Fun wfun 6427  cfv 6433  𝑅1cr1 9520
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7588
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-ral 3069  df-rex 3070  df-reu 3072  df-rab 3073  df-v 3434  df-sbc 3717  df-csb 3833  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-pss 3906  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-iun 4926  df-br 5075  df-opab 5137  df-mpt 5158  df-tr 5192  df-id 5489  df-eprel 5495  df-po 5503  df-so 5504  df-fr 5544  df-we 5546  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-pred 6202  df-ord 6269  df-on 6270  df-lim 6271  df-suc 6272  df-iota 6391  df-fun 6435  df-fn 6436  df-f 6437  df-f1 6438  df-fo 6439  df-f1o 6440  df-fv 6441  df-ov 7278  df-om 7713  df-2nd 7832  df-frecs 8097  df-wrecs 8128  df-recs 8202  df-rdg 8241  df-r1 9522
This theorem is referenced by:  rankr1ai  9556  r1val3  9596
  Copyright terms: Public domain W3C validator