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