Step |
Hyp |
Ref |
Expression |
1 |
|
dffi2 |
|- ( F e. ( fBas ` X ) -> ( fi ` F ) = |^| { z | ( F C_ z /\ A. u e. z A. v e. z ( u i^i v ) e. z ) } ) |
2 |
|
sseq2 |
|- ( t = ( u i^i v ) -> ( x C_ t <-> x C_ ( u i^i v ) ) ) |
3 |
2
|
rexbidv |
|- ( t = ( u i^i v ) -> ( E. x e. F x C_ t <-> E. x e. F x C_ ( u i^i v ) ) ) |
4 |
|
inss1 |
|- ( u i^i v ) C_ u |
5 |
|
simp1r |
|- ( ( ( F e. ( fBas ` X ) /\ u e. ~P U. F ) /\ ( y e. F /\ y C_ u ) /\ ( z e. F /\ z C_ v ) ) -> u e. ~P U. F ) |
6 |
5
|
elpwid |
|- ( ( ( F e. ( fBas ` X ) /\ u e. ~P U. F ) /\ ( y e. F /\ y C_ u ) /\ ( z e. F /\ z C_ v ) ) -> u C_ U. F ) |
7 |
4 6
|
sstrid |
|- ( ( ( F e. ( fBas ` X ) /\ u e. ~P U. F ) /\ ( y e. F /\ y C_ u ) /\ ( z e. F /\ z C_ v ) ) -> ( u i^i v ) C_ U. F ) |
8 |
|
vex |
|- u e. _V |
9 |
8
|
inex1 |
|- ( u i^i v ) e. _V |
10 |
9
|
elpw |
|- ( ( u i^i v ) e. ~P U. F <-> ( u i^i v ) C_ U. F ) |
11 |
7 10
|
sylibr |
|- ( ( ( F e. ( fBas ` X ) /\ u e. ~P U. F ) /\ ( y e. F /\ y C_ u ) /\ ( z e. F /\ z C_ v ) ) -> ( u i^i v ) e. ~P U. F ) |
12 |
|
simpl |
|- ( ( F e. ( fBas ` X ) /\ u e. ~P U. F ) -> F e. ( fBas ` X ) ) |
13 |
|
simpl |
|- ( ( y e. F /\ y C_ u ) -> y e. F ) |
14 |
|
simpl |
|- ( ( z e. F /\ z C_ v ) -> z e. F ) |
15 |
|
fbasssin |
|- ( ( F e. ( fBas ` X ) /\ y e. F /\ z e. F ) -> E. x e. F x C_ ( y i^i z ) ) |
16 |
12 13 14 15
|
syl3an |
|- ( ( ( F e. ( fBas ` X ) /\ u e. ~P U. F ) /\ ( y e. F /\ y C_ u ) /\ ( z e. F /\ z C_ v ) ) -> E. x e. F x C_ ( y i^i z ) ) |
17 |
|
ss2in |
|- ( ( y C_ u /\ z C_ v ) -> ( y i^i z ) C_ ( u i^i v ) ) |
18 |
17
|
ad2ant2l |
|- ( ( ( y e. F /\ y C_ u ) /\ ( z e. F /\ z C_ v ) ) -> ( y i^i z ) C_ ( u i^i v ) ) |
19 |
18
|
3adant1 |
|- ( ( ( F e. ( fBas ` X ) /\ u e. ~P U. F ) /\ ( y e. F /\ y C_ u ) /\ ( z e. F /\ z C_ v ) ) -> ( y i^i z ) C_ ( u i^i v ) ) |
20 |
|
sstr |
|- ( ( x C_ ( y i^i z ) /\ ( y i^i z ) C_ ( u i^i v ) ) -> x C_ ( u i^i v ) ) |
21 |
20
|
expcom |
|- ( ( y i^i z ) C_ ( u i^i v ) -> ( x C_ ( y i^i z ) -> x C_ ( u i^i v ) ) ) |
22 |
19 21
|
syl |
|- ( ( ( F e. ( fBas ` X ) /\ u e. ~P U. F ) /\ ( y e. F /\ y C_ u ) /\ ( z e. F /\ z C_ v ) ) -> ( x C_ ( y i^i z ) -> x C_ ( u i^i v ) ) ) |
23 |
22
|
reximdv |
|- ( ( ( F e. ( fBas ` X ) /\ u e. ~P U. F ) /\ ( y e. F /\ y C_ u ) /\ ( z e. F /\ z C_ v ) ) -> ( E. x e. F x C_ ( y i^i z ) -> E. x e. F x C_ ( u i^i v ) ) ) |
24 |
16 23
|
mpd |
|- ( ( ( F e. ( fBas ` X ) /\ u e. ~P U. F ) /\ ( y e. F /\ y C_ u ) /\ ( z e. F /\ z C_ v ) ) -> E. x e. F x C_ ( u i^i v ) ) |
25 |
3 11 24
|
elrabd |
|- ( ( ( F e. ( fBas ` X ) /\ u e. ~P U. F ) /\ ( y e. F /\ y C_ u ) /\ ( z e. F /\ z C_ v ) ) -> ( u i^i v ) e. { t e. ~P U. F | E. x e. F x C_ t } ) |
26 |
25
|
3expa |
|- ( ( ( ( F e. ( fBas ` X ) /\ u e. ~P U. F ) /\ ( y e. F /\ y C_ u ) ) /\ ( z e. F /\ z C_ v ) ) -> ( u i^i v ) e. { t e. ~P U. F | E. x e. F x C_ t } ) |
27 |
26
|
rexlimdvaa |
|- ( ( ( F e. ( fBas ` X ) /\ u e. ~P U. F ) /\ ( y e. F /\ y C_ u ) ) -> ( E. z e. F z C_ v -> ( u i^i v ) e. { t e. ~P U. F | E. x e. F x C_ t } ) ) |
28 |
27
|
ralrimivw |
|- ( ( ( F e. ( fBas ` X ) /\ u e. ~P U. F ) /\ ( y e. F /\ y C_ u ) ) -> A. v e. ~P U. F ( E. z e. F z C_ v -> ( u i^i v ) e. { t e. ~P U. F | E. x e. F x C_ t } ) ) |
29 |
|
sseq2 |
|- ( t = v -> ( x C_ t <-> x C_ v ) ) |
30 |
29
|
rexbidv |
|- ( t = v -> ( E. x e. F x C_ t <-> E. x e. F x C_ v ) ) |
31 |
|
sseq1 |
|- ( x = z -> ( x C_ v <-> z C_ v ) ) |
32 |
31
|
cbvrexvw |
|- ( E. x e. F x C_ v <-> E. z e. F z C_ v ) |
33 |
30 32
|
bitrdi |
|- ( t = v -> ( E. x e. F x C_ t <-> E. z e. F z C_ v ) ) |
34 |
33
|
ralrab |
|- ( A. v e. { t e. ~P U. F | E. x e. F x C_ t } ( u i^i v ) e. { t e. ~P U. F | E. x e. F x C_ t } <-> A. v e. ~P U. F ( E. z e. F z C_ v -> ( u i^i v ) e. { t e. ~P U. F | E. x e. F x C_ t } ) ) |
35 |
28 34
|
sylibr |
|- ( ( ( F e. ( fBas ` X ) /\ u e. ~P U. F ) /\ ( y e. F /\ y C_ u ) ) -> A. v e. { t e. ~P U. F | E. x e. F x C_ t } ( u i^i v ) e. { t e. ~P U. F | E. x e. F x C_ t } ) |
36 |
35
|
rexlimdvaa |
|- ( ( F e. ( fBas ` X ) /\ u e. ~P U. F ) -> ( E. y e. F y C_ u -> A. v e. { t e. ~P U. F | E. x e. F x C_ t } ( u i^i v ) e. { t e. ~P U. F | E. x e. F x C_ t } ) ) |
37 |
36
|
ralrimiva |
|- ( F e. ( fBas ` X ) -> A. u e. ~P U. F ( E. y e. F y C_ u -> A. v e. { t e. ~P U. F | E. x e. F x C_ t } ( u i^i v ) e. { t e. ~P U. F | E. x e. F x C_ t } ) ) |
38 |
|
sseq2 |
|- ( t = u -> ( x C_ t <-> x C_ u ) ) |
39 |
38
|
rexbidv |
|- ( t = u -> ( E. x e. F x C_ t <-> E. x e. F x C_ u ) ) |
40 |
|
sseq1 |
|- ( x = y -> ( x C_ u <-> y C_ u ) ) |
41 |
40
|
cbvrexvw |
|- ( E. x e. F x C_ u <-> E. y e. F y C_ u ) |
42 |
39 41
|
bitrdi |
|- ( t = u -> ( E. x e. F x C_ t <-> E. y e. F y C_ u ) ) |
43 |
42
|
ralrab |
|- ( A. u e. { t e. ~P U. F | E. x e. F x C_ t } A. v e. { t e. ~P U. F | E. x e. F x C_ t } ( u i^i v ) e. { t e. ~P U. F | E. x e. F x C_ t } <-> A. u e. ~P U. F ( E. y e. F y C_ u -> A. v e. { t e. ~P U. F | E. x e. F x C_ t } ( u i^i v ) e. { t e. ~P U. F | E. x e. F x C_ t } ) ) |
44 |
37 43
|
sylibr |
|- ( F e. ( fBas ` X ) -> A. u e. { t e. ~P U. F | E. x e. F x C_ t } A. v e. { t e. ~P U. F | E. x e. F x C_ t } ( u i^i v ) e. { t e. ~P U. F | E. x e. F x C_ t } ) |
45 |
|
pwuni |
|- F C_ ~P U. F |
46 |
|
ssid |
|- t C_ t |
47 |
|
sseq1 |
|- ( x = t -> ( x C_ t <-> t C_ t ) ) |
48 |
47
|
rspcev |
|- ( ( t e. F /\ t C_ t ) -> E. x e. F x C_ t ) |
49 |
46 48
|
mpan2 |
|- ( t e. F -> E. x e. F x C_ t ) |
50 |
49
|
rgen |
|- A. t e. F E. x e. F x C_ t |
51 |
|
ssrab |
|- ( F C_ { t e. ~P U. F | E. x e. F x C_ t } <-> ( F C_ ~P U. F /\ A. t e. F E. x e. F x C_ t ) ) |
52 |
45 50 51
|
mpbir2an |
|- F C_ { t e. ~P U. F | E. x e. F x C_ t } |
53 |
44 52
|
jctil |
|- ( F e. ( fBas ` X ) -> ( F C_ { t e. ~P U. F | E. x e. F x C_ t } /\ A. u e. { t e. ~P U. F | E. x e. F x C_ t } A. v e. { t e. ~P U. F | E. x e. F x C_ t } ( u i^i v ) e. { t e. ~P U. F | E. x e. F x C_ t } ) ) |
54 |
|
uniexg |
|- ( F e. ( fBas ` X ) -> U. F e. _V ) |
55 |
|
pwexg |
|- ( U. F e. _V -> ~P U. F e. _V ) |
56 |
|
rabexg |
|- ( ~P U. F e. _V -> { t e. ~P U. F | E. x e. F x C_ t } e. _V ) |
57 |
|
sseq2 |
|- ( z = { t e. ~P U. F | E. x e. F x C_ t } -> ( F C_ z <-> F C_ { t e. ~P U. F | E. x e. F x C_ t } ) ) |
58 |
|
eleq2 |
|- ( z = { t e. ~P U. F | E. x e. F x C_ t } -> ( ( u i^i v ) e. z <-> ( u i^i v ) e. { t e. ~P U. F | E. x e. F x C_ t } ) ) |
59 |
58
|
raleqbi1dv |
|- ( z = { t e. ~P U. F | E. x e. F x C_ t } -> ( A. v e. z ( u i^i v ) e. z <-> A. v e. { t e. ~P U. F | E. x e. F x C_ t } ( u i^i v ) e. { t e. ~P U. F | E. x e. F x C_ t } ) ) |
60 |
59
|
raleqbi1dv |
|- ( z = { t e. ~P U. F | E. x e. F x C_ t } -> ( A. u e. z A. v e. z ( u i^i v ) e. z <-> A. u e. { t e. ~P U. F | E. x e. F x C_ t } A. v e. { t e. ~P U. F | E. x e. F x C_ t } ( u i^i v ) e. { t e. ~P U. F | E. x e. F x C_ t } ) ) |
61 |
57 60
|
anbi12d |
|- ( z = { t e. ~P U. F | E. x e. F x C_ t } -> ( ( F C_ z /\ A. u e. z A. v e. z ( u i^i v ) e. z ) <-> ( F C_ { t e. ~P U. F | E. x e. F x C_ t } /\ A. u e. { t e. ~P U. F | E. x e. F x C_ t } A. v e. { t e. ~P U. F | E. x e. F x C_ t } ( u i^i v ) e. { t e. ~P U. F | E. x e. F x C_ t } ) ) ) |
62 |
61
|
elabg |
|- ( { t e. ~P U. F | E. x e. F x C_ t } e. _V -> ( { t e. ~P U. F | E. x e. F x C_ t } e. { z | ( F C_ z /\ A. u e. z A. v e. z ( u i^i v ) e. z ) } <-> ( F C_ { t e. ~P U. F | E. x e. F x C_ t } /\ A. u e. { t e. ~P U. F | E. x e. F x C_ t } A. v e. { t e. ~P U. F | E. x e. F x C_ t } ( u i^i v ) e. { t e. ~P U. F | E. x e. F x C_ t } ) ) ) |
63 |
54 55 56 62
|
4syl |
|- ( F e. ( fBas ` X ) -> ( { t e. ~P U. F | E. x e. F x C_ t } e. { z | ( F C_ z /\ A. u e. z A. v e. z ( u i^i v ) e. z ) } <-> ( F C_ { t e. ~P U. F | E. x e. F x C_ t } /\ A. u e. { t e. ~P U. F | E. x e. F x C_ t } A. v e. { t e. ~P U. F | E. x e. F x C_ t } ( u i^i v ) e. { t e. ~P U. F | E. x e. F x C_ t } ) ) ) |
64 |
53 63
|
mpbird |
|- ( F e. ( fBas ` X ) -> { t e. ~P U. F | E. x e. F x C_ t } e. { z | ( F C_ z /\ A. u e. z A. v e. z ( u i^i v ) e. z ) } ) |
65 |
|
intss1 |
|- ( { t e. ~P U. F | E. x e. F x C_ t } e. { z | ( F C_ z /\ A. u e. z A. v e. z ( u i^i v ) e. z ) } -> |^| { z | ( F C_ z /\ A. u e. z A. v e. z ( u i^i v ) e. z ) } C_ { t e. ~P U. F | E. x e. F x C_ t } ) |
66 |
64 65
|
syl |
|- ( F e. ( fBas ` X ) -> |^| { z | ( F C_ z /\ A. u e. z A. v e. z ( u i^i v ) e. z ) } C_ { t e. ~P U. F | E. x e. F x C_ t } ) |
67 |
1 66
|
eqsstrd |
|- ( F e. ( fBas ` X ) -> ( fi ` F ) C_ { t e. ~P U. F | E. x e. F x C_ t } ) |
68 |
67
|
sselda |
|- ( ( F e. ( fBas ` X ) /\ A e. ( fi ` F ) ) -> A e. { t e. ~P U. F | E. x e. F x C_ t } ) |
69 |
|
sseq2 |
|- ( t = A -> ( x C_ t <-> x C_ A ) ) |
70 |
69
|
rexbidv |
|- ( t = A -> ( E. x e. F x C_ t <-> E. x e. F x C_ A ) ) |
71 |
70
|
elrab |
|- ( A e. { t e. ~P U. F | E. x e. F x C_ t } <-> ( A e. ~P U. F /\ E. x e. F x C_ A ) ) |
72 |
71
|
simprbi |
|- ( A e. { t e. ~P U. F | E. x e. F x C_ t } -> E. x e. F x C_ A ) |
73 |
68 72
|
syl |
|- ( ( F e. ( fBas ` X ) /\ A e. ( fi ` F ) ) -> E. x e. F x C_ A ) |