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