Step |
Hyp |
Ref |
Expression |
1 |
|
pclfin.a |
|- A = ( Atoms ` K ) |
2 |
|
pclfin.c |
|- U = ( PCl ` K ) |
3 |
1 2
|
pclfinN |
|- ( ( K e. AtLat /\ X C_ A ) -> ( U ` X ) = U_ y e. ( Fin i^i ~P X ) ( U ` y ) ) |
4 |
3
|
eleq2d |
|- ( ( K e. AtLat /\ X C_ A ) -> ( P e. ( U ` X ) <-> P e. U_ y e. ( Fin i^i ~P X ) ( U ` y ) ) ) |
5 |
|
eliun |
|- ( P e. U_ y e. ( Fin i^i ~P X ) ( U ` y ) <-> E. y e. ( Fin i^i ~P X ) P e. ( U ` y ) ) |
6 |
4 5
|
bitrdi |
|- ( ( K e. AtLat /\ X C_ A ) -> ( P e. ( U ` X ) <-> E. y e. ( Fin i^i ~P X ) P e. ( U ` y ) ) ) |
7 |
|
elin |
|- ( y e. ( Fin i^i ~P X ) <-> ( y e. Fin /\ y e. ~P X ) ) |
8 |
|
elpwi |
|- ( y e. ~P X -> y C_ X ) |
9 |
8
|
anim2i |
|- ( ( y e. Fin /\ y e. ~P X ) -> ( y e. Fin /\ y C_ X ) ) |
10 |
7 9
|
sylbi |
|- ( y e. ( Fin i^i ~P X ) -> ( y e. Fin /\ y C_ X ) ) |
11 |
10
|
anim1i |
|- ( ( y e. ( Fin i^i ~P X ) /\ P e. ( U ` y ) ) -> ( ( y e. Fin /\ y C_ X ) /\ P e. ( U ` y ) ) ) |
12 |
|
anass |
|- ( ( ( y e. Fin /\ y C_ X ) /\ P e. ( U ` y ) ) <-> ( y e. Fin /\ ( y C_ X /\ P e. ( U ` y ) ) ) ) |
13 |
11 12
|
sylib |
|- ( ( y e. ( Fin i^i ~P X ) /\ P e. ( U ` y ) ) -> ( y e. Fin /\ ( y C_ X /\ P e. ( U ` y ) ) ) ) |
14 |
13
|
reximi2 |
|- ( E. y e. ( Fin i^i ~P X ) P e. ( U ` y ) -> E. y e. Fin ( y C_ X /\ P e. ( U ` y ) ) ) |
15 |
6 14
|
syl6bi |
|- ( ( K e. AtLat /\ X C_ A ) -> ( P e. ( U ` X ) -> E. y e. Fin ( y C_ X /\ P e. ( U ` y ) ) ) ) |
16 |
15
|
3impia |
|- ( ( K e. AtLat /\ X C_ A /\ P e. ( U ` X ) ) -> E. y e. Fin ( y C_ X /\ P e. ( U ` y ) ) ) |