Step |
Hyp |
Ref |
Expression |
1 |
|
prtlem18.1 |
|- .~ = { <. x , y >. | E. u e. A ( x e. u /\ y e. u ) } |
2 |
1
|
relopabiv |
|- Rel .~ |
3 |
2
|
a1i |
|- ( Prt A -> Rel .~ ) |
4 |
1
|
prtlem16 |
|- dom .~ = U. A |
5 |
4
|
a1i |
|- ( Prt A -> dom .~ = U. A ) |
6 |
|
prtlem15 |
|- ( Prt A -> ( E. v e. A E. q e. A ( ( z e. v /\ w e. v ) /\ ( w e. q /\ p e. q ) ) -> E. r e. A ( z e. r /\ p e. r ) ) ) |
7 |
1
|
prtlem13 |
|- ( z .~ w <-> E. v e. A ( z e. v /\ w e. v ) ) |
8 |
1
|
prtlem13 |
|- ( w .~ p <-> E. q e. A ( w e. q /\ p e. q ) ) |
9 |
7 8
|
anbi12i |
|- ( ( z .~ w /\ w .~ p ) <-> ( E. v e. A ( z e. v /\ w e. v ) /\ E. q e. A ( w e. q /\ p e. q ) ) ) |
10 |
|
reeanv |
|- ( E. v e. A E. q e. A ( ( z e. v /\ w e. v ) /\ ( w e. q /\ p e. q ) ) <-> ( E. v e. A ( z e. v /\ w e. v ) /\ E. q e. A ( w e. q /\ p e. q ) ) ) |
11 |
9 10
|
bitr4i |
|- ( ( z .~ w /\ w .~ p ) <-> E. v e. A E. q e. A ( ( z e. v /\ w e. v ) /\ ( w e. q /\ p e. q ) ) ) |
12 |
1
|
prtlem13 |
|- ( z .~ p <-> E. r e. A ( z e. r /\ p e. r ) ) |
13 |
6 11 12
|
3imtr4g |
|- ( Prt A -> ( ( z .~ w /\ w .~ p ) -> z .~ p ) ) |
14 |
|
pm3.22 |
|- ( ( z e. v /\ w e. v ) -> ( w e. v /\ z e. v ) ) |
15 |
14
|
reximi |
|- ( E. v e. A ( z e. v /\ w e. v ) -> E. v e. A ( w e. v /\ z e. v ) ) |
16 |
1
|
prtlem13 |
|- ( w .~ z <-> E. v e. A ( w e. v /\ z e. v ) ) |
17 |
15 7 16
|
3imtr4i |
|- ( z .~ w -> w .~ z ) |
18 |
13 17
|
jctil |
|- ( Prt A -> ( ( z .~ w -> w .~ z ) /\ ( ( z .~ w /\ w .~ p ) -> z .~ p ) ) ) |
19 |
18
|
alrimivv |
|- ( Prt A -> A. w A. p ( ( z .~ w -> w .~ z ) /\ ( ( z .~ w /\ w .~ p ) -> z .~ p ) ) ) |
20 |
19
|
alrimiv |
|- ( Prt A -> A. z A. w A. p ( ( z .~ w -> w .~ z ) /\ ( ( z .~ w /\ w .~ p ) -> z .~ p ) ) ) |
21 |
|
dfer2 |
|- ( .~ Er U. A <-> ( Rel .~ /\ dom .~ = U. A /\ A. z A. w A. p ( ( z .~ w -> w .~ z ) /\ ( ( z .~ w /\ w .~ p ) -> z .~ p ) ) ) ) |
22 |
3 5 20 21
|
syl3anbrc |
|- ( Prt A -> .~ Er U. A ) |