Theorem intgru 9636

Description: The intersection of a family of universes is a universe. (Contributed by Mario Carneiro, 9-Jun-2013.)

Assertion

Ref	Expression
intgru	|- ( ( A C_ Univ /\ A =/= (/) ) -> |^| A e. Univ )

Proof of Theorem intgru

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

Step	Hyp	Ref	Expression
1		simpr 477	. . 3 |- ( ( A C_ Univ /\ A =/= (/) ) -> A =/= (/) )
2		intex 4820	. . 3 |- ( A =/= (/) <-> |^| A e. _V )
3	1, 2	sylib 208	. 2 |- ( ( A C_ Univ /\ A =/= (/) ) -> |^| A e. _V )
4		dfss3 3592	. . . . 5 |- ( A C_ Univ <-> A. u e. A u e. Univ )
5		grutr 9615	. . . . . 6 |- ( u e. Univ -> Tr u )
6	5	ralimi 2952	. . . . 5 |- ( A. u e. A u e. Univ -> A. u e. A Tr u )
7	4, 6	sylbi 207	. . . 4 |- ( A C_ Univ -> A. u e. A Tr u )
8		trint 4768	. . . 4 |- ( A. u e. A Tr u -> Tr |^| A )
9	7, 8	syl 17	. . 3 |- ( A C_ Univ -> Tr |^| A )
10	9	adantr 481	. 2 |- ( ( A C_ Univ /\ A =/= (/) ) -> Tr |^| A )
11		grupw 9617	. . . . . . . . . 10 |- ( ( u e. Univ /\ x e. u ) -> ~P x e. u )
12	11	ex 450	. . . . . . . . 9 |- ( u e. Univ -> ( x e. u -> ~P x e. u ) )
13	12	ral2imi 2947	. . . . . . . 8 |- ( A. u e. A u e. Univ -> ( A. u e. A x e. u -> A. u e. A ~P x e. u ) )
14		vex 3203	. . . . . . . . 9 |- x e. _V
15	14	elint2 4482	. . . . . . . 8 |- ( x e. |^| A <-> A. u e. A x e. u )
16		vpwex 4849	. . . . . . . . 9 |- ~P x e. _V
17	16	elint2 4482	. . . . . . . 8 |- ( ~P x e. |^| A <-> A. u e. A ~P x e. u )
18	13, 15, 17	3imtr4g 285	. . . . . . 7 |- ( A. u e. A u e. Univ -> ( x e. |^| A -> ~P x e. |^| A ) )
19	18	imp 445	. . . . . 6 |- ( ( A. u e. A u e. Univ /\ x e. |^| A ) -> ~P x e. |^| A )
20	19	adantlr 751	. . . . 5 |- ( ( ( A. u e. A u e. Univ /\ A =/= (/) ) /\ x e. |^| A ) -> ~P x e. |^| A )
21		r19.26 3064	. . . . . . . . . 10 |- ( A. u e. A ( u e. Univ /\ x e. u ) <-> ( A. u e. A u e. Univ /\ A. u e. A x e. u ) )
22		grupr 9619	. . . . . . . . . . . 12 |- ( ( u e. Univ /\ x e. u /\ y e. u ) -> { x , y } e. u )
23	22	3expia 1267	. . . . . . . . . . 11 |- ( ( u e. Univ /\ x e. u ) -> ( y e. u -> { x , y } e. u ) )
24	23	ral2imi 2947	. . . . . . . . . 10 |- ( A. u e. A ( u e. Univ /\ x e. u ) -> ( A. u e. A y e. u -> A. u e. A { x , y } e. u ) )
25	21, 24	sylbir 225	. . . . . . . . 9 |- ( ( A. u e. A u e. Univ /\ A. u e. A x e. u ) -> ( A. u e. A y e. u -> A. u e. A { x , y } e. u ) )
26		vex 3203	. . . . . . . . . 10 |- y e. _V
27	26	elint2 4482	. . . . . . . . 9 |- ( y e. |^| A <-> A. u e. A y e. u )
28		prex 4909	. . . . . . . . . 10 |- { x , y } e. _V
29	28	elint2 4482	. . . . . . . . 9 |- ( { x , y } e. |^| A <-> A. u e. A { x , y } e. u )
30	25, 27, 29	3imtr4g 285	. . . . . . . 8 |- ( ( A. u e. A u e. Univ /\ A. u e. A x e. u ) -> ( y e. |^| A -> { x , y } e. |^| A ) )
31	15, 30	sylan2b 492	. . . . . . 7 |- ( ( A. u e. A u e. Univ /\ x e. |^| A ) -> ( y e. |^| A -> { x , y } e. |^| A ) )
32	31	ralrimiv 2965	. . . . . 6 |- ( ( A. u e. A u e. Univ /\ x e. |^| A ) -> A. y e. |^| A { x , y } e. |^| A )
33	32	adantlr 751	. . . . 5 |- ( ( ( A. u e. A u e. Univ /\ A =/= (/) ) /\ x e. |^| A ) -> A. y e. |^| A { x , y } e. |^| A )
34		elmapg 7870	. . . . . . . . . 10 |- ( ( |^| A e. _V /\ x e. _V ) -> ( y e. ( |^| A ^m x ) <-> y : x --> |^| A ) )
35	14, 34	mpan2 707	. . . . . . . . 9 |- ( |^| A e. _V -> ( y e. ( |^| A ^m x ) <-> y : x --> |^| A ) )
36	2, 35	sylbi 207	. . . . . . . 8 |- ( A =/= (/) -> ( y e. ( |^| A ^m x ) <-> y : x --> |^| A ) )
37	36	ad2antlr 763	. . . . . . 7 |- ( ( ( A. u e. A u e. Univ /\ A =/= (/) ) /\ x e. |^| A ) -> ( y e. ( |^| A ^m x ) <-> y : x --> |^| A ) )
38		intss1 4492	. . . . . . . . . . . 12 |- ( u e. A -> |^| A C_ u )
39		fss 6056	. . . . . . . . . . . 12 |- ( ( y : x --> |^| A /\ |^| A C_ u ) -> y : x --> u )
40	38, 39	sylan2 491	. . . . . . . . . . 11 |- ( ( y : x --> |^| A /\ u e. A ) -> y : x --> u )
41	40	ralrimiva 2966	. . . . . . . . . 10 |- ( y : x --> |^| A -> A. u e. A y : x --> u )
42		gruurn 9620	. . . . . . . . . . . . . 14 |- ( ( u e. Univ /\ x e. u /\ y : x --> u ) -> U. ran y e. u )
43	42	3expia 1267	. . . . . . . . . . . . 13 |- ( ( u e. Univ /\ x e. u ) -> ( y : x --> u -> U. ran y e. u ) )
44	43	ral2imi 2947	. . . . . . . . . . . 12 |- ( A. u e. A ( u e. Univ /\ x e. u ) -> ( A. u e. A y : x --> u -> A. u e. A U. ran y e. u ) )
45	21, 44	sylbir 225	. . . . . . . . . . 11 |- ( ( A. u e. A u e. Univ /\ A. u e. A x e. u ) -> ( A. u e. A y : x --> u -> A. u e. A U. ran y e. u ) )
46	15, 45	sylan2b 492	. . . . . . . . . 10 |- ( ( A. u e. A u e. Univ /\ x e. |^| A ) -> ( A. u e. A y : x --> u -> A. u e. A U. ran y e. u ) )
47	41, 46	syl5 34	. . . . . . . . 9 |- ( ( A. u e. A u e. Univ /\ x e. |^| A ) -> ( y : x --> |^| A -> A. u e. A U. ran y e. u ) )
48	26	rnex 7100	. . . . . . . . . . 11 |- ran y e. _V
49	48	uniex 6953	. . . . . . . . . 10 |- U. ran y e. _V
50	49	elint2 4482	. . . . . . . . 9 |- ( U. ran y e. |^| A <-> A. u e. A U. ran y e. u )
51	47, 50	syl6ibr 242	. . . . . . . 8 |- ( ( A. u e. A u e. Univ /\ x e. |^| A ) -> ( y : x --> |^| A -> U. ran y e. |^| A ) )
52	51	adantlr 751	. . . . . . 7 |- ( ( ( A. u e. A u e. Univ /\ A =/= (/) ) /\ x e. |^| A ) -> ( y : x --> |^| A -> U. ran y e. |^| A ) )
53	37, 52	sylbid 230	. . . . . 6 |- ( ( ( A. u e. A u e. Univ /\ A =/= (/) ) /\ x e. |^| A ) -> ( y e. ( |^| A ^m x ) -> U. ran y e. |^| A ) )
54	53	ralrimiv 2965	. . . . 5 |- ( ( ( A. u e. A u e. Univ /\ A =/= (/) ) /\ x e. |^| A ) -> A. y e. ( |^| A ^m x ) U. ran y e. |^| A )
55	20, 33, 54	3jca 1242	. . . 4 |- ( ( ( A. u e. A u e. Univ /\ A =/= (/) ) /\ x e. |^| A ) -> ( ~P x e. |^| A /\ A. y e. |^| A { x , y } e. |^| A /\ A. y e. ( |^| A ^m x ) U. ran y e. |^| A ) )
56	55	ralrimiva 2966	. . 3 |- ( ( A. u e. A u e. Univ /\ A =/= (/) ) -> A. x e. |^| A ( ~P x e. |^| A /\ A. y e. |^| A { x , y } e. |^| A /\ A. y e. ( |^| A ^m x ) U. ran y e. |^| A ) )
57	4, 56	sylanb 489	. 2 |- ( ( A C_ Univ /\ A =/= (/) ) -> A. x e. |^| A ( ~P x e. |^| A /\ A. y e. |^| A { x , y } e. |^| A /\ A. y e. ( |^| A ^m x ) U. ran y e. |^| A ) )
58		elgrug 9614	. . 3 |- ( |^| A e. _V -> ( |^| A e. Univ <-> ( Tr |^| A /\ A. x e. |^| A ( ~P x e. |^| A /\ A. y e. |^| A { x , y } e. |^| A /\ A. y e. ( |^| A ^m x ) U. ran y e. |^| A ) ) ) )
59	58	biimpar 502	. 2 |- ( ( |^| A e. _V /\ ( Tr |^| A /\ A. x e. |^| A ( ~P x e. |^| A /\ A. y e. |^| A { x , y } e. |^| A /\ A. y e. ( |^| A ^m x ) U. ran y e. |^| A ) ) ) -> |^| A e. Univ )
60	3, 10, 57, 59	syl12anc 1324	1 |- ( ( A C_ Univ /\ A =/= (/) ) -> |^| A e. Univ )

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   ran crn 5115   -->wf 5884  (class class class)co 6650   ^m cmap 7857   Univcgru 9612

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-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-int 4476  df-br 4654  df-opab 4713  df-tr 4753  df-id 5024  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-fv 5896  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-map 7859  df-gru 9613

This theorem is referenced by: (None)