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∈Au∈Univ
5 grutr ⊢u∈Univ→Tr⁡u
6 5 ralimi ⊢∀u∈Au∈Univ→∀u∈ATr⁡u
7 4 6 sylbi ⊢A⊆Univ→∀u∈ATr⁡u
8 trint ⊢∀u∈ATr⁡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∈Au∈Univ→∀u∈Ax∈u→∀u∈A𝒫x∈u
14 vex ⊢x∈V
15 14 elint2 ⊢x∈⋂A↔∀u∈Ax∈u
16 vpwex ⊢𝒫x∈V
17 16 elint2 ⊢𝒫x∈⋂A↔∀u∈A𝒫x∈u
18 13 15 17 3imtr4g ⊢∀u∈Au∈Univ→x∈⋂A→𝒫x∈⋂A
19 18 imp ⊢∀u∈Au∈Univ∧x∈⋂A→𝒫x∈⋂A
20 19 adantlr ⊢∀u∈Au∈Univ∧A≠∅∧x∈⋂A→𝒫x∈⋂A
21 r19.26 ⊢∀u∈Au∈Univ∧x∈u↔∀u∈Au∈Univ∧∀u∈Ax∈u
22 grupr ⊢u∈Univ∧x∈u∧y∈u→xy∈u
23 22 3expia ⊢u∈Univ∧x∈u→y∈u→xy∈u
24 23 ral2imi ⊢∀u∈Au∈Univ∧x∈u→∀u∈Ay∈u→∀u∈Axy∈u
25 21 24 sylbir ⊢∀u∈Au∈Univ∧∀u∈Ax∈u→∀u∈Ay∈u→∀u∈Axy∈u
26 vex ⊢y∈V
27 26 elint2 ⊢y∈⋂A↔∀u∈Ay∈u
28 prex ⊢xy∈V
29 28 elint2 ⊢xy∈⋂A↔∀u∈Axy∈u
30 25 27 29 3imtr4g ⊢∀u∈Au∈Univ∧∀u∈Ax∈u→y∈⋂A→xy∈⋂A
31 15 30 sylan2b ⊢∀u∈Au∈Univ∧x∈⋂A→y∈⋂A→xy∈⋂A
32 31 ralrimiv ⊢∀u∈Au∈Univ∧x∈⋂A→∀y∈⋂Axy∈⋂A
33 32 adantlr ⊢∀u∈Au∈Univ∧A≠∅∧x∈⋂A→∀y∈⋂Axy∈⋂A
34 elmapg ⊢⋂A∈V∧x∈V→y∈⋂Ax↔y:x⟶⋂A
35 34 elvd ⊢⋂A∈V→y∈⋂Ax↔y:x⟶⋂A
36 2 35 sylbi ⊢A≠∅→y∈⋂Ax↔y:x⟶⋂A
37 36 ad2antlr ⊢∀u∈Au∈Univ∧A≠∅∧x∈⋂A→y∈⋂Ax↔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∈Ay: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∈Au∈Univ∧x∈u→∀u∈Ay:x⟶u→∀u∈A⋃ran⁡y∈u
45 21 44 sylbir ⊢∀u∈Au∈Univ∧∀u∈Ax∈u→∀u∈Ay:x⟶u→∀u∈A⋃ran⁡y∈u
46 15 45 sylan2b ⊢∀u∈Au∈Univ∧x∈⋂A→∀u∈Ay:x⟶u→∀u∈A⋃ran⁡y∈u
47 41 46 syl5 ⊢∀u∈Au∈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∈Au∈Univ∧x∈⋂A→y:x⟶⋂A→⋃ran⁡y∈⋂A
52 51 adantlr ⊢∀u∈Au∈Univ∧A≠∅∧x∈⋂A→y:x⟶⋂A→⋃ran⁡y∈⋂A
53 37 52 sylbid ⊢∀u∈Au∈Univ∧A≠∅∧x∈⋂A→y∈⋂Ax→⋃ran⁡y∈⋂A
54 53 ralrimiv ⊢∀u∈Au∈Univ∧A≠∅∧x∈⋂A→∀y∈⋂Ax⋃ran⁡y∈⋂A
55 20 33 54 3jca ⊢∀u∈Au∈Univ∧A≠∅∧x∈⋂A→𝒫x∈⋂A∧∀y∈⋂Axy∈⋂A∧∀y∈⋂Ax⋃ran⁡y∈⋂A
56 55 ralrimiva ⊢∀u∈Au∈Univ∧A≠∅→∀x∈⋂A𝒫x∈⋂A∧∀y∈⋂Axy∈⋂A∧∀y∈⋂Ax⋃ran⁡y∈⋂A
57 4 56 sylanb ⊢A⊆Univ∧A≠∅→∀x∈⋂A𝒫x∈⋂A∧∀y∈⋂Axy∈⋂A∧∀y∈⋂Ax⋃ran⁡y∈⋂A
58 elgrug ⊢⋂A∈V→⋂A∈Univ↔Tr⁡⋂A∧∀x∈⋂A𝒫x∈⋂A∧∀y∈⋂Axy∈⋂A∧∀y∈⋂Ax⋃ran⁡y∈⋂A
59 58 biimpar ⊢⋂A∈V∧Tr⁡⋂A∧∀x∈⋂A𝒫x∈⋂A∧∀y∈⋂Axy∈⋂A∧∀y∈⋂Ax⋃ran⁡y∈⋂A→⋂A∈Univ
60 3 10 57 59 syl12anc ⊢A⊆Univ∧A≠∅→⋂A∈Univ