# 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 ${⊢}\left({U}\in \mathrm{Univ}\wedge {A}\subseteq {U}\wedge \left({B}\in {U}\wedge {B}\approx {A}\right)\right)\to {A}\in {U}$

### Proof

Step Hyp Ref Expression
1 bren ${⊢}{B}\approx {A}↔\exists {y}\phantom{\rule{.4em}{0ex}}{y}:{B}\underset{1-1 onto}{⟶}{A}$
2 f1ofo ${⊢}{y}:{B}\underset{1-1 onto}{⟶}{A}\to {y}:{B}\underset{onto}{⟶}{A}$
3 simp3l ${⊢}\left({U}\in \mathrm{Univ}\wedge {B}\in {U}\wedge \left({y}:{B}\underset{onto}{⟶}{A}\wedge {A}\subseteq {U}\right)\right)\to {y}:{B}\underset{onto}{⟶}{A}$
4 forn ${⊢}{y}:{B}\underset{onto}{⟶}{A}\to \mathrm{ran}{y}={A}$
5 3 4 syl ${⊢}\left({U}\in \mathrm{Univ}\wedge {B}\in {U}\wedge \left({y}:{B}\underset{onto}{⟶}{A}\wedge {A}\subseteq {U}\right)\right)\to \mathrm{ran}{y}={A}$
6 fof ${⊢}{y}:{B}\underset{onto}{⟶}{A}\to {y}:{B}⟶{A}$
7 fss ${⊢}\left({y}:{B}⟶{A}\wedge {A}\subseteq {U}\right)\to {y}:{B}⟶{U}$
8 6 7 sylan ${⊢}\left({y}:{B}\underset{onto}{⟶}{A}\wedge {A}\subseteq {U}\right)\to {y}:{B}⟶{U}$
9 grurn ${⊢}\left({U}\in \mathrm{Univ}\wedge {B}\in {U}\wedge {y}:{B}⟶{U}\right)\to \mathrm{ran}{y}\in {U}$
10 8 9 syl3an3 ${⊢}\left({U}\in \mathrm{Univ}\wedge {B}\in {U}\wedge \left({y}:{B}\underset{onto}{⟶}{A}\wedge {A}\subseteq {U}\right)\right)\to \mathrm{ran}{y}\in {U}$
11 5 10 eqeltrrd ${⊢}\left({U}\in \mathrm{Univ}\wedge {B}\in {U}\wedge \left({y}:{B}\underset{onto}{⟶}{A}\wedge {A}\subseteq {U}\right)\right)\to {A}\in {U}$
12 11 3expia ${⊢}\left({U}\in \mathrm{Univ}\wedge {B}\in {U}\right)\to \left(\left({y}:{B}\underset{onto}{⟶}{A}\wedge {A}\subseteq {U}\right)\to {A}\in {U}\right)$
13 12 expd ${⊢}\left({U}\in \mathrm{Univ}\wedge {B}\in {U}\right)\to \left({y}:{B}\underset{onto}{⟶}{A}\to \left({A}\subseteq {U}\to {A}\in {U}\right)\right)$
14 2 13 syl5 ${⊢}\left({U}\in \mathrm{Univ}\wedge {B}\in {U}\right)\to \left({y}:{B}\underset{1-1 onto}{⟶}{A}\to \left({A}\subseteq {U}\to {A}\in {U}\right)\right)$
15 14 exlimdv ${⊢}\left({U}\in \mathrm{Univ}\wedge {B}\in {U}\right)\to \left(\exists {y}\phantom{\rule{.4em}{0ex}}{y}:{B}\underset{1-1 onto}{⟶}{A}\to \left({A}\subseteq {U}\to {A}\in {U}\right)\right)$
16 15 com3r ${⊢}{A}\subseteq {U}\to \left(\left({U}\in \mathrm{Univ}\wedge {B}\in {U}\right)\to \left(\exists {y}\phantom{\rule{.4em}{0ex}}{y}:{B}\underset{1-1 onto}{⟶}{A}\to {A}\in {U}\right)\right)$
17 16 expdimp ${⊢}\left({A}\subseteq {U}\wedge {U}\in \mathrm{Univ}\right)\to \left({B}\in {U}\to \left(\exists {y}\phantom{\rule{.4em}{0ex}}{y}:{B}\underset{1-1 onto}{⟶}{A}\to {A}\in {U}\right)\right)$
18 1 17 syl7bi ${⊢}\left({A}\subseteq {U}\wedge {U}\in \mathrm{Univ}\right)\to \left({B}\in {U}\to \left({B}\approx {A}\to {A}\in {U}\right)\right)$
19 18 impd ${⊢}\left({A}\subseteq {U}\wedge {U}\in \mathrm{Univ}\right)\to \left(\left({B}\in {U}\wedge {B}\approx {A}\right)\to {A}\in {U}\right)$
20 19 ancoms ${⊢}\left({U}\in \mathrm{Univ}\wedge {A}\subseteq {U}\right)\to \left(\left({B}\in {U}\wedge {B}\approx {A}\right)\to {A}\in {U}\right)$
21 20 3impia ${⊢}\left({U}\in \mathrm{Univ}\wedge {A}\subseteq {U}\wedge \left({B}\in {U}\wedge {B}\approx {A}\right)\right)\to {A}\in {U}$