# Metamath Proof Explorer

## Theorem intwun

Description: The intersection of a collection of weak universes is a weak universe. (Contributed by Mario Carneiro, 2-Jan-2017)

Ref Expression
Assertion intwun ${⊢}\left({A}\subseteq \mathrm{WUni}\wedge {A}\ne \varnothing \right)\to \bigcap {A}\in \mathrm{WUni}$

### Proof

Step Hyp Ref Expression
1 simpl ${⊢}\left({A}\subseteq \mathrm{WUni}\wedge {A}\ne \varnothing \right)\to {A}\subseteq \mathrm{WUni}$
2 1 sselda ${⊢}\left(\left({A}\subseteq \mathrm{WUni}\wedge {A}\ne \varnothing \right)\wedge {u}\in {A}\right)\to {u}\in \mathrm{WUni}$
3 wuntr ${⊢}{u}\in \mathrm{WUni}\to \mathrm{Tr}{u}$
4 2 3 syl ${⊢}\left(\left({A}\subseteq \mathrm{WUni}\wedge {A}\ne \varnothing \right)\wedge {u}\in {A}\right)\to \mathrm{Tr}{u}$
5 4 ralrimiva ${⊢}\left({A}\subseteq \mathrm{WUni}\wedge {A}\ne \varnothing \right)\to \forall {u}\in {A}\phantom{\rule{.4em}{0ex}}\mathrm{Tr}{u}$
6 trint ${⊢}\forall {u}\in {A}\phantom{\rule{.4em}{0ex}}\mathrm{Tr}{u}\to \mathrm{Tr}\bigcap {A}$
7 5 6 syl ${⊢}\left({A}\subseteq \mathrm{WUni}\wedge {A}\ne \varnothing \right)\to \mathrm{Tr}\bigcap {A}$
8 2 wun0 ${⊢}\left(\left({A}\subseteq \mathrm{WUni}\wedge {A}\ne \varnothing \right)\wedge {u}\in {A}\right)\to \varnothing \in {u}$
9 8 ralrimiva ${⊢}\left({A}\subseteq \mathrm{WUni}\wedge {A}\ne \varnothing \right)\to \forall {u}\in {A}\phantom{\rule{.4em}{0ex}}\varnothing \in {u}$
10 0ex ${⊢}\varnothing \in \mathrm{V}$
11 10 elint2 ${⊢}\varnothing \in \bigcap {A}↔\forall {u}\in {A}\phantom{\rule{.4em}{0ex}}\varnothing \in {u}$
12 9 11 sylibr ${⊢}\left({A}\subseteq \mathrm{WUni}\wedge {A}\ne \varnothing \right)\to \varnothing \in \bigcap {A}$
13 12 ne0d ${⊢}\left({A}\subseteq \mathrm{WUni}\wedge {A}\ne \varnothing \right)\to \bigcap {A}\ne \varnothing$
14 2 adantlr ${⊢}\left(\left(\left({A}\subseteq \mathrm{WUni}\wedge {A}\ne \varnothing \right)\wedge {x}\in \bigcap {A}\right)\wedge {u}\in {A}\right)\to {u}\in \mathrm{WUni}$
15 intss1 ${⊢}{u}\in {A}\to \bigcap {A}\subseteq {u}$
16 15 adantl ${⊢}\left(\left({A}\subseteq \mathrm{WUni}\wedge {A}\ne \varnothing \right)\wedge {u}\in {A}\right)\to \bigcap {A}\subseteq {u}$
17 16 sselda ${⊢}\left(\left(\left({A}\subseteq \mathrm{WUni}\wedge {A}\ne \varnothing \right)\wedge {u}\in {A}\right)\wedge {x}\in \bigcap {A}\right)\to {x}\in {u}$
18 17 an32s ${⊢}\left(\left(\left({A}\subseteq \mathrm{WUni}\wedge {A}\ne \varnothing \right)\wedge {x}\in \bigcap {A}\right)\wedge {u}\in {A}\right)\to {x}\in {u}$
19 14 18 wununi ${⊢}\left(\left(\left({A}\subseteq \mathrm{WUni}\wedge {A}\ne \varnothing \right)\wedge {x}\in \bigcap {A}\right)\wedge {u}\in {A}\right)\to \bigcup {x}\in {u}$
20 19 ralrimiva ${⊢}\left(\left({A}\subseteq \mathrm{WUni}\wedge {A}\ne \varnothing \right)\wedge {x}\in \bigcap {A}\right)\to \forall {u}\in {A}\phantom{\rule{.4em}{0ex}}\bigcup {x}\in {u}$
21 vuniex ${⊢}\bigcup {x}\in \mathrm{V}$
22 21 elint2 ${⊢}\bigcup {x}\in \bigcap {A}↔\forall {u}\in {A}\phantom{\rule{.4em}{0ex}}\bigcup {x}\in {u}$
23 20 22 sylibr ${⊢}\left(\left({A}\subseteq \mathrm{WUni}\wedge {A}\ne \varnothing \right)\wedge {x}\in \bigcap {A}\right)\to \bigcup {x}\in \bigcap {A}$
24 14 18 wunpw ${⊢}\left(\left(\left({A}\subseteq \mathrm{WUni}\wedge {A}\ne \varnothing \right)\wedge {x}\in \bigcap {A}\right)\wedge {u}\in {A}\right)\to 𝒫{x}\in {u}$
25 24 ralrimiva ${⊢}\left(\left({A}\subseteq \mathrm{WUni}\wedge {A}\ne \varnothing \right)\wedge {x}\in \bigcap {A}\right)\to \forall {u}\in {A}\phantom{\rule{.4em}{0ex}}𝒫{x}\in {u}$
26 vpwex ${⊢}𝒫{x}\in \mathrm{V}$
27 26 elint2 ${⊢}𝒫{x}\in \bigcap {A}↔\forall {u}\in {A}\phantom{\rule{.4em}{0ex}}𝒫{x}\in {u}$
28 25 27 sylibr ${⊢}\left(\left({A}\subseteq \mathrm{WUni}\wedge {A}\ne \varnothing \right)\wedge {x}\in \bigcap {A}\right)\to 𝒫{x}\in \bigcap {A}$
29 14 adantlr ${⊢}\left(\left(\left(\left({A}\subseteq \mathrm{WUni}\wedge {A}\ne \varnothing \right)\wedge {x}\in \bigcap {A}\right)\wedge {y}\in \bigcap {A}\right)\wedge {u}\in {A}\right)\to {u}\in \mathrm{WUni}$
30 18 adantlr ${⊢}\left(\left(\left(\left({A}\subseteq \mathrm{WUni}\wedge {A}\ne \varnothing \right)\wedge {x}\in \bigcap {A}\right)\wedge {y}\in \bigcap {A}\right)\wedge {u}\in {A}\right)\to {x}\in {u}$
31 15 adantl ${⊢}\left(\left(\left({A}\subseteq \mathrm{WUni}\wedge {A}\ne \varnothing \right)\wedge {x}\in \bigcap {A}\right)\wedge {u}\in {A}\right)\to \bigcap {A}\subseteq {u}$
32 31 sselda ${⊢}\left(\left(\left(\left({A}\subseteq \mathrm{WUni}\wedge {A}\ne \varnothing \right)\wedge {x}\in \bigcap {A}\right)\wedge {u}\in {A}\right)\wedge {y}\in \bigcap {A}\right)\to {y}\in {u}$
33 32 an32s ${⊢}\left(\left(\left(\left({A}\subseteq \mathrm{WUni}\wedge {A}\ne \varnothing \right)\wedge {x}\in \bigcap {A}\right)\wedge {y}\in \bigcap {A}\right)\wedge {u}\in {A}\right)\to {y}\in {u}$
34 29 30 33 wunpr ${⊢}\left(\left(\left(\left({A}\subseteq \mathrm{WUni}\wedge {A}\ne \varnothing \right)\wedge {x}\in \bigcap {A}\right)\wedge {y}\in \bigcap {A}\right)\wedge {u}\in {A}\right)\to \left\{{x},{y}\right\}\in {u}$
35 34 ralrimiva ${⊢}\left(\left(\left({A}\subseteq \mathrm{WUni}\wedge {A}\ne \varnothing \right)\wedge {x}\in \bigcap {A}\right)\wedge {y}\in \bigcap {A}\right)\to \forall {u}\in {A}\phantom{\rule{.4em}{0ex}}\left\{{x},{y}\right\}\in {u}$
36 prex ${⊢}\left\{{x},{y}\right\}\in \mathrm{V}$
37 36 elint2 ${⊢}\left\{{x},{y}\right\}\in \bigcap {A}↔\forall {u}\in {A}\phantom{\rule{.4em}{0ex}}\left\{{x},{y}\right\}\in {u}$
38 35 37 sylibr ${⊢}\left(\left(\left({A}\subseteq \mathrm{WUni}\wedge {A}\ne \varnothing \right)\wedge {x}\in \bigcap {A}\right)\wedge {y}\in \bigcap {A}\right)\to \left\{{x},{y}\right\}\in \bigcap {A}$
39 38 ralrimiva ${⊢}\left(\left({A}\subseteq \mathrm{WUni}\wedge {A}\ne \varnothing \right)\wedge {x}\in \bigcap {A}\right)\to \forall {y}\in \bigcap {A}\phantom{\rule{.4em}{0ex}}\left\{{x},{y}\right\}\in \bigcap {A}$
40 23 28 39 3jca ${⊢}\left(\left({A}\subseteq \mathrm{WUni}\wedge {A}\ne \varnothing \right)\wedge {x}\in \bigcap {A}\right)\to \left(\bigcup {x}\in \bigcap {A}\wedge 𝒫{x}\in \bigcap {A}\wedge \forall {y}\in \bigcap {A}\phantom{\rule{.4em}{0ex}}\left\{{x},{y}\right\}\in \bigcap {A}\right)$
41 40 ralrimiva ${⊢}\left({A}\subseteq \mathrm{WUni}\wedge {A}\ne \varnothing \right)\to \forall {x}\in \bigcap {A}\phantom{\rule{.4em}{0ex}}\left(\bigcup {x}\in \bigcap {A}\wedge 𝒫{x}\in \bigcap {A}\wedge \forall {y}\in \bigcap {A}\phantom{\rule{.4em}{0ex}}\left\{{x},{y}\right\}\in \bigcap {A}\right)$
42 simpr ${⊢}\left({A}\subseteq \mathrm{WUni}\wedge {A}\ne \varnothing \right)\to {A}\ne \varnothing$
43 intex ${⊢}{A}\ne \varnothing ↔\bigcap {A}\in \mathrm{V}$
44 42 43 sylib ${⊢}\left({A}\subseteq \mathrm{WUni}\wedge {A}\ne \varnothing \right)\to \bigcap {A}\in \mathrm{V}$
45 iswun ${⊢}\bigcap {A}\in \mathrm{V}\to \left(\bigcap {A}\in \mathrm{WUni}↔\left(\mathrm{Tr}\bigcap {A}\wedge \bigcap {A}\ne \varnothing \wedge \forall {x}\in \bigcap {A}\phantom{\rule{.4em}{0ex}}\left(\bigcup {x}\in \bigcap {A}\wedge 𝒫{x}\in \bigcap {A}\wedge \forall {y}\in \bigcap {A}\phantom{\rule{.4em}{0ex}}\left\{{x},{y}\right\}\in \bigcap {A}\right)\right)\right)$
46 44 45 syl ${⊢}\left({A}\subseteq \mathrm{WUni}\wedge {A}\ne \varnothing \right)\to \left(\bigcap {A}\in \mathrm{WUni}↔\left(\mathrm{Tr}\bigcap {A}\wedge \bigcap {A}\ne \varnothing \wedge \forall {x}\in \bigcap {A}\phantom{\rule{.4em}{0ex}}\left(\bigcup {x}\in \bigcap {A}\wedge 𝒫{x}\in \bigcap {A}\wedge \forall {y}\in \bigcap {A}\phantom{\rule{.4em}{0ex}}\left\{{x},{y}\right\}\in \bigcap {A}\right)\right)\right)$
47 7 13 41 46 mpbir3and ${⊢}\left({A}\subseteq \mathrm{WUni}\wedge {A}\ne \varnothing \right)\to \bigcap {A}\in \mathrm{WUni}$