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 )