Metamath Proof Explorer

Theorem intgru

Description: The intersection of a family of universes is a universe. (Contributed by Mario Carneiro, 9-Jun-2013)

Ref Expression
Assertion intgru ⊢ A ⊆ Univ ∧ A ≠ ∅ → ⋂ A ∈ Univ

Proof

Step Hyp Ref Expression
1 simpr ⊢ A ⊆ Univ ∧ A ≠ ∅ → A ≠ ∅
2 intex ⊢ A ≠ ∅ ↔ ⋂ A ∈ V
3 1 2 sylib ⊢ A ⊆ Univ ∧ A ≠ ∅ → ⋂ A ∈ V
4 dfss3 ⊢ A ⊆ Univ ↔ ∀ u ∈ A u ∈ Univ
5 grutr ⊢ u ∈ Univ → Tr ⁡ u
6 5 ralimi ⊢ ∀ u ∈ A u ∈ Univ → ∀ u ∈ A Tr ⁡ u
7 4 6 sylbi ⊢ A ⊆ Univ → ∀ u ∈ A Tr ⁡ u
8 trint ⊢ ∀ u ∈ A Tr ⁡ u → Tr ⁡ ⋂ A
9 7 8 syl ⊢ A ⊆ Univ → Tr ⁡ ⋂ A
10 9 adantr ⊢ A ⊆ Univ ∧ A ≠ ∅ → Tr ⁡ ⋂ A
11 grupw ⊢ u ∈ Univ ∧ x ∈ u → 𝒫 x ∈ u
12 11 ex ⊢ u ∈ Univ → x ∈ u → 𝒫 x ∈ u
13 12 ral2imi ⊢ ∀ u ∈ A u ∈ Univ → ∀ u ∈ A x ∈ u → ∀ u ∈ A 𝒫 x ∈ u
14 vex ⊢ x ∈ V
15 14 elint2 ⊢ x ∈ ⋂ A ↔ ∀ u ∈ A x ∈ u
16 vpwex ⊢ 𝒫 x ∈ V
17 16 elint2 ⊢ 𝒫 x ∈ ⋂ A ↔ ∀ u ∈ A 𝒫 x ∈ u
18 13 15 17 3imtr4g ⊢ ∀ u ∈ A u ∈ Univ → x ∈ ⋂ A → 𝒫 x ∈ ⋂ A
19 18 imp ⊢ ∀ u ∈ A u ∈ Univ ∧ x ∈ ⋂ A → 𝒫 x ∈ ⋂ A
20 19 adantlr ⊢ ∀ u ∈ A u ∈ Univ ∧ A ≠ ∅ ∧ x ∈ ⋂ A → 𝒫 x ∈ ⋂ A
21 r19.26 ⊢ ∀ u ∈ A u ∈ Univ ∧ x ∈ u ↔ ∀ u ∈ A u ∈ Univ ∧ ∀ u ∈ A x ∈ u
22 grupr ⊢ u ∈ Univ ∧ x ∈ u ∧ y ∈ u → x y ∈ u
23 22 3expia ⊢ u ∈ Univ ∧ x ∈ u → y ∈ u → x y ∈ u
24 23 ral2imi ⊢ ∀ u ∈ A u ∈ Univ ∧ x ∈ u → ∀ u ∈ A y ∈ u → ∀ u ∈ A x y ∈ u
25 21 24 sylbir ⊢ ∀ u ∈ A u ∈ Univ ∧ ∀ u ∈ A x ∈ u → ∀ u ∈ A y ∈ u → ∀ u ∈ A x y ∈ u
26 vex ⊢ y ∈ V
27 26 elint2 ⊢ y ∈ ⋂ A ↔ ∀ u ∈ A y ∈ u
28 prex ⊢ x y ∈ V
29 28 elint2 ⊢ x y ∈ ⋂ A ↔ ∀ u ∈ A x y ∈ u
30 25 27 29 3imtr4g ⊢ ∀ u ∈ A u ∈ Univ ∧ ∀ u ∈ A x ∈ u → y ∈ ⋂ A → x y ∈ ⋂ A
31 15 30 sylan2b ⊢ ∀ u ∈ A u ∈ Univ ∧ x ∈ ⋂ A → y ∈ ⋂ A → x y ∈ ⋂ A
32 31 ralrimiv ⊢ ∀ u ∈ A u ∈ Univ ∧ x ∈ ⋂ A → ∀ y ∈ ⋂ A x y ∈ ⋂ A
33 32 adantlr ⊢ ∀ u ∈ A u ∈ Univ ∧ A ≠ ∅ ∧ x ∈ ⋂ A → ∀ y ∈ ⋂ A x y ∈ ⋂ A
34 elmapg ⊢ ⋂ A ∈ V ∧ x ∈ V → y ∈ ⋂ A x ↔ y : x ⟶ ⋂ A
35 34 elvd ⊢ ⋂ A ∈ V → y ∈ ⋂ A x ↔ y : x ⟶ ⋂ A
36 2 35 sylbi ⊢ A ≠ ∅ → y ∈ ⋂ A x ↔ y : x ⟶ ⋂ A
37 36 ad2antlr ⊢ ∀ u ∈ A u ∈ Univ ∧ A ≠ ∅ ∧ x ∈ ⋂ A → y ∈ ⋂ A x ↔ y : x ⟶ ⋂ A
38 intss1 ⊢ u ∈ A → ⋂ A ⊆ u
39 fss ⊢ y : x ⟶ ⋂ A ∧ ⋂ A ⊆ u → y : x ⟶ u
40 38 39 sylan2 ⊢ y : x ⟶ ⋂ A ∧ u ∈ A → y : x ⟶ u
41 40 ralrimiva ⊢ y : x ⟶ ⋂ A → ∀ u ∈ A y : x ⟶ u
42 gruurn ⊢ u ∈ Univ ∧ x ∈ u ∧ y : x ⟶ u → ⋃ ran ⁡ y ∈ u
43 42 3expia ⊢ u ∈ Univ ∧ x ∈ u → y : x ⟶ u → ⋃ ran ⁡ y ∈ u
44 43 ral2imi ⊢ ∀ u ∈ A u ∈ Univ ∧ x ∈ u → ∀ u ∈ A y : x ⟶ u → ∀ u ∈ A ⋃ ran ⁡ y ∈ u
45 21 44 sylbir ⊢ ∀ u ∈ A u ∈ Univ ∧ ∀ u ∈ A x ∈ u → ∀ u ∈ A y : x ⟶ u → ∀ u ∈ A ⋃ ran ⁡ y ∈ u
46 15 45 sylan2b ⊢ ∀ u ∈ A u ∈ Univ ∧ x ∈ ⋂ A → ∀ u ∈ A y : x ⟶ u → ∀ u ∈ A ⋃ ran ⁡ y ∈ u
47 41 46 syl5 ⊢ ∀ u ∈ A u ∈ Univ ∧ x ∈ ⋂ A → y : x ⟶ ⋂ A → ∀ u ∈ A ⋃ ran ⁡ y ∈ u
48 26 rnex ⊢ ran ⁡ y ∈ V
49 48 uniex ⊢ ⋃ ran ⁡ y ∈ V
50 49 elint2 ⊢ ⋃ ran ⁡ y ∈ ⋂ A ↔ ∀ u ∈ A ⋃ ran ⁡ y ∈ u
51 47 50 syl6ibr ⊢ ∀ u ∈ A u ∈ Univ ∧ x ∈ ⋂ A → y : x ⟶ ⋂ A → ⋃ ran ⁡ y ∈ ⋂ A
52 51 adantlr ⊢ ∀ u ∈ A u ∈ Univ ∧ A ≠ ∅ ∧ x ∈ ⋂ A → y : x ⟶ ⋂ A → ⋃ ran ⁡ y ∈ ⋂ A
53 37 52 sylbid ⊢ ∀ u ∈ A u ∈ Univ ∧ A ≠ ∅ ∧ x ∈ ⋂ A → y ∈ ⋂ A x → ⋃ ran ⁡ y ∈ ⋂ A
54 53 ralrimiv ⊢ ∀ u ∈ A u ∈ Univ ∧ A ≠ ∅ ∧ x ∈ ⋂ A → ∀ y ∈ ⋂ A x ⋃ ran ⁡ y ∈ ⋂ A
55 20 33 54 3jca ⊢ ∀ u ∈ A u ∈ Univ ∧ A ≠ ∅ ∧ x ∈ ⋂ A → 𝒫 x ∈ ⋂ A ∧ ∀ y ∈ ⋂ A x y ∈ ⋂ A ∧ ∀ y ∈ ⋂ A x ⋃ ran ⁡ y ∈ ⋂ A
56 55 ralrimiva ⊢ ∀ u ∈ A u ∈ Univ ∧ A ≠ ∅ → ∀ x ∈ ⋂ A 𝒫 x ∈ ⋂ A ∧ ∀ y ∈ ⋂ A x y ∈ ⋂ A ∧ ∀ y ∈ ⋂ A x ⋃ ran ⁡ y ∈ ⋂ A
57 4 56 sylanb ⊢ A ⊆ Univ ∧ A ≠ ∅ → ∀ x ∈ ⋂ A 𝒫 x ∈ ⋂ A ∧ ∀ y ∈ ⋂ A x y ∈ ⋂ A ∧ ∀ y ∈ ⋂ A x ⋃ ran ⁡ y ∈ ⋂ A
58 elgrug ⊢ ⋂ A ∈ V → ⋂ A ∈ Univ ↔ Tr ⁡ ⋂ A ∧ ∀ x ∈ ⋂ A 𝒫 x ∈ ⋂ A ∧ ∀ y ∈ ⋂ A x y ∈ ⋂ A ∧ ∀ y ∈ ⋂ A x ⋃ ran ⁡ y ∈ ⋂ A
59 58 biimpar ⊢ ⋂ A ∈ V ∧ Tr ⁡ ⋂ A ∧ ∀ x ∈ ⋂ A 𝒫 x ∈ ⋂ A ∧ ∀ y ∈ ⋂ A x y ∈ ⋂ A ∧ ∀ y ∈ ⋂ A x ⋃ ran ⁡ y ∈ ⋂ A → ⋂ A ∈ Univ
60 3 10 57 59 syl12anc ⊢ A ⊆ Univ ∧ A ≠ ∅ → ⋂ A ∈ Univ