Step |
Hyp |
Ref |
Expression |
1 |
|
elin |
|- ( y e. ( ~P F i^i Fin ) <-> ( y e. ~P F /\ y e. Fin ) ) |
2 |
|
elpwi |
|- ( y e. ~P F -> y C_ F ) |
3 |
2
|
anim1i |
|- ( ( y e. ~P F /\ y e. Fin ) -> ( y C_ F /\ y e. Fin ) ) |
4 |
1 3
|
sylbi |
|- ( y e. ( ~P F i^i Fin ) -> ( y C_ F /\ y e. Fin ) ) |
5 |
|
fbssint |
|- ( ( F e. ( fBas ` X ) /\ y C_ F /\ y e. Fin ) -> E. z e. F z C_ |^| y ) |
6 |
5
|
3expb |
|- ( ( F e. ( fBas ` X ) /\ ( y C_ F /\ y e. Fin ) ) -> E. z e. F z C_ |^| y ) |
7 |
4 6
|
sylan2 |
|- ( ( F e. ( fBas ` X ) /\ y e. ( ~P F i^i Fin ) ) -> E. z e. F z C_ |^| y ) |
8 |
|
0nelfb |
|- ( F e. ( fBas ` X ) -> -. (/) e. F ) |
9 |
8
|
ad2antrr |
|- ( ( ( F e. ( fBas ` X ) /\ y e. ( ~P F i^i Fin ) ) /\ z e. F ) -> -. (/) e. F ) |
10 |
|
eleq1 |
|- ( z = (/) -> ( z e. F <-> (/) e. F ) ) |
11 |
10
|
biimpcd |
|- ( z e. F -> ( z = (/) -> (/) e. F ) ) |
12 |
11
|
adantl |
|- ( ( ( F e. ( fBas ` X ) /\ y e. ( ~P F i^i Fin ) ) /\ z e. F ) -> ( z = (/) -> (/) e. F ) ) |
13 |
9 12
|
mtod |
|- ( ( ( F e. ( fBas ` X ) /\ y e. ( ~P F i^i Fin ) ) /\ z e. F ) -> -. z = (/) ) |
14 |
|
ss0 |
|- ( z C_ (/) -> z = (/) ) |
15 |
13 14
|
nsyl |
|- ( ( ( F e. ( fBas ` X ) /\ y e. ( ~P F i^i Fin ) ) /\ z e. F ) -> -. z C_ (/) ) |
16 |
15
|
adantrr |
|- ( ( ( F e. ( fBas ` X ) /\ y e. ( ~P F i^i Fin ) ) /\ ( z e. F /\ z C_ |^| y ) ) -> -. z C_ (/) ) |
17 |
|
sseq2 |
|- ( (/) = |^| y -> ( z C_ (/) <-> z C_ |^| y ) ) |
18 |
17
|
biimprcd |
|- ( z C_ |^| y -> ( (/) = |^| y -> z C_ (/) ) ) |
19 |
18
|
ad2antll |
|- ( ( ( F e. ( fBas ` X ) /\ y e. ( ~P F i^i Fin ) ) /\ ( z e. F /\ z C_ |^| y ) ) -> ( (/) = |^| y -> z C_ (/) ) ) |
20 |
16 19
|
mtod |
|- ( ( ( F e. ( fBas ` X ) /\ y e. ( ~P F i^i Fin ) ) /\ ( z e. F /\ z C_ |^| y ) ) -> -. (/) = |^| y ) |
21 |
7 20
|
rexlimddv |
|- ( ( F e. ( fBas ` X ) /\ y e. ( ~P F i^i Fin ) ) -> -. (/) = |^| y ) |
22 |
21
|
nrexdv |
|- ( F e. ( fBas ` X ) -> -. E. y e. ( ~P F i^i Fin ) (/) = |^| y ) |
23 |
|
0ex |
|- (/) e. _V |
24 |
|
elfi |
|- ( ( (/) e. _V /\ F e. ( fBas ` X ) ) -> ( (/) e. ( fi ` F ) <-> E. y e. ( ~P F i^i Fin ) (/) = |^| y ) ) |
25 |
23 24
|
mpan |
|- ( F e. ( fBas ` X ) -> ( (/) e. ( fi ` F ) <-> E. y e. ( ~P F i^i Fin ) (/) = |^| y ) ) |
26 |
22 25
|
mtbird |
|- ( F e. ( fBas ` X ) -> -. (/) e. ( fi ` F ) ) |