Step |
Hyp |
Ref |
Expression |
1 |
|
intss1 |
|- ( u e. Y -> |^| Y C_ u ) |
2 |
1
|
3ad2ant2 |
|- ( ( [C.] Or Y /\ u e. Y /\ A. v e. Y -. v C. u ) -> |^| Y C_ u ) |
3 |
|
sorpssi |
|- ( ( [C.] Or Y /\ ( u e. Y /\ v e. Y ) ) -> ( u C_ v \/ v C_ u ) ) |
4 |
3
|
anassrs |
|- ( ( ( [C.] Or Y /\ u e. Y ) /\ v e. Y ) -> ( u C_ v \/ v C_ u ) ) |
5 |
|
sspss |
|- ( v C_ u <-> ( v C. u \/ v = u ) ) |
6 |
|
orel1 |
|- ( -. v C. u -> ( ( v C. u \/ v = u ) -> v = u ) ) |
7 |
|
eqimss2 |
|- ( v = u -> u C_ v ) |
8 |
6 7
|
syl6com |
|- ( ( v C. u \/ v = u ) -> ( -. v C. u -> u C_ v ) ) |
9 |
5 8
|
sylbi |
|- ( v C_ u -> ( -. v C. u -> u C_ v ) ) |
10 |
9
|
jao1i |
|- ( ( u C_ v \/ v C_ u ) -> ( -. v C. u -> u C_ v ) ) |
11 |
4 10
|
syl |
|- ( ( ( [C.] Or Y /\ u e. Y ) /\ v e. Y ) -> ( -. v C. u -> u C_ v ) ) |
12 |
11
|
ralimdva |
|- ( ( [C.] Or Y /\ u e. Y ) -> ( A. v e. Y -. v C. u -> A. v e. Y u C_ v ) ) |
13 |
12
|
3impia |
|- ( ( [C.] Or Y /\ u e. Y /\ A. v e. Y -. v C. u ) -> A. v e. Y u C_ v ) |
14 |
|
ssint |
|- ( u C_ |^| Y <-> A. v e. Y u C_ v ) |
15 |
13 14
|
sylibr |
|- ( ( [C.] Or Y /\ u e. Y /\ A. v e. Y -. v C. u ) -> u C_ |^| Y ) |
16 |
2 15
|
eqssd |
|- ( ( [C.] Or Y /\ u e. Y /\ A. v e. Y -. v C. u ) -> |^| Y = u ) |
17 |
|
simp2 |
|- ( ( [C.] Or Y /\ u e. Y /\ A. v e. Y -. v C. u ) -> u e. Y ) |
18 |
16 17
|
eqeltrd |
|- ( ( [C.] Or Y /\ u e. Y /\ A. v e. Y -. v C. u ) -> |^| Y e. Y ) |
19 |
18
|
rexlimdv3a |
|- ( [C.] Or Y -> ( E. u e. Y A. v e. Y -. v C. u -> |^| Y e. Y ) ) |
20 |
|
intss1 |
|- ( v e. Y -> |^| Y C_ v ) |
21 |
|
ssnpss |
|- ( |^| Y C_ v -> -. v C. |^| Y ) |
22 |
20 21
|
syl |
|- ( v e. Y -> -. v C. |^| Y ) |
23 |
22
|
rgen |
|- A. v e. Y -. v C. |^| Y |
24 |
|
psseq2 |
|- ( u = |^| Y -> ( v C. u <-> v C. |^| Y ) ) |
25 |
24
|
notbid |
|- ( u = |^| Y -> ( -. v C. u <-> -. v C. |^| Y ) ) |
26 |
25
|
ralbidv |
|- ( u = |^| Y -> ( A. v e. Y -. v C. u <-> A. v e. Y -. v C. |^| Y ) ) |
27 |
26
|
rspcev |
|- ( ( |^| Y e. Y /\ A. v e. Y -. v C. |^| Y ) -> E. u e. Y A. v e. Y -. v C. u ) |
28 |
23 27
|
mpan2 |
|- ( |^| Y e. Y -> E. u e. Y A. v e. Y -. v C. u ) |
29 |
19 28
|
impbid1 |
|- ( [C.] Or Y -> ( E. u e. Y A. v e. Y -. v C. u <-> |^| Y e. Y ) ) |