Step |
Hyp |
Ref |
Expression |
1 |
|
ltrelnq |
|- |
2 |
|
relxp |
|- Rel ( Q. X. Q. ) |
3 |
|
relss |
|- ( ( Rel ( Q. X. Q. ) -> Rel |
4 |
1 2 3
|
mp2 |
|- Rel |
5 |
4
|
brrelex1i |
|- ( C C e. _V ) |
6 |
|
eleq1 |
|- ( x = B -> ( x e. A <-> B e. A ) ) |
7 |
6
|
anbi2d |
|- ( x = B -> ( ( A e. P. /\ x e. A ) <-> ( A e. P. /\ B e. A ) ) ) |
8 |
|
breq2 |
|- ( x = B -> ( y y |
9 |
7 8
|
anbi12d |
|- ( x = B -> ( ( ( A e. P. /\ x e. A ) /\ y ( ( A e. P. /\ B e. A ) /\ y |
10 |
9
|
imbi1d |
|- ( x = B -> ( ( ( ( A e. P. /\ x e. A ) /\ y y e. A ) <-> ( ( ( A e. P. /\ B e. A ) /\ y y e. A ) ) ) |
11 |
|
breq1 |
|- ( y = C -> ( y C |
12 |
11
|
anbi2d |
|- ( y = C -> ( ( ( A e. P. /\ B e. A ) /\ y ( ( A e. P. /\ B e. A ) /\ C |
13 |
|
eleq1 |
|- ( y = C -> ( y e. A <-> C e. A ) ) |
14 |
12 13
|
imbi12d |
|- ( y = C -> ( ( ( ( A e. P. /\ B e. A ) /\ y y e. A ) <-> ( ( ( A e. P. /\ B e. A ) /\ C C e. A ) ) ) |
15 |
|
elnpi |
|- ( A e. P. <-> ( ( A e. _V /\ (/) C. A /\ A C. Q. ) /\ A. x e. A ( A. y ( y y e. A ) /\ E. y e. A x |
16 |
15
|
simprbi |
|- ( A e. P. -> A. x e. A ( A. y ( y y e. A ) /\ E. y e. A x |
17 |
16
|
r19.21bi |
|- ( ( A e. P. /\ x e. A ) -> ( A. y ( y y e. A ) /\ E. y e. A x |
18 |
17
|
simpld |
|- ( ( A e. P. /\ x e. A ) -> A. y ( y y e. A ) ) |
19 |
18
|
19.21bi |
|- ( ( A e. P. /\ x e. A ) -> ( y y e. A ) ) |
20 |
19
|
imp |
|- ( ( ( A e. P. /\ x e. A ) /\ y y e. A ) |
21 |
10 14 20
|
vtocl2g |
|- ( ( B e. A /\ C e. _V ) -> ( ( ( A e. P. /\ B e. A ) /\ C C e. A ) ) |
22 |
5 21
|
sylan2 |
|- ( ( B e. A /\ C ( ( ( A e. P. /\ B e. A ) /\ C C e. A ) ) |
23 |
22
|
adantll |
|- ( ( ( A e. P. /\ B e. A ) /\ C ( ( ( A e. P. /\ B e. A ) /\ C C e. A ) ) |
24 |
23
|
pm2.43i |
|- ( ( ( A e. P. /\ B e. A ) /\ C C e. A ) |
25 |
24
|
ex |
|- ( ( A e. P. /\ B e. A ) -> ( C C e. A ) ) |