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 ( ( 𝑈 ∈ Univ ∧ 𝐴 ⊆ 𝑈 ∧ ( 𝐵 ∈ 𝑈 ∧ 𝐵 ≈ 𝐴 ) ) → 𝐴 ∈ 𝑈 )

Proof

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