MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  gruelss Structured version   Unicode version

Theorem gruelss 9101
Description: A Grothendieck universe is transitive, so each element is a subset of the universe. (Contributed by Mario Carneiro, 9-Jun-2013.)
Assertion
Ref Expression
gruelss  |-  ( ( U  e.  Univ  /\  A  e.  U )  ->  A  C_  U )

Proof of Theorem gruelss
StepHypRef Expression
1 grutr 9100 . 2  |-  ( U  e.  Univ  ->  Tr  U
)
2 trss 4482 . . 3  |-  ( Tr  U  ->  ( A  e.  U  ->  A  C_  U ) )
32imp 427 . 2  |-  ( ( Tr  U  /\  A  e.  U )  ->  A  C_  U )
41, 3sylan 469 1  |-  ( ( U  e.  Univ  /\  A  e.  U )  ->  A  C_  U )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    e. wcel 1836    C_ wss 3402   Tr wtr 4473   Univcgru 9097
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1633  ax-4 1646  ax-5 1719  ax-6 1765  ax-7 1808  ax-10 1855  ax-11 1860  ax-12 1872  ax-13 2016  ax-ext 2370
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1402  df-ex 1628  df-nf 1632  df-sb 1758  df-clab 2378  df-cleq 2384  df-clel 2387  df-nfc 2542  df-ral 2747  df-rex 2748  df-rab 2751  df-v 3049  df-dif 3405  df-un 3407  df-in 3409  df-ss 3416  df-nul 3725  df-if 3871  df-sn 3958  df-pr 3960  df-op 3964  df-uni 4177  df-br 4381  df-tr 4474  df-iota 5473  df-fv 5517  df-ov 6217  df-gru 9098
This theorem is referenced by:  gruss  9103  gruuni  9107  gruel  9110  grur1a  9126  grur1  9127
  Copyright terms: Public domain W3C validator