Step |
Hyp |
Ref |
Expression |
1 |
|
df-rex |
|- ( E. g e. 1P x = ( f .Q g ) <-> E. g ( g e. 1P /\ x = ( f .Q g ) ) ) |
2 |
|
elprnq |
|- ( ( A e. P. /\ f e. A ) -> f e. Q. ) |
3 |
|
breq1 |
|- ( x = ( f .Q g ) -> ( x ( f .Q g ) |
4 |
|
df-1p |
|- 1P = { g | g |
5 |
4
|
abeq2i |
|- ( g e. 1P <-> g |
6 |
|
ltmnq |
|- ( f e. Q. -> ( g ( f .Q g ) |
7 |
|
mulidnq |
|- ( f e. Q. -> ( f .Q 1Q ) = f ) |
8 |
7
|
breq2d |
|- ( f e. Q. -> ( ( f .Q g ) ( f .Q g ) |
9 |
6 8
|
bitrd |
|- ( f e. Q. -> ( g ( f .Q g ) |
10 |
5 9
|
bitr2id |
|- ( f e. Q. -> ( ( f .Q g ) g e. 1P ) ) |
11 |
3 10
|
sylan9bbr |
|- ( ( f e. Q. /\ x = ( f .Q g ) ) -> ( x g e. 1P ) ) |
12 |
2 11
|
sylan |
|- ( ( ( A e. P. /\ f e. A ) /\ x = ( f .Q g ) ) -> ( x g e. 1P ) ) |
13 |
12
|
ex |
|- ( ( A e. P. /\ f e. A ) -> ( x = ( f .Q g ) -> ( x g e. 1P ) ) ) |
14 |
13
|
pm5.32rd |
|- ( ( A e. P. /\ f e. A ) -> ( ( x ( g e. 1P /\ x = ( f .Q g ) ) ) ) |
15 |
14
|
exbidv |
|- ( ( A e. P. /\ f e. A ) -> ( E. g ( x E. g ( g e. 1P /\ x = ( f .Q g ) ) ) ) |
16 |
|
19.42v |
|- ( E. g ( x ( x |
17 |
15 16
|
bitr3di |
|- ( ( A e. P. /\ f e. A ) -> ( E. g ( g e. 1P /\ x = ( f .Q g ) ) <-> ( x |
18 |
1 17
|
syl5bb |
|- ( ( A e. P. /\ f e. A ) -> ( E. g e. 1P x = ( f .Q g ) <-> ( x |
19 |
18
|
rexbidva |
|- ( A e. P. -> ( E. f e. A E. g e. 1P x = ( f .Q g ) <-> E. f e. A ( x |
20 |
|
1pr |
|- 1P e. P. |
21 |
|
df-mp |
|- .P. = ( y e. P. , z e. P. |-> { w | E. u e. y E. v e. z w = ( u .Q v ) } ) |
22 |
|
mulclnq |
|- ( ( u e. Q. /\ v e. Q. ) -> ( u .Q v ) e. Q. ) |
23 |
21 22
|
genpelv |
|- ( ( A e. P. /\ 1P e. P. ) -> ( x e. ( A .P. 1P ) <-> E. f e. A E. g e. 1P x = ( f .Q g ) ) ) |
24 |
20 23
|
mpan2 |
|- ( A e. P. -> ( x e. ( A .P. 1P ) <-> E. f e. A E. g e. 1P x = ( f .Q g ) ) ) |
25 |
|
prnmax |
|- ( ( A e. P. /\ x e. A ) -> E. f e. A x |
26 |
|
ltrelnq |
|- |
27 |
26
|
brel |
|- ( x ( x e. Q. /\ f e. Q. ) ) |
28 |
|
vex |
|- f e. _V |
29 |
|
vex |
|- x e. _V |
30 |
|
fvex |
|- ( *Q ` f ) e. _V |
31 |
|
mulcomnq |
|- ( y .Q z ) = ( z .Q y ) |
32 |
|
mulassnq |
|- ( ( y .Q z ) .Q w ) = ( y .Q ( z .Q w ) ) |
33 |
28 29 30 31 32
|
caov12 |
|- ( f .Q ( x .Q ( *Q ` f ) ) ) = ( x .Q ( f .Q ( *Q ` f ) ) ) |
34 |
|
recidnq |
|- ( f e. Q. -> ( f .Q ( *Q ` f ) ) = 1Q ) |
35 |
34
|
oveq2d |
|- ( f e. Q. -> ( x .Q ( f .Q ( *Q ` f ) ) ) = ( x .Q 1Q ) ) |
36 |
33 35
|
eqtrid |
|- ( f e. Q. -> ( f .Q ( x .Q ( *Q ` f ) ) ) = ( x .Q 1Q ) ) |
37 |
|
mulidnq |
|- ( x e. Q. -> ( x .Q 1Q ) = x ) |
38 |
36 37
|
sylan9eqr |
|- ( ( x e. Q. /\ f e. Q. ) -> ( f .Q ( x .Q ( *Q ` f ) ) ) = x ) |
39 |
38
|
eqcomd |
|- ( ( x e. Q. /\ f e. Q. ) -> x = ( f .Q ( x .Q ( *Q ` f ) ) ) ) |
40 |
|
ovex |
|- ( x .Q ( *Q ` f ) ) e. _V |
41 |
|
oveq2 |
|- ( g = ( x .Q ( *Q ` f ) ) -> ( f .Q g ) = ( f .Q ( x .Q ( *Q ` f ) ) ) ) |
42 |
41
|
eqeq2d |
|- ( g = ( x .Q ( *Q ` f ) ) -> ( x = ( f .Q g ) <-> x = ( f .Q ( x .Q ( *Q ` f ) ) ) ) ) |
43 |
40 42
|
spcev |
|- ( x = ( f .Q ( x .Q ( *Q ` f ) ) ) -> E. g x = ( f .Q g ) ) |
44 |
27 39 43
|
3syl |
|- ( x E. g x = ( f .Q g ) ) |
45 |
44
|
a1i |
|- ( f e. A -> ( x E. g x = ( f .Q g ) ) ) |
46 |
45
|
ancld |
|- ( f e. A -> ( x ( x |
47 |
46
|
reximia |
|- ( E. f e. A x E. f e. A ( x |
48 |
25 47
|
syl |
|- ( ( A e. P. /\ x e. A ) -> E. f e. A ( x |
49 |
48
|
ex |
|- ( A e. P. -> ( x e. A -> E. f e. A ( x |
50 |
|
prcdnq |
|- ( ( A e. P. /\ f e. A ) -> ( x x e. A ) ) |
51 |
50
|
adantrd |
|- ( ( A e. P. /\ f e. A ) -> ( ( x x e. A ) ) |
52 |
51
|
rexlimdva |
|- ( A e. P. -> ( E. f e. A ( x x e. A ) ) |
53 |
49 52
|
impbid |
|- ( A e. P. -> ( x e. A <-> E. f e. A ( x |
54 |
19 24 53
|
3bitr4d |
|- ( A e. P. -> ( x e. ( A .P. 1P ) <-> x e. A ) ) |
55 |
54
|
eqrdv |
|- ( A e. P. -> ( A .P. 1P ) = A ) |