Theorem intwun 9557

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

Assertion

Ref	Expression
intwun	|- ( ( A C_ WUni /\ A =/= (/) ) -> |^| A e. WUni )

Proof of Theorem intwun

Dummy variables x u y are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		simpl 473	. . . . . 6 |- ( ( A C_ WUni /\ A =/= (/) ) -> A C_ WUni )
2	1	sselda 3603	. . . . 5 |- ( ( ( A C_ WUni /\ A =/= (/) ) /\ u e. A ) -> u e. WUni )
3		wuntr 9527	. . . . 5 |- ( u e. WUni -> Tr u )
4	2, 3	syl 17	. . . 4 |- ( ( ( A C_ WUni /\ A =/= (/) ) /\ u e. A ) -> Tr u )
5	4	ralrimiva 2966	. . 3 |- ( ( A C_ WUni /\ A =/= (/) ) -> A. u e. A Tr u )
6		trint 4768	. . 3 |- ( A. u e. A Tr u -> Tr |^| A )
7	5, 6	syl 17	. 2 |- ( ( A C_ WUni /\ A =/= (/) ) -> Tr |^| A )
8	2	wun0 9540	. . . . 5 |- ( ( ( A C_ WUni /\ A =/= (/) ) /\ u e. A ) -> (/) e. u )
9	8	ralrimiva 2966	. . . 4 |- ( ( A C_ WUni /\ A =/= (/) ) -> A. u e. A (/) e. u )
10		0ex 4790	. . . . 5 |- (/) e. _V
11	10	elint2 4482	. . . 4 |- ( (/) e. |^| A <-> A. u e. A (/) e. u )
12	9, 11	sylibr 224	. . 3 |- ( ( A C_ WUni /\ A =/= (/) ) -> (/) e. |^| A )
13		ne0i 3921	. . 3 |- ( (/) e. |^| A -> |^| A =/= (/) )
14	12, 13	syl 17	. 2 |- ( ( A C_ WUni /\ A =/= (/) ) -> |^| A =/= (/) )
15	2	adantlr 751	. . . . . . 7 |- ( ( ( ( A C_ WUni /\ A =/= (/) ) /\ x e. |^| A ) /\ u e. A ) -> u e. WUni )
16		intss1 4492	. . . . . . . . . 10 |- ( u e. A -> |^| A C_ u )
17	16	adantl 482	. . . . . . . . 9 |- ( ( ( A C_ WUni /\ A =/= (/) ) /\ u e. A ) -> |^| A C_ u )
18	17	sselda 3603	. . . . . . . 8 |- ( ( ( ( A C_ WUni /\ A =/= (/) ) /\ u e. A ) /\ x e. |^| A ) -> x e. u )
19	18	an32s 846	. . . . . . 7 |- ( ( ( ( A C_ WUni /\ A =/= (/) ) /\ x e. |^| A ) /\ u e. A ) -> x e. u )
20	15, 19	wununi 9528	. . . . . 6 |- ( ( ( ( A C_ WUni /\ A =/= (/) ) /\ x e. |^| A ) /\ u e. A ) -> U. x e. u )
21	20	ralrimiva 2966	. . . . 5 |- ( ( ( A C_ WUni /\ A =/= (/) ) /\ x e. |^| A ) -> A. u e. A U. x e. u )
22		vuniex 6954	. . . . . 6 |- U. x e. _V
23	22	elint2 4482	. . . . 5 |- ( U. x e. |^| A <-> A. u e. A U. x e. u )
24	21, 23	sylibr 224	. . . 4 |- ( ( ( A C_ WUni /\ A =/= (/) ) /\ x e. |^| A ) -> U. x e. |^| A )
25	15, 19	wunpw 9529	. . . . . 6 |- ( ( ( ( A C_ WUni /\ A =/= (/) ) /\ x e. |^| A ) /\ u e. A ) -> ~P x e. u )
26	25	ralrimiva 2966	. . . . 5 |- ( ( ( A C_ WUni /\ A =/= (/) ) /\ x e. |^| A ) -> A. u e. A ~P x e. u )
27		vpwex 4849	. . . . . 6 |- ~P x e. _V
28	27	elint2 4482	. . . . 5 |- ( ~P x e. |^| A <-> A. u e. A ~P x e. u )
29	26, 28	sylibr 224	. . . 4 |- ( ( ( A C_ WUni /\ A =/= (/) ) /\ x e. |^| A ) -> ~P x e. |^| A )
30	15	adantlr 751	. . . . . . . 8 |- ( ( ( ( ( A C_ WUni /\ A =/= (/) ) /\ x e. |^| A ) /\ y e. |^| A ) /\ u e. A ) -> u e. WUni )
31	19	adantlr 751	. . . . . . . 8 |- ( ( ( ( ( A C_ WUni /\ A =/= (/) ) /\ x e. |^| A ) /\ y e. |^| A ) /\ u e. A ) -> x e. u )
32	16	adantl 482	. . . . . . . . . 10 |- ( ( ( ( A C_ WUni /\ A =/= (/) ) /\ x e. |^| A ) /\ u e. A ) -> |^| A C_ u )
33	32	sselda 3603	. . . . . . . . 9 |- ( ( ( ( ( A C_ WUni /\ A =/= (/) ) /\ x e. |^| A ) /\ u e. A ) /\ y e. |^| A ) -> y e. u )
34	33	an32s 846	. . . . . . . 8 |- ( ( ( ( ( A C_ WUni /\ A =/= (/) ) /\ x e. |^| A ) /\ y e. |^| A ) /\ u e. A ) -> y e. u )
35	30, 31, 34	wunpr 9531	. . . . . . 7 |- ( ( ( ( ( A C_ WUni /\ A =/= (/) ) /\ x e. |^| A ) /\ y e. |^| A ) /\ u e. A ) -> { x , y } e. u )
36	35	ralrimiva 2966	. . . . . 6 |- ( ( ( ( A C_ WUni /\ A =/= (/) ) /\ x e. |^| A ) /\ y e. |^| A ) -> A. u e. A { x , y } e. u )
37		prex 4909	. . . . . . 7 |- { x , y } e. _V
38	37	elint2 4482	. . . . . 6 |- ( { x , y } e. |^| A <-> A. u e. A { x , y } e. u )
39	36, 38	sylibr 224	. . . . 5 |- ( ( ( ( A C_ WUni /\ A =/= (/) ) /\ x e. |^| A ) /\ y e. |^| A ) -> { x , y } e. |^| A )
40	39	ralrimiva 2966	. . . 4 |- ( ( ( A C_ WUni /\ A =/= (/) ) /\ x e. |^| A ) -> A. y e. |^| A { x , y } e. |^| A )
41	24, 29, 40	3jca 1242	. . 3 |- ( ( ( A C_ WUni /\ A =/= (/) ) /\ x e. |^| A ) -> ( U. x e. |^| A /\ ~P x e. |^| A /\ A. y e. |^| A { x , y } e. |^| A ) )
42	41	ralrimiva 2966	. 2 |- ( ( A C_ WUni /\ A =/= (/) ) -> A. x e. |^| A ( U. x e. |^| A /\ ~P x e. |^| A /\ A. y e. |^| A { x , y } e. |^| A ) )
43		simpr 477	. . . 4 |- ( ( A C_ WUni /\ A =/= (/) ) -> A =/= (/) )
44		intex 4820	. . . 4 |- ( A =/= (/) <-> |^| A e. _V )
45	43, 44	sylib 208	. . 3 |- ( ( A C_ WUni /\ A =/= (/) ) -> |^| A e. _V )
46		iswun 9526	. . 3 |- ( |^| 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 ) ) ) )
47	45, 46	syl 17	. 2 |- ( ( 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 ) ) ) )
48	7, 14, 42, 47	mpbir3and 1245	1 |- ( ( A C_ WUni /\ A =/= (/) ) -> |^| A e. WUni )

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384   /\ w3a 1037   e. wcel 1990   =/= wne 2794   A.wral 2912   _Vcvv 3200   C_ wss 3574   (/)c0 3915   ~Pcpw 4158   {cpr 4179   U.cuni 4436   |^|cint 4475   Tr wtr 4752  WUnicwun 9522

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-pw 4160  df-sn 4178  df-pr 4180  df-uni 4437  df-int 4476  df-tr 4753  df-wun 9524

This theorem is referenced by:  wunccl  9566