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