Step |
Hyp |
Ref |
Expression |
1 |
|
opsrso.o |
|- O = ( ( I ordPwSer R ) ` T ) |
2 |
|
opsrso.i |
|- ( ph -> I e. V ) |
3 |
|
opsrso.r |
|- ( ph -> R e. Toset ) |
4 |
|
opsrso.t |
|- ( ph -> T C_ ( I X. I ) ) |
5 |
|
opsrso.w |
|- ( ph -> T We I ) |
6 |
|
opsrtoslem.s |
|- S = ( I mPwSer R ) |
7 |
|
opsrtoslem.b |
|- B = ( Base ` S ) |
8 |
|
opsrtoslem.q |
|- .< = ( lt ` R ) |
9 |
|
opsrtoslem.c |
|- C = ( T |
10 |
|
opsrtoslem.d |
|- D = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |
11 |
|
opsrtoslem.ps |
|- ( ps <-> E. z e. D ( ( x ` z ) .< ( y ` z ) /\ A. w e. D ( w C z -> ( x ` w ) = ( y ` w ) ) ) ) |
12 |
|
opsrtoslem.l |
|- .<_ = ( le ` O ) |
13 |
6 1 7 8 9 10 12 4
|
opsrle |
|- ( ph -> .<_ = { <. x , y >. | ( { x , y } C_ B /\ ( E. z e. D ( ( x ` z ) .< ( y ` z ) /\ A. w e. D ( w C z -> ( x ` w ) = ( y ` w ) ) ) \/ x = y ) ) } ) |
14 |
|
unopab |
|- ( { <. x , y >. | ( { x , y } C_ B /\ ps ) } u. { <. x , y >. | ( { x , y } C_ B /\ x = y ) } ) = { <. x , y >. | ( ( { x , y } C_ B /\ ps ) \/ ( { x , y } C_ B /\ x = y ) ) } |
15 |
|
inopab |
|- ( { <. x , y >. | ps } i^i { <. x , y >. | ( x e. B /\ y e. B ) } ) = { <. x , y >. | ( ps /\ ( x e. B /\ y e. B ) ) } |
16 |
|
df-xp |
|- ( B X. B ) = { <. x , y >. | ( x e. B /\ y e. B ) } |
17 |
16
|
ineq2i |
|- ( { <. x , y >. | ps } i^i ( B X. B ) ) = ( { <. x , y >. | ps } i^i { <. x , y >. | ( x e. B /\ y e. B ) } ) |
18 |
|
vex |
|- x e. _V |
19 |
|
vex |
|- y e. _V |
20 |
18 19
|
prss |
|- ( ( x e. B /\ y e. B ) <-> { x , y } C_ B ) |
21 |
20
|
anbi1i |
|- ( ( ( x e. B /\ y e. B ) /\ ps ) <-> ( { x , y } C_ B /\ ps ) ) |
22 |
|
ancom |
|- ( ( ( x e. B /\ y e. B ) /\ ps ) <-> ( ps /\ ( x e. B /\ y e. B ) ) ) |
23 |
21 22
|
bitr3i |
|- ( ( { x , y } C_ B /\ ps ) <-> ( ps /\ ( x e. B /\ y e. B ) ) ) |
24 |
23
|
opabbii |
|- { <. x , y >. | ( { x , y } C_ B /\ ps ) } = { <. x , y >. | ( ps /\ ( x e. B /\ y e. B ) ) } |
25 |
15 17 24
|
3eqtr4i |
|- ( { <. x , y >. | ps } i^i ( B X. B ) ) = { <. x , y >. | ( { x , y } C_ B /\ ps ) } |
26 |
|
opabresid |
|- ( _I |` B ) = { <. x , y >. | ( x e. B /\ y = x ) } |
27 |
|
equcom |
|- ( x = y <-> y = x ) |
28 |
27
|
anbi2i |
|- ( ( x e. B /\ x = y ) <-> ( x e. B /\ y = x ) ) |
29 |
|
eleq1w |
|- ( x = y -> ( x e. B <-> y e. B ) ) |
30 |
29
|
biimpac |
|- ( ( x e. B /\ x = y ) -> y e. B ) |
31 |
30
|
pm4.71i |
|- ( ( x e. B /\ x = y ) <-> ( ( x e. B /\ x = y ) /\ y e. B ) ) |
32 |
28 31
|
bitr3i |
|- ( ( x e. B /\ y = x ) <-> ( ( x e. B /\ x = y ) /\ y e. B ) ) |
33 |
|
an32 |
|- ( ( ( x e. B /\ x = y ) /\ y e. B ) <-> ( ( x e. B /\ y e. B ) /\ x = y ) ) |
34 |
20
|
anbi1i |
|- ( ( ( x e. B /\ y e. B ) /\ x = y ) <-> ( { x , y } C_ B /\ x = y ) ) |
35 |
32 33 34
|
3bitri |
|- ( ( x e. B /\ y = x ) <-> ( { x , y } C_ B /\ x = y ) ) |
36 |
35
|
opabbii |
|- { <. x , y >. | ( x e. B /\ y = x ) } = { <. x , y >. | ( { x , y } C_ B /\ x = y ) } |
37 |
26 36
|
eqtri |
|- ( _I |` B ) = { <. x , y >. | ( { x , y } C_ B /\ x = y ) } |
38 |
25 37
|
uneq12i |
|- ( ( { <. x , y >. | ps } i^i ( B X. B ) ) u. ( _I |` B ) ) = ( { <. x , y >. | ( { x , y } C_ B /\ ps ) } u. { <. x , y >. | ( { x , y } C_ B /\ x = y ) } ) |
39 |
11
|
orbi1i |
|- ( ( ps \/ x = y ) <-> ( E. z e. D ( ( x ` z ) .< ( y ` z ) /\ A. w e. D ( w C z -> ( x ` w ) = ( y ` w ) ) ) \/ x = y ) ) |
40 |
39
|
anbi2i |
|- ( ( { x , y } C_ B /\ ( ps \/ x = y ) ) <-> ( { x , y } C_ B /\ ( E. z e. D ( ( x ` z ) .< ( y ` z ) /\ A. w e. D ( w C z -> ( x ` w ) = ( y ` w ) ) ) \/ x = y ) ) ) |
41 |
|
andi |
|- ( ( { x , y } C_ B /\ ( ps \/ x = y ) ) <-> ( ( { x , y } C_ B /\ ps ) \/ ( { x , y } C_ B /\ x = y ) ) ) |
42 |
40 41
|
bitr3i |
|- ( ( { x , y } C_ B /\ ( E. z e. D ( ( x ` z ) .< ( y ` z ) /\ A. w e. D ( w C z -> ( x ` w ) = ( y ` w ) ) ) \/ x = y ) ) <-> ( ( { x , y } C_ B /\ ps ) \/ ( { x , y } C_ B /\ x = y ) ) ) |
43 |
42
|
opabbii |
|- { <. x , y >. | ( { x , y } C_ B /\ ( E. z e. D ( ( x ` z ) .< ( y ` z ) /\ A. w e. D ( w C z -> ( x ` w ) = ( y ` w ) ) ) \/ x = y ) ) } = { <. x , y >. | ( ( { x , y } C_ B /\ ps ) \/ ( { x , y } C_ B /\ x = y ) ) } |
44 |
14 38 43
|
3eqtr4ri |
|- { <. x , y >. | ( { x , y } C_ B /\ ( E. z e. D ( ( x ` z ) .< ( y ` z ) /\ A. w e. D ( w C z -> ( x ` w ) = ( y ` w ) ) ) \/ x = y ) ) } = ( ( { <. x , y >. | ps } i^i ( B X. B ) ) u. ( _I |` B ) ) |
45 |
13 44
|
eqtrdi |
|- ( ph -> .<_ = ( ( { <. x , y >. | ps } i^i ( B X. B ) ) u. ( _I |` B ) ) ) |