Metamath Proof Explorer

Theorem intgru

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

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

Proof

Step Hyp Ref Expression
1 intex 
 |-  ( A =/= (/) <-> |^| A e. _V )
2 1 bilani 
 |-  ( ( A C_ Univ /\ A =/= (/) ) -> |^| A e. _V )
3 dfss3 
 |-  ( A C_ Univ <-> A. u e. A u e. Univ )
4 grutr 
 |-  ( u e. Univ -> Tr u )
5 4 ralimi 
 |-  ( A. u e. A u e. Univ -> A. u e. A Tr u )
6 3 5 sylbi 
 |-  ( A C_ Univ -> A. u e. A Tr u )
7 trint 
 |-  ( A. u e. A Tr u -> Tr |^| A )
8 6 7 syl 
 |-  ( A C_ Univ -> Tr |^| A )
9 8 adantr 
 |-  ( ( A C_ Univ /\ A =/= (/) ) -> Tr |^| A )
10 grupw 
 |-  ( ( u e. Univ /\ x e. u ) -> ~P x e. u )
11 10 ex 
 |-  ( u e. Univ -> ( x e. u -> ~P x e. u ) )
12 11 ral2imi 
 |-  ( A. u e. A u e. Univ -> ( A. u e. A x e. u -> A. u e. A ~P x e. u ) )
13 vex 
 |-  x e. _V
14 13 elint2 
 |-  ( x e. |^| A <-> A. u e. A x e. u )
15 vpwex 
 |-  ~P x e. _V
16 15 elint2 
 |-  ( ~P x e. |^| A <-> A. u e. A ~P x e. u )
17 12 14 16 3imtr4g 
 |-  ( A. u e. A u e. Univ -> ( x e. |^| A -> ~P x e. |^| A ) )
18 17 imp 
 |-  ( ( A. u e. A u e. Univ /\ x e. |^| A ) -> ~P x e. |^| A )
19 18 adantlr 
 |-  ( ( ( A. u e. A u e. Univ /\ A =/= (/) ) /\ x e. |^| A ) -> ~P x e. |^| A )
20 r19.26 
 |-  ( A. u e. A ( u e. Univ /\ x e. u ) <-> ( A. u e. A u e. Univ /\ A. u e. A x e. u ) )
21 grupr 
 |-  ( ( u e. Univ /\ x e. u /\ y e. u ) -> { x , y } e. u )
22 21 3expia 
 |-  ( ( u e. Univ /\ x e. u ) -> ( y e. u -> { x , y } e. u ) )
23 22 ral2imi 
 |-  ( 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 ) )
24 20 23 sylbir 
 |-  ( ( 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 ) )
25 vex 
 |-  y e. _V
26 25 elint2 
 |-  ( y e. |^| A <-> A. u e. A y e. u )
27 prex 
 |-  { x , y } e. _V
28 27 elint2 
 |-  ( { x , y } e. |^| A <-> A. u e. A { x , y } e. u )
29 24 26 28 3imtr4g 
 |-  ( ( A. u e. A u e. Univ /\ A. u e. A x e. u ) -> ( y e. |^| A -> { x , y } e. |^| A ) )
30 14 29 sylan2b 
 |-  ( ( A. u e. A u e. Univ /\ x e. |^| A ) -> ( y e. |^| A -> { x , y } e. |^| A ) )
31 30 ralrimiv 
 |-  ( ( A. u e. A u e. Univ /\ x e. |^| A ) -> A. y e. |^| A { x , y } e. |^| A )
32 31 adantlr 
 |-  ( ( ( A. u e. A u e. Univ /\ A =/= (/) ) /\ x e. |^| A ) -> A. y e. |^| A { x , y } e. |^| A )
33 elmapg 
 |-  ( ( |^| A e. _V /\ x e. _V ) -> ( y e. ( |^| A ^m x ) <-> y : x --> |^| A ) )
34 33 elvd 
 |-  ( |^| A e. _V -> ( y e. ( |^| A ^m x ) <-> y : x --> |^| A ) )
35 1 34 sylbi 
 |-  ( A =/= (/) -> ( y e. ( |^| A ^m x ) <-> y : x --> |^| A ) )
36 35 ad2antlr 
 |-  ( ( ( A. u e. A u e. Univ /\ A =/= (/) ) /\ x e. |^| A ) -> ( y e. ( |^| A ^m x ) <-> y : x --> |^| A ) )
37 intss1 
 |-  ( u e. A -> |^| A C_ u )
38 fss 
 |-  ( ( y : x --> |^| A /\ |^| A C_ u ) -> y : x --> u )
39 37 38 sylan2 
 |-  ( ( y : x --> |^| A /\ u e. A ) -> y : x --> u )
40 39 ralrimiva 
 |-  ( y : x --> |^| A -> A. u e. A y : x --> u )
41 gruurn 
 |-  ( ( u e. Univ /\ x e. u /\ y : x --> u ) -> U. ran y e. u )
42 41 3expia 
 |-  ( ( u e. Univ /\ x e. u ) -> ( y : x --> u -> U. ran y e. u ) )
43 42 ral2imi 
 |-  ( 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 ) )
44 20 43 sylbir 
 |-  ( ( 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 ) )
45 14 44 sylan2b 
 |-  ( ( 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 ) )
46 40 45 syl5 
 |-  ( ( A. u e. A u e. Univ /\ x e. |^| A ) -> ( y : x --> |^| A -> A. u e. A U. ran y e. u ) )
47 25 rnex 
 |-  ran y e. _V
48 47 uniex 
 |-  U. ran y e. _V
49 48 elint2 
 |-  ( U. ran y e. |^| A <-> A. u e. A U. ran y e. u )
50 46 49 imbitrrdi 
 |-  ( ( A. u e. A u e. Univ /\ x e. |^| A ) -> ( y : x --> |^| A -> U. ran y e. |^| A ) )
51 50 adantlr 
 |-  ( ( ( A. u e. A u e. Univ /\ A =/= (/) ) /\ x e. |^| A ) -> ( y : x --> |^| A -> U. ran y e. |^| A ) )
52 36 51 sylbid 
 |-  ( ( ( A. u e. A u e. Univ /\ A =/= (/) ) /\ x e. |^| A ) -> ( y e. ( |^| A ^m x ) -> U. ran y e. |^| A ) )
53 52 ralrimiv 
 |-  ( ( ( A. u e. A u e. Univ /\ A =/= (/) ) /\ x e. |^| A ) -> A. y e. ( |^| A ^m x ) U. ran y e. |^| A )
54 19 32 53 3jca 
 |-  ( ( ( 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 ) )
55 54 ralrimiva 
 |-  ( ( 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 ) )
56 3 55 sylanb 
 |-  ( ( 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 ) )
57 elgrug 
 |-  ( |^| 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 ) ) ) )
58 57 biimpar 
 |-  ( ( |^| 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 )
59 2 9 56 58 syl12anc 
 |-  ( ( A C_ Univ /\ A =/= (/) ) -> |^| A e. Univ )