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 ( ( 𝐴 ⊆ Univ ∧ 𝐴 ≠ ∅ ) → ∩ 𝐴 ∈ Univ )

Proof

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