This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 
|- ( ( A C_ WUni /\ A =/= (/) ) -> |^| A e. WUni )

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( A C_ WUni /\ A =/= (/) ) -> A C_ WUni )
2 1 sselda 
 |-  ( ( ( A C_ WUni /\ A =/= (/) ) /\ u e. A ) -> u e. WUni )
3 wuntr 
 |-  ( u e. WUni -> Tr u )
4 2 3 syl 
 |-  ( ( ( A C_ WUni /\ A =/= (/) ) /\ u e. A ) -> Tr u )
5 4 ralrimiva 
 |-  ( ( A C_ WUni /\ A =/= (/) ) -> A. u e. A Tr u )
6 trint 
 |-  ( A. u e. A Tr u -> Tr |^| A )
7 5 6 syl 
 |-  ( ( A C_ WUni /\ A =/= (/) ) -> Tr |^| A )
8 2 wun0 
 |-  ( ( ( A C_ WUni /\ A =/= (/) ) /\ u e. A ) -> (/) e. u )
9 8 ralrimiva 
 |-  ( ( A C_ WUni /\ A =/= (/) ) -> A. u e. A (/) e. u )
10 0ex 
 |-  (/) e. _V
11 10 elint2 
 |-  ( (/) e. |^| A <-> A. u e. A (/) e. u )
12 9 11 sylibr 
 |-  ( ( A C_ WUni /\ A =/= (/) ) -> (/) e. |^| A )
13 12 ne0d 
 |-  ( ( A C_ WUni /\ A =/= (/) ) -> |^| A =/= (/) )
14 2 adantlr 
 |-  ( ( ( ( A C_ WUni /\ A =/= (/) ) /\ x e. |^| A ) /\ u e. A ) -> u e. WUni )
15 intss1 
 |-  ( u e. A -> |^| A C_ u )
16 15 adantl 
 |-  ( ( ( A C_ WUni /\ A =/= (/) ) /\ u e. A ) -> |^| A C_ u )
17 16 sselda 
 |-  ( ( ( ( A C_ WUni /\ A =/= (/) ) /\ u e. A ) /\ x e. |^| A ) -> x e. u )
18 17 an32s 
 |-  ( ( ( ( A C_ WUni /\ A =/= (/) ) /\ x e. |^| A ) /\ u e. A ) -> x e. u )
19 14 18 wununi 
 |-  ( ( ( ( A C_ WUni /\ A =/= (/) ) /\ x e. |^| A ) /\ u e. A ) -> U. x e. u )
20 19 ralrimiva 
 |-  ( ( ( A C_ WUni /\ A =/= (/) ) /\ x e. |^| A ) -> A. u e. A U. x e. u )
21 vuniex 
 |-  U. x e. _V
22 21 elint2 
 |-  ( U. x e. |^| A <-> A. u e. A U. x e. u )
23 20 22 sylibr 
 |-  ( ( ( A C_ WUni /\ A =/= (/) ) /\ x e. |^| A ) -> U. x e. |^| A )
24 14 18 wunpw 
 |-  ( ( ( ( A C_ WUni /\ A =/= (/) ) /\ x e. |^| A ) /\ u e. A ) -> ~P x e. u )
25 24 ralrimiva 
 |-  ( ( ( A C_ WUni /\ A =/= (/) ) /\ x e. |^| A ) -> A. u e. A ~P x e. u )
26 vpwex 
 |-  ~P x e. _V
27 26 elint2 
 |-  ( ~P x e. |^| A <-> A. u e. A ~P x e. u )
28 25 27 sylibr 
 |-  ( ( ( A C_ WUni /\ A =/= (/) ) /\ x e. |^| A ) -> ~P x e. |^| A )
29 14 adantlr 
 |-  ( ( ( ( ( A C_ WUni /\ A =/= (/) ) /\ x e. |^| A ) /\ y e. |^| A ) /\ u e. A ) -> u e. WUni )
30 18 adantlr 
 |-  ( ( ( ( ( A C_ WUni /\ A =/= (/) ) /\ x e. |^| A ) /\ y e. |^| A ) /\ u e. A ) -> x e. u )
31 15 adantl 
 |-  ( ( ( ( A C_ WUni /\ A =/= (/) ) /\ x e. |^| A ) /\ u e. A ) -> |^| A C_ u )
32 31 sselda 
 |-  ( ( ( ( ( A C_ WUni /\ A =/= (/) ) /\ x e. |^| A ) /\ u e. A ) /\ y e. |^| A ) -> y e. u )
33 32 an32s 
 |-  ( ( ( ( ( A C_ WUni /\ A =/= (/) ) /\ x e. |^| A ) /\ y e. |^| A ) /\ u e. A ) -> y e. u )
34 29 30 33 wunpr 
 |-  ( ( ( ( ( A C_ WUni /\ A =/= (/) ) /\ x e. |^| A ) /\ y e. |^| A ) /\ u e. A ) -> { x , y } e. u )
35 34 ralrimiva 
 |-  ( ( ( ( A C_ WUni /\ A =/= (/) ) /\ x e. |^| A ) /\ y e. |^| A ) -> A. u e. A { x , y } e. u )
36 prex 
 |-  { x , y } e. _V
37 36 elint2 
 |-  ( { x , y } e. |^| A <-> A. u e. A { x , y } e. u )
38 35 37 sylibr 
 |-  ( ( ( ( A C_ WUni /\ A =/= (/) ) /\ x e. |^| A ) /\ y e. |^| A ) -> { x , y } e. |^| A )
39 38 ralrimiva 
 |-  ( ( ( A C_ WUni /\ A =/= (/) ) /\ x e. |^| A ) -> A. y e. |^| A { x , y } e. |^| A )
40 23 28 39 3jca 
 |-  ( ( ( A C_ WUni /\ A =/= (/) ) /\ x e. |^| A ) -> ( U. x e. |^| A /\ ~P x e. |^| A /\ A. y e. |^| A { x , y } e. |^| A ) )
41 40 ralrimiva 
 |-  ( ( A C_ WUni /\ A =/= (/) ) -> A. x e. |^| A ( U. x e. |^| A /\ ~P x e. |^| A /\ A. y e. |^| A { x , y } e. |^| A ) )
42 simpr 
 |-  ( ( A C_ WUni /\ A =/= (/) ) -> A =/= (/) )
43 intex 
 |-  ( A =/= (/) <-> |^| A e. _V )
44 42 43 sylib 
 |-  ( ( A C_ WUni /\ A =/= (/) ) -> |^| A e. _V )
45 iswun 
 |-  ( |^| A e. _V -> ( |^| A e. WUni <-> ( Tr |^| A /\ |^| A =/= (/) /\ A. x e. |^| A ( U. x e. |^| A /\ ~P x e. |^| A /\ A. y e. |^| A { x , y } e. |^| A ) ) ) )
46 44 45 syl 
 |-  ( ( A C_ WUni /\ A =/= (/) ) -> ( |^| A e. WUni <-> ( Tr |^| A /\ |^| A =/= (/) /\ A. x e. |^| A ( U. x e. |^| A /\ ~P x e. |^| A /\ A. y e. |^| A { x , y } e. |^| A ) ) ) )
47 7 13 41 46 mpbir3and 
 |-  ( ( A C_ WUni /\ A =/= (/) ) -> |^| A e. WUni )