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

Theorem grutsk 10034
Description: Grothendieck universes are the same as transitive Tarski classes. (The proof in the forward direction requires Foundation.) (Contributed by Mario Carneiro, 24-Jun-2013.)
Assertion
Ref Expression
grutsk Univ = {𝑥 ∈ Tarski ∣ Tr 𝑥}

Proof of Theorem grutsk
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 0tsk 9967 . . . . . . . 8 ∅ ∈ Tarski
2 eleq1 2847 . . . . . . . 8 (𝑦 = ∅ → (𝑦 ∈ Tarski ↔ ∅ ∈ Tarski))
31, 2mpbiri 250 . . . . . . 7 (𝑦 = ∅ → 𝑦 ∈ Tarski)
43a1i 11 . . . . . 6 (𝑦 ∈ Univ → (𝑦 = ∅ → 𝑦 ∈ Tarski))
5 vex 3412 . . . . . . . . . . 11 𝑦 ∈ V
6 unir1 9028 . . . . . . . . . . 11 (𝑅1 “ On) = V
75, 6eleqtrri 2859 . . . . . . . . . 10 𝑦 (𝑅1 “ On)
8 eqid 2772 . . . . . . . . . . 11 (𝑦 ∩ On) = (𝑦 ∩ On)
98grur1 10032 . . . . . . . . . 10 ((𝑦 ∈ Univ ∧ 𝑦 (𝑅1 “ On)) → 𝑦 = (𝑅1‘(𝑦 ∩ On)))
107, 9mpan2 678 . . . . . . . . 9 (𝑦 ∈ Univ → 𝑦 = (𝑅1‘(𝑦 ∩ On)))
1110adantr 473 . . . . . . . 8 ((𝑦 ∈ Univ ∧ 𝑦 ≠ ∅) → 𝑦 = (𝑅1‘(𝑦 ∩ On)))
128gruina 10030 . . . . . . . . 9 ((𝑦 ∈ Univ ∧ 𝑦 ≠ ∅) → (𝑦 ∩ On) ∈ Inacc)
13 inatsk 9990 . . . . . . . . 9 ((𝑦 ∩ On) ∈ Inacc → (𝑅1‘(𝑦 ∩ On)) ∈ Tarski)
1412, 13syl 17 . . . . . . . 8 ((𝑦 ∈ Univ ∧ 𝑦 ≠ ∅) → (𝑅1‘(𝑦 ∩ On)) ∈ Tarski)
1511, 14eqeltrd 2860 . . . . . . 7 ((𝑦 ∈ Univ ∧ 𝑦 ≠ ∅) → 𝑦 ∈ Tarski)
1615ex 405 . . . . . 6 (𝑦 ∈ Univ → (𝑦 ≠ ∅ → 𝑦 ∈ Tarski))
174, 16pm2.61dne 3048 . . . . 5 (𝑦 ∈ Univ → 𝑦 ∈ Tarski)
18 grutr 10005 . . . . 5 (𝑦 ∈ Univ → Tr 𝑦)
1917, 18jca 504 . . . 4 (𝑦 ∈ Univ → (𝑦 ∈ Tarski ∧ Tr 𝑦))
20 grutsk1 10033 . . . 4 ((𝑦 ∈ Tarski ∧ Tr 𝑦) → 𝑦 ∈ Univ)
2119, 20impbii 201 . . 3 (𝑦 ∈ Univ ↔ (𝑦 ∈ Tarski ∧ Tr 𝑦))
22 treq 5030 . . . 4 (𝑥 = 𝑦 → (Tr 𝑥 ↔ Tr 𝑦))
2322elrab 3589 . . 3 (𝑦 ∈ {𝑥 ∈ Tarski ∣ Tr 𝑥} ↔ (𝑦 ∈ Tarski ∧ Tr 𝑦))
2421, 23bitr4i 270 . 2 (𝑦 ∈ Univ ↔ 𝑦 ∈ {𝑥 ∈ Tarski ∣ Tr 𝑥})
2524eqriv 2769 1 Univ = {𝑥 ∈ Tarski ∣ Tr 𝑥}
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 387   = wceq 1507  wcel 2048  wne 2961  {crab 3086  Vcvv 3409  cin 3824  c0 4173   cuni 4706  Tr wtr 5024  cima 5403  Oncon0 6023  cfv 6182  𝑅1cr1 8977  Inacccina 9895  Tarskictsk 9960  Univcgru 10002
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1964  ax-8 2050  ax-9 2057  ax-10 2077  ax-11 2091  ax-12 2104  ax-13 2299  ax-ext 2745  ax-rep 5043  ax-sep 5054  ax-nul 5061  ax-pow 5113  ax-pr 5180  ax-un 7273  ax-reg 8843  ax-inf2 8890  ax-ac2 9675
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3or 1069  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2014  df-mo 2544  df-eu 2580  df-clab 2754  df-cleq 2765  df-clel 2840  df-nfc 2912  df-ne 2962  df-ral 3087  df-rex 3088  df-reu 3089  df-rmo 3090  df-rab 3091  df-v 3411  df-sbc 3678  df-csb 3783  df-dif 3828  df-un 3830  df-in 3832  df-ss 3839  df-pss 3841  df-nul 4174  df-if 4345  df-pw 4418  df-sn 4436  df-pr 4438  df-tp 4440  df-op 4442  df-uni 4707  df-int 4744  df-iun 4788  df-iin 4789  df-br 4924  df-opab 4986  df-mpt 5003  df-tr 5025  df-id 5305  df-eprel 5310  df-po 5319  df-so 5320  df-fr 5359  df-se 5360  df-we 5361  df-xp 5406  df-rel 5407  df-cnv 5408  df-co 5409  df-dm 5410  df-rn 5411  df-res 5412  df-ima 5413  df-pred 5980  df-ord 6026  df-on 6027  df-lim 6028  df-suc 6029  df-iota 6146  df-fun 6184  df-fn 6185  df-f 6186  df-f1 6187  df-fo 6188  df-f1o 6189  df-fv 6190  df-isom 6191  df-riota 6931  df-ov 6973  df-oprab 6974  df-mpo 6975  df-om 7391  df-1st 7494  df-2nd 7495  df-wrecs 7743  df-smo 7780  df-recs 7805  df-rdg 7843  df-1o 7897  df-2o 7898  df-oadd 7901  df-er 8081  df-map 8200  df-ixp 8252  df-en 8299  df-dom 8300  df-sdom 8301  df-fin 8302  df-oi 8761  df-har 8809  df-tc 8965  df-r1 8979  df-rank 8980  df-card 9154  df-aleph 9155  df-cf 9156  df-acn 9157  df-ac 9328  df-wina 9896  df-ina 9897  df-tsk 9961  df-gru 10003
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator