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 
|- ( ( U e. Univ /\ A C_ U /\ ( B e. U /\ B ~~ A ) ) -> A e. U )

Proof

Step Hyp Ref Expression
1 bren 
 |-  ( B ~~ A <-> E. y y : B -1-1-onto-> A )
2 f1ofo 
 |-  ( y : B -1-1-onto-> A -> y : B -onto-> A )
3 simp3l 
 |-  ( ( U e. Univ /\ B e. U /\ ( y : B -onto-> A /\ A C_ U ) ) -> y : B -onto-> A )
4 forn 
 |-  ( y : B -onto-> A -> ran y = A )
5 3 4 syl 
 |-  ( ( U e. Univ /\ B e. U /\ ( y : B -onto-> A /\ A C_ U ) ) -> ran y = A )
6 fof 
 |-  ( y : B -onto-> A -> y : B --> A )
7 fss 
 |-  ( ( y : B --> A /\ A C_ U ) -> y : B --> U )
8 6 7 sylan 
 |-  ( ( y : B -onto-> A /\ A C_ U ) -> y : B --> U )
9 grurn 
 |-  ( ( U e. Univ /\ B e. U /\ y : B --> U ) -> ran y e. U )
10 8 9 syl3an3 
 |-  ( ( U e. Univ /\ B e. U /\ ( y : B -onto-> A /\ A C_ U ) ) -> ran y e. U )
11 5 10 eqeltrrd 
 |-  ( ( U e. Univ /\ B e. U /\ ( y : B -onto-> A /\ A C_ U ) ) -> A e. U )
12 11 3expia 
 |-  ( ( U e. Univ /\ B e. U ) -> ( ( y : B -onto-> A /\ A C_ U ) -> A e. U ) )
13 12 expd 
 |-  ( ( U e. Univ /\ B e. U ) -> ( y : B -onto-> A -> ( A C_ U -> A e. U ) ) )
14 2 13 syl5 
 |-  ( ( U e. Univ /\ B e. U ) -> ( y : B -1-1-onto-> A -> ( A C_ U -> A e. U ) ) )
15 14 exlimdv 
 |-  ( ( U e. Univ /\ B e. U ) -> ( E. y y : B -1-1-onto-> A -> ( A C_ U -> A e. U ) ) )
16 15 com3r 
 |-  ( A C_ U -> ( ( U e. Univ /\ B e. U ) -> ( E. y y : B -1-1-onto-> A -> A e. U ) ) )
17 16 expdimp 
 |-  ( ( A C_ U /\ U e. Univ ) -> ( B e. U -> ( E. y y : B -1-1-onto-> A -> A e. U ) ) )
18 1 17 syl7bi 
 |-  ( ( A C_ U /\ U e. Univ ) -> ( B e. U -> ( B ~~ A -> A e. U ) ) )
19 18 impd 
 |-  ( ( A C_ U /\ U e. Univ ) -> ( ( B e. U /\ B ~~ A ) -> A e. U ) )
20 19 ancoms 
 |-  ( ( U e. Univ /\ A C_ U ) -> ( ( B e. U /\ B ~~ A ) -> A e. U ) )
21 20 3impia 
 |-  ( ( U e. Univ /\ A C_ U /\ ( B e. U /\ B ~~ A ) ) -> A e. U )