Metamath Proof Explorer


Theorem gruen

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 UUnivAUBUBAAU

Proof

Step Hyp Ref Expression
1 bren BAyy:B1-1 ontoA
2 f1ofo y:B1-1 ontoAy:BontoA
3 simp3l UUnivBUy:BontoAAUy:BontoA
4 forn y:BontoArany=A
5 3 4 syl UUnivBUy:BontoAAUrany=A
6 fof y:BontoAy:BA
7 fss y:BAAUy:BU
8 6 7 sylan y:BontoAAUy:BU
9 grurn UUnivBUy:BUranyU
10 8 9 syl3an3 UUnivBUy:BontoAAUranyU
11 5 10 eqeltrrd UUnivBUy:BontoAAUAU
12 11 3expia UUnivBUy:BontoAAUAU
13 12 expd UUnivBUy:BontoAAUAU
14 2 13 syl5 UUnivBUy:B1-1 ontoAAUAU
15 14 exlimdv UUnivBUyy:B1-1 ontoAAUAU
16 15 com3r AUUUnivBUyy:B1-1 ontoAAU
17 16 expdimp AUUUnivBUyy:B1-1 ontoAAU
18 1 17 syl7bi AUUUnivBUBAAU
19 18 impd AUUUnivBUBAAU
20 19 ancoms UUnivAUBUBAAU
21 20 3impia UUnivAUBUBAAU