Description: A Grothendieck universe contains all subsets of itself that are equipotent to an element of the universe. (Contributed by Mario Carneiro, 9-Jun-2013)
Ref | Expression | ||
---|---|---|---|
Assertion | gruen | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bren | |
|
2 | f1ofo | |
|
3 | simp3l | |
|
4 | forn | |
|
5 | 3 4 | syl | |
6 | fof | |
|
7 | fss | |
|
8 | 6 7 | sylan | |
9 | grurn | |
|
10 | 8 9 | syl3an3 | |
11 | 5 10 | eqeltrrd | |
12 | 11 | 3expia | |
13 | 12 | expd | |
14 | 2 13 | syl5 | |
15 | 14 | exlimdv | |
16 | 15 | com3r | |
17 | 16 | expdimp | |
18 | 1 17 | syl7bi | |
19 | 18 | impd | |
20 | 19 | ancoms | |
21 | 20 | 3impia | |