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 ∈ Univ ∧ A ⊆ U ∧ B ∈ U ∧ B ≈ A → A ∈ U

Proof

Step Hyp Ref Expression
1 bren ⊢ B ≈ A ↔ ∃ y y : B ⟶ 1-1 onto A
2 f1ofo ⊢ y : B ⟶ 1-1 onto A → y : B ⟶ onto A
3 simp3l ⊢ U ∈ Univ ∧ B ∈ U ∧ y : B ⟶ onto A ∧ A ⊆ U → y : B ⟶ onto A
4 forn ⊢ y : B ⟶ onto A → ran ⁡ y = A
5 3 4 syl ⊢ U ∈ Univ ∧ B ∈ U ∧ y : B ⟶ onto A ∧ A ⊆ U → ran ⁡ y = A
6 fof ⊢ y : B ⟶ onto A → y : B ⟶ A
7 fss ⊢ y : B ⟶ A ∧ A ⊆ U → y : B ⟶ U
8 6 7 sylan ⊢ y : B ⟶ onto A ∧ A ⊆ U → y : B ⟶ U
9 grurn ⊢ U ∈ Univ ∧ B ∈ U ∧ y : B ⟶ U → ran ⁡ y ∈ U
10 8 9 syl3an3 ⊢ U ∈ Univ ∧ B ∈ U ∧ y : B ⟶ onto A ∧ A ⊆ U → ran ⁡ y ∈ U
11 5 10 eqeltrrd ⊢ U ∈ Univ ∧ B ∈ U ∧ y : B ⟶ onto A ∧ A ⊆ U → A ∈ U
12 11 3expia ⊢ U ∈ Univ ∧ B ∈ U → y : B ⟶ onto A ∧ A ⊆ U → A ∈ U
13 12 expd ⊢ U ∈ Univ ∧ B ∈ U → y : B ⟶ onto A → A ⊆ U → A ∈ U
14 2 13 syl5 ⊢ U ∈ Univ ∧ B ∈ U → y : B ⟶ 1-1 onto A → A ⊆ U → A ∈ U
15 14 exlimdv ⊢ U ∈ Univ ∧ B ∈ U → ∃ y y : B ⟶ 1-1 onto A → A ⊆ U → A ∈ U
16 15 com3r ⊢ A ⊆ U → U ∈ Univ ∧ B ∈ U → ∃ y y : B ⟶ 1-1 onto A → A ∈ U
17 16 expdimp ⊢ A ⊆ U ∧ U ∈ Univ → B ∈ U → ∃ y y : B ⟶ 1-1 onto A → A ∈ U
18 1 17 syl7bi ⊢ A ⊆ U ∧ U ∈ Univ → B ∈ U → B ≈ A → A ∈ U
19 18 impd ⊢ A ⊆ U ∧ U ∈ Univ → B ∈ U ∧ B ≈ A → A ∈ U
20 19 ancoms ⊢ U ∈ Univ ∧ A ⊆ U → B ∈ U ∧ B ≈ A → A ∈ U
21 20 3impia ⊢ U ∈ Univ ∧ A ⊆ U ∧ B ∈ U ∧ B ≈ A → A ∈ U