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 syl6ibr
 |-  ( ( 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 )