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

Theorem r1val1 9214
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 487 . . . . . 6 ((𝐴 ∈ dom 𝑅1𝐴 = ∅) → 𝐴 = ∅)
21fveq2d 6673 . . . . 5 ((𝐴 ∈ dom 𝑅1𝐴 = ∅) → (𝑅1𝐴) = (𝑅1‘∅))
3 r10 9196 . . . . 5 (𝑅1‘∅) = ∅
42, 3syl6eq 2872 . . . 4 ((𝐴 ∈ dom 𝑅1𝐴 = ∅) → (𝑅1𝐴) = ∅)
5 0ss 4349 . . . . 5 ∅ ⊆ 𝑥𝐴 𝒫 (𝑅1𝑥)
65a1i 11 . . . 4 ((𝐴 ∈ dom 𝑅1𝐴 = ∅) → ∅ ⊆ 𝑥𝐴 𝒫 (𝑅1𝑥))
74, 6eqsstrd 4004 . . 3 ((𝐴 ∈ dom 𝑅1𝐴 = ∅) → (𝑅1𝐴) ⊆ 𝑥𝐴 𝒫 (𝑅1𝑥))
8 nfv 1911 . . . . 5 𝑥 𝐴 ∈ dom 𝑅1
9 nfcv 2977 . . . . . 6 𝑥(𝑅1𝐴)
10 nfiu1 4952 . . . . . 6 𝑥 𝑥𝐴 𝒫 (𝑅1𝑥)
119, 10nfss 3959 . . . . 5 𝑥(𝑅1𝐴) ⊆ 𝑥𝐴 𝒫 (𝑅1𝑥)
12 simpr 487 . . . . . . . . . 10 ((𝐴 ∈ dom 𝑅1𝐴 = suc 𝑥) → 𝐴 = suc 𝑥)
1312fveq2d 6673 . . . . . . . . 9 ((𝐴 ∈ dom 𝑅1𝐴 = suc 𝑥) → (𝑅1𝐴) = (𝑅1‘suc 𝑥))
14 eleq1 2900 . . . . . . . . . . . 12 (𝐴 = suc 𝑥 → (𝐴 ∈ dom 𝑅1 ↔ suc 𝑥 ∈ dom 𝑅1))
1514biimpac 481 . . . . . . . . . . 11 ((𝐴 ∈ dom 𝑅1𝐴 = suc 𝑥) → suc 𝑥 ∈ dom 𝑅1)
16 r1funlim 9194 . . . . . . . . . . . . 13 (Fun 𝑅1 ∧ Lim dom 𝑅1)
1716simpri 488 . . . . . . . . . . . 12 Lim dom 𝑅1
18 limsuc 7563 . . . . . . . . . . . 12 (Lim dom 𝑅1 → (𝑥 ∈ dom 𝑅1 ↔ suc 𝑥 ∈ dom 𝑅1))
1917, 18ax-mp 5 . . . . . . . . . . 11 (𝑥 ∈ dom 𝑅1 ↔ suc 𝑥 ∈ dom 𝑅1)
2015, 19sylibr 236 . . . . . . . . . 10 ((𝐴 ∈ dom 𝑅1𝐴 = suc 𝑥) → 𝑥 ∈ dom 𝑅1)
21 r1sucg 9197 . . . . . . . . . 10 (𝑥 ∈ dom 𝑅1 → (𝑅1‘suc 𝑥) = 𝒫 (𝑅1𝑥))
2220, 21syl 17 . . . . . . . . 9 ((𝐴 ∈ dom 𝑅1𝐴 = suc 𝑥) → (𝑅1‘suc 𝑥) = 𝒫 (𝑅1𝑥))
2313, 22eqtrd 2856 . . . . . . . 8 ((𝐴 ∈ dom 𝑅1𝐴 = suc 𝑥) → (𝑅1𝐴) = 𝒫 (𝑅1𝑥))
24 vex 3497 . . . . . . . . . . 11 𝑥 ∈ V
2524sucid 6269 . . . . . . . . . 10 𝑥 ∈ suc 𝑥
2625, 12eleqtrrid 2920 . . . . . . . . 9 ((𝐴 ∈ dom 𝑅1𝐴 = suc 𝑥) → 𝑥𝐴)
27 ssiun2 4970 . . . . . . . . 9 (𝑥𝐴 → 𝒫 (𝑅1𝑥) ⊆ 𝑥𝐴 𝒫 (𝑅1𝑥))
2826, 27syl 17 . . . . . . . 8 ((𝐴 ∈ dom 𝑅1𝐴 = suc 𝑥) → 𝒫 (𝑅1𝑥) ⊆ 𝑥𝐴 𝒫 (𝑅1𝑥))
2923, 28eqsstrd 4004 . . . . . . 7 ((𝐴 ∈ dom 𝑅1𝐴 = suc 𝑥) → (𝑅1𝐴) ⊆ 𝑥𝐴 𝒫 (𝑅1𝑥))
3029ex 415 . . . . . 6 (𝐴 ∈ dom 𝑅1 → (𝐴 = suc 𝑥 → (𝑅1𝐴) ⊆ 𝑥𝐴 𝒫 (𝑅1𝑥)))
3130a1d 25 . . . . 5 (𝐴 ∈ dom 𝑅1 → (𝑥 ∈ On → (𝐴 = suc 𝑥 → (𝑅1𝐴) ⊆ 𝑥𝐴 𝒫 (𝑅1𝑥))))
328, 11, 31rexlimd 3317 . . . 4 (𝐴 ∈ dom 𝑅1 → (∃𝑥 ∈ On 𝐴 = suc 𝑥 → (𝑅1𝐴) ⊆ 𝑥𝐴 𝒫 (𝑅1𝑥)))
3332imp 409 . . 3 ((𝐴 ∈ dom 𝑅1 ∧ ∃𝑥 ∈ On 𝐴 = suc 𝑥) → (𝑅1𝐴) ⊆ 𝑥𝐴 𝒫 (𝑅1𝑥))
34 r1limg 9199 . . . . 5 ((𝐴 ∈ dom 𝑅1 ∧ Lim 𝐴) → (𝑅1𝐴) = 𝑥𝐴 (𝑅1𝑥))
35 r1tr 9204 . . . . . . . . 9 Tr (𝑅1𝑥)
36 dftr4 5176 . . . . . . . . 9 (Tr (𝑅1𝑥) ↔ (𝑅1𝑥) ⊆ 𝒫 (𝑅1𝑥))
3735, 36mpbi 232 . . . . . . . 8 (𝑅1𝑥) ⊆ 𝒫 (𝑅1𝑥)
3837a1i 11 . . . . . . 7 ((𝐴 ∈ dom 𝑅1 ∧ Lim 𝐴) → (𝑅1𝑥) ⊆ 𝒫 (𝑅1𝑥))
3938ralrimivw 3183 . . . . . 6 ((𝐴 ∈ dom 𝑅1 ∧ Lim 𝐴) → ∀𝑥𝐴 (𝑅1𝑥) ⊆ 𝒫 (𝑅1𝑥))
40 ss2iun 4936 . . . . . 6 (∀𝑥𝐴 (𝑅1𝑥) ⊆ 𝒫 (𝑅1𝑥) → 𝑥𝐴 (𝑅1𝑥) ⊆ 𝑥𝐴 𝒫 (𝑅1𝑥))
4139, 40syl 17 . . . . 5 ((𝐴 ∈ dom 𝑅1 ∧ Lim 𝐴) → 𝑥𝐴 (𝑅1𝑥) ⊆ 𝑥𝐴 𝒫 (𝑅1𝑥))
4234, 41eqsstrd 4004 . . . 4 ((𝐴 ∈ dom 𝑅1 ∧ Lim 𝐴) → (𝑅1𝐴) ⊆ 𝑥𝐴 𝒫 (𝑅1𝑥))
4342adantrl 714 . . 3 ((𝐴 ∈ dom 𝑅1 ∧ (𝐴 ∈ V ∧ Lim 𝐴)) → (𝑅1𝐴) ⊆ 𝑥𝐴 𝒫 (𝑅1𝑥))
44 limord 6249 . . . . . . 7 (Lim dom 𝑅1 → Ord dom 𝑅1)
4517, 44ax-mp 5 . . . . . 6 Ord dom 𝑅1
46 ordsson 7503 . . . . . 6 (Ord dom 𝑅1 → dom 𝑅1 ⊆ On)
4745, 46ax-mp 5 . . . . 5 dom 𝑅1 ⊆ On
4847sseli 3962 . . . 4 (𝐴 ∈ dom 𝑅1𝐴 ∈ On)
49 onzsl 7560 . . . 4 (𝐴 ∈ On ↔ (𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥 ∨ (𝐴 ∈ V ∧ Lim 𝐴)))
5048, 49sylib 220 . . 3 (𝐴 ∈ dom 𝑅1 → (𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥 ∨ (𝐴 ∈ V ∧ Lim 𝐴)))
517, 33, 43, 50mpjao3dan 1427 . 2 (𝐴 ∈ dom 𝑅1 → (𝑅1𝐴) ⊆ 𝑥𝐴 𝒫 (𝑅1𝑥))
52 ordtr1 6233 . . . . . . . 8 (Ord dom 𝑅1 → ((𝑥𝐴𝐴 ∈ dom 𝑅1) → 𝑥 ∈ dom 𝑅1))
5345, 52ax-mp 5 . . . . . . 7 ((𝑥𝐴𝐴 ∈ dom 𝑅1) → 𝑥 ∈ dom 𝑅1)
5453ancoms 461 . . . . . 6 ((𝐴 ∈ dom 𝑅1𝑥𝐴) → 𝑥 ∈ dom 𝑅1)
5554, 21syl 17 . . . . 5 ((𝐴 ∈ dom 𝑅1𝑥𝐴) → (𝑅1‘suc 𝑥) = 𝒫 (𝑅1𝑥))
56 simpr 487 . . . . . . 7 ((𝐴 ∈ dom 𝑅1𝑥𝐴) → 𝑥𝐴)
57 ordelord 6212 . . . . . . . . . 10 ((Ord dom 𝑅1𝐴 ∈ dom 𝑅1) → Ord 𝐴)
5845, 57mpan 688 . . . . . . . . 9 (𝐴 ∈ dom 𝑅1 → Ord 𝐴)
5958adantr 483 . . . . . . . 8 ((𝐴 ∈ dom 𝑅1𝑥𝐴) → Ord 𝐴)
60 ordelsuc 7534 . . . . . . . 8 ((𝑥𝐴 ∧ Ord 𝐴) → (𝑥𝐴 ↔ suc 𝑥𝐴))
6156, 59, 60syl2anc 586 . . . . . . 7 ((𝐴 ∈ dom 𝑅1𝑥𝐴) → (𝑥𝐴 ↔ suc 𝑥𝐴))
6256, 61mpbid 234 . . . . . 6 ((𝐴 ∈ dom 𝑅1𝑥𝐴) → suc 𝑥𝐴)
6354, 19sylib 220 . . . . . . 7 ((𝐴 ∈ dom 𝑅1𝑥𝐴) → suc 𝑥 ∈ dom 𝑅1)
64 simpl 485 . . . . . . 7 ((𝐴 ∈ dom 𝑅1𝑥𝐴) → 𝐴 ∈ dom 𝑅1)
65 r1ord3g 9207 . . . . . . 7 ((suc 𝑥 ∈ dom 𝑅1𝐴 ∈ dom 𝑅1) → (suc 𝑥𝐴 → (𝑅1‘suc 𝑥) ⊆ (𝑅1𝐴)))
6663, 64, 65syl2anc 586 . . . . . 6 ((𝐴 ∈ dom 𝑅1𝑥𝐴) → (suc 𝑥𝐴 → (𝑅1‘suc 𝑥) ⊆ (𝑅1𝐴)))
6762, 66mpd 15 . . . . 5 ((𝐴 ∈ dom 𝑅1𝑥𝐴) → (𝑅1‘suc 𝑥) ⊆ (𝑅1𝐴))
6855, 67eqsstrrd 4005 . . . 4 ((𝐴 ∈ dom 𝑅1𝑥𝐴) → 𝒫 (𝑅1𝑥) ⊆ (𝑅1𝐴))
6968ralrimiva 3182 . . 3 (𝐴 ∈ dom 𝑅1 → ∀𝑥𝐴 𝒫 (𝑅1𝑥) ⊆ (𝑅1𝐴))
70 iunss 4968 . . 3 ( 𝑥𝐴 𝒫 (𝑅1𝑥) ⊆ (𝑅1𝐴) ↔ ∀𝑥𝐴 𝒫 (𝑅1𝑥) ⊆ (𝑅1𝐴))
7169, 70sylibr 236 . 2 (𝐴 ∈ dom 𝑅1 𝑥𝐴 𝒫 (𝑅1𝑥) ⊆ (𝑅1𝐴))
7251, 71eqssd 3983 1 (𝐴 ∈ dom 𝑅1 → (𝑅1𝐴) = 𝑥𝐴 𝒫 (𝑅1𝑥))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 208  wa 398  w3o 1082   = wceq 1533  wcel 2110  wral 3138  wrex 3139  Vcvv 3494  wss 3935  c0 4290  𝒫 cpw 4538   ciun 4918  Tr wtr 5171  dom cdm 5554  Ord word 6189  Oncon0 6190  Lim wlim 6191  suc csuc 6192  Fun wfun 6348  cfv 6354  𝑅1cr1 9190
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-sep 5202  ax-nul 5209  ax-pow 5265  ax-pr 5329  ax-un 7460
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-reu 3145  df-rab 3147  df-v 3496  df-sbc 3772  df-csb 3883  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-pss 3953  df-nul 4291  df-if 4467  df-pw 4540  df-sn 4567  df-pr 4569  df-tp 4571  df-op 4573  df-uni 4838  df-iun 4920  df-br 5066  df-opab 5128  df-mpt 5146  df-tr 5172  df-id 5459  df-eprel 5464  df-po 5473  df-so 5474  df-fr 5513  df-we 5515  df-xp 5560  df-rel 5561  df-cnv 5562  df-co 5563  df-dm 5564  df-rn 5565  df-res 5566  df-ima 5567  df-pred 6147  df-ord 6193  df-on 6194  df-lim 6195  df-suc 6196  df-iota 6313  df-fun 6356  df-fn 6357  df-f 6358  df-f1 6359  df-fo 6360  df-f1o 6361  df-fv 6362  df-om 7580  df-wrecs 7946  df-recs 8007  df-rdg 8045  df-r1 9192
This theorem is referenced by:  rankr1ai  9226  r1val3  9266
  Copyright terms: Public domain W3C validator