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

Theorem r1tr 8890
Description: The cumulative hierarchy of sets is transitive. Lemma 7T of [Enderton] p. 202. (Contributed by NM, 8-Sep-2003.) (Revised by Mario Carneiro, 16-Nov-2014.)
Assertion
Ref Expression
r1tr Tr (𝑅1𝐴)

Proof of Theorem r1tr
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 r1funlim 8880 . . . . . 6 (Fun 𝑅1 ∧ Lim dom 𝑅1)
21simpri 480 . . . . 5 Lim dom 𝑅1
3 limord 6001 . . . . 5 (Lim dom 𝑅1 → Ord dom 𝑅1)
4 ordsson 7224 . . . . 5 (Ord dom 𝑅1 → dom 𝑅1 ⊆ On)
52, 3, 4mp2b 10 . . . 4 dom 𝑅1 ⊆ On
65sseli 3795 . . 3 (𝐴 ∈ dom 𝑅1𝐴 ∈ On)
7 fveq2 6412 . . . . . 6 (𝑥 = ∅ → (𝑅1𝑥) = (𝑅1‘∅))
8 r10 8882 . . . . . 6 (𝑅1‘∅) = ∅
97, 8syl6eq 2850 . . . . 5 (𝑥 = ∅ → (𝑅1𝑥) = ∅)
10 treq 4952 . . . . 5 ((𝑅1𝑥) = ∅ → (Tr (𝑅1𝑥) ↔ Tr ∅))
119, 10syl 17 . . . 4 (𝑥 = ∅ → (Tr (𝑅1𝑥) ↔ Tr ∅))
12 fveq2 6412 . . . . 5 (𝑥 = 𝑦 → (𝑅1𝑥) = (𝑅1𝑦))
13 treq 4952 . . . . 5 ((𝑅1𝑥) = (𝑅1𝑦) → (Tr (𝑅1𝑥) ↔ Tr (𝑅1𝑦)))
1412, 13syl 17 . . . 4 (𝑥 = 𝑦 → (Tr (𝑅1𝑥) ↔ Tr (𝑅1𝑦)))
15 fveq2 6412 . . . . 5 (𝑥 = suc 𝑦 → (𝑅1𝑥) = (𝑅1‘suc 𝑦))
16 treq 4952 . . . . 5 ((𝑅1𝑥) = (𝑅1‘suc 𝑦) → (Tr (𝑅1𝑥) ↔ Tr (𝑅1‘suc 𝑦)))
1715, 16syl 17 . . . 4 (𝑥 = suc 𝑦 → (Tr (𝑅1𝑥) ↔ Tr (𝑅1‘suc 𝑦)))
18 fveq2 6412 . . . . 5 (𝑥 = 𝐴 → (𝑅1𝑥) = (𝑅1𝐴))
19 treq 4952 . . . . 5 ((𝑅1𝑥) = (𝑅1𝐴) → (Tr (𝑅1𝑥) ↔ Tr (𝑅1𝐴)))
2018, 19syl 17 . . . 4 (𝑥 = 𝐴 → (Tr (𝑅1𝑥) ↔ Tr (𝑅1𝐴)))
21 tr0 4957 . . . 4 Tr ∅
22 limsuc 7284 . . . . . . . 8 (Lim dom 𝑅1 → (𝑦 ∈ dom 𝑅1 ↔ suc 𝑦 ∈ dom 𝑅1))
232, 22ax-mp 5 . . . . . . 7 (𝑦 ∈ dom 𝑅1 ↔ suc 𝑦 ∈ dom 𝑅1)
24 simpr 478 . . . . . . . . 9 ((𝑦 ∈ On ∧ Tr (𝑅1𝑦)) → Tr (𝑅1𝑦))
25 pwtr 5113 . . . . . . . . 9 (Tr (𝑅1𝑦) ↔ Tr 𝒫 (𝑅1𝑦))
2624, 25sylib 210 . . . . . . . 8 ((𝑦 ∈ On ∧ Tr (𝑅1𝑦)) → Tr 𝒫 (𝑅1𝑦))
27 r1sucg 8883 . . . . . . . . 9 (𝑦 ∈ dom 𝑅1 → (𝑅1‘suc 𝑦) = 𝒫 (𝑅1𝑦))
28 treq 4952 . . . . . . . . 9 ((𝑅1‘suc 𝑦) = 𝒫 (𝑅1𝑦) → (Tr (𝑅1‘suc 𝑦) ↔ Tr 𝒫 (𝑅1𝑦)))
2927, 28syl 17 . . . . . . . 8 (𝑦 ∈ dom 𝑅1 → (Tr (𝑅1‘suc 𝑦) ↔ Tr 𝒫 (𝑅1𝑦)))
3026, 29syl5ibrcom 239 . . . . . . 7 ((𝑦 ∈ On ∧ Tr (𝑅1𝑦)) → (𝑦 ∈ dom 𝑅1 → Tr (𝑅1‘suc 𝑦)))
3123, 30syl5bir 235 . . . . . 6 ((𝑦 ∈ On ∧ Tr (𝑅1𝑦)) → (suc 𝑦 ∈ dom 𝑅1 → Tr (𝑅1‘suc 𝑦)))
32 ndmfv 6442 . . . . . . . 8 (¬ suc 𝑦 ∈ dom 𝑅1 → (𝑅1‘suc 𝑦) = ∅)
33 treq 4952 . . . . . . . 8 ((𝑅1‘suc 𝑦) = ∅ → (Tr (𝑅1‘suc 𝑦) ↔ Tr ∅))
3432, 33syl 17 . . . . . . 7 (¬ suc 𝑦 ∈ dom 𝑅1 → (Tr (𝑅1‘suc 𝑦) ↔ Tr ∅))
3521, 34mpbiri 250 . . . . . 6 (¬ suc 𝑦 ∈ dom 𝑅1 → Tr (𝑅1‘suc 𝑦))
3631, 35pm2.61d1 173 . . . . 5 ((𝑦 ∈ On ∧ Tr (𝑅1𝑦)) → Tr (𝑅1‘suc 𝑦))
3736ex 402 . . . 4 (𝑦 ∈ On → (Tr (𝑅1𝑦) → Tr (𝑅1‘suc 𝑦)))
38 triun 4959 . . . . . . . 8 (∀𝑦𝑥 Tr (𝑅1𝑦) → Tr 𝑦𝑥 (𝑅1𝑦))
39 r1limg 8885 . . . . . . . . . 10 ((𝑥 ∈ dom 𝑅1 ∧ Lim 𝑥) → (𝑅1𝑥) = 𝑦𝑥 (𝑅1𝑦))
4039ancoms 451 . . . . . . . . 9 ((Lim 𝑥𝑥 ∈ dom 𝑅1) → (𝑅1𝑥) = 𝑦𝑥 (𝑅1𝑦))
41 treq 4952 . . . . . . . . 9 ((𝑅1𝑥) = 𝑦𝑥 (𝑅1𝑦) → (Tr (𝑅1𝑥) ↔ Tr 𝑦𝑥 (𝑅1𝑦)))
4240, 41syl 17 . . . . . . . 8 ((Lim 𝑥𝑥 ∈ dom 𝑅1) → (Tr (𝑅1𝑥) ↔ Tr 𝑦𝑥 (𝑅1𝑦)))
4338, 42syl5ibr 238 . . . . . . 7 ((Lim 𝑥𝑥 ∈ dom 𝑅1) → (∀𝑦𝑥 Tr (𝑅1𝑦) → Tr (𝑅1𝑥)))
4443impancom 444 . . . . . 6 ((Lim 𝑥 ∧ ∀𝑦𝑥 Tr (𝑅1𝑦)) → (𝑥 ∈ dom 𝑅1 → Tr (𝑅1𝑥)))
45 ndmfv 6442 . . . . . . . 8 𝑥 ∈ dom 𝑅1 → (𝑅1𝑥) = ∅)
4645, 10syl 17 . . . . . . 7 𝑥 ∈ dom 𝑅1 → (Tr (𝑅1𝑥) ↔ Tr ∅))
4721, 46mpbiri 250 . . . . . 6 𝑥 ∈ dom 𝑅1 → Tr (𝑅1𝑥))
4844, 47pm2.61d1 173 . . . . 5 ((Lim 𝑥 ∧ ∀𝑦𝑥 Tr (𝑅1𝑦)) → Tr (𝑅1𝑥))
4948ex 402 . . . 4 (Lim 𝑥 → (∀𝑦𝑥 Tr (𝑅1𝑦) → Tr (𝑅1𝑥)))
5011, 14, 17, 20, 21, 37, 49tfinds 7294 . . 3 (𝐴 ∈ On → Tr (𝑅1𝐴))
516, 50syl 17 . 2 (𝐴 ∈ dom 𝑅1 → Tr (𝑅1𝐴))
52 ndmfv 6442 . . . 4 𝐴 ∈ dom 𝑅1 → (𝑅1𝐴) = ∅)
53 treq 4952 . . . 4 ((𝑅1𝐴) = ∅ → (Tr (𝑅1𝐴) ↔ Tr ∅))
5452, 53syl 17 . . 3 𝐴 ∈ dom 𝑅1 → (Tr (𝑅1𝐴) ↔ Tr ∅))
5521, 54mpbiri 250 . 2 𝐴 ∈ dom 𝑅1 → Tr (𝑅1𝐴))
5651, 55pm2.61i 177 1 Tr (𝑅1𝐴)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 198  wa 385   = wceq 1653  wcel 2157  wral 3090  wss 3770  c0 4116  𝒫 cpw 4350   ciun 4711  Tr wtr 4946  dom cdm 5313  Ord word 5941  Oncon0 5942  Lim wlim 5943  suc csuc 5944  Fun wfun 6096  cfv 6102  𝑅1cr1 8876
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-8 2159  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-13 2378  ax-ext 2778  ax-sep 4976  ax-nul 4984  ax-pow 5036  ax-pr 5098  ax-un 7184
This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-3or 1109  df-3an 1110  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-mo 2592  df-eu 2610  df-clab 2787  df-cleq 2793  df-clel 2796  df-nfc 2931  df-ne 2973  df-ral 3095  df-rex 3096  df-reu 3097  df-rab 3099  df-v 3388  df-sbc 3635  df-csb 3730  df-dif 3773  df-un 3775  df-in 3777  df-ss 3784  df-pss 3786  df-nul 4117  df-if 4279  df-pw 4352  df-sn 4370  df-pr 4372  df-tp 4374  df-op 4376  df-uni 4630  df-iun 4713  df-br 4845  df-opab 4907  df-mpt 4924  df-tr 4947  df-id 5221  df-eprel 5226  df-po 5234  df-so 5235  df-fr 5272  df-we 5274  df-xp 5319  df-rel 5320  df-cnv 5321  df-co 5322  df-dm 5323  df-rn 5324  df-res 5325  df-ima 5326  df-pred 5899  df-ord 5945  df-on 5946  df-lim 5947  df-suc 5948  df-iota 6065  df-fun 6104  df-fn 6105  df-f 6106  df-f1 6107  df-fo 6108  df-f1o 6109  df-fv 6110  df-om 7301  df-wrecs 7646  df-recs 7708  df-rdg 7746  df-r1 8878
This theorem is referenced by:  r1tr2  8891  r1ordg  8892  r1ord3g  8893  r1ord2  8895  r1sssuc  8897  r1pwss  8898  r1val1  8900  rankwflemb  8907  r1elwf  8910  r1elssi  8919  uniwf  8933  tcrank  8998  ackbij2lem3  9352  r1limwun  9847  tskr1om2  9879
  Copyright terms: Public domain W3C validator