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