| Step |
Hyp |
Ref |
Expression |
| 1 |
|
dmoprab |
|- dom { <. <. a , b >. , c >. | ( ( a e. ~P No /\ b e. ( <. | E. c ( ( a e. ~P No /\ b e. ( < |
| 2 |
|
df-scut |
|- |s = ( a e. ~P No , b e. ( < ( iota_ x e. { y e. No | ( a < |
| 3 |
|
df-mpo |
|- ( a e. ~P No , b e. ( < ( iota_ x e. { y e. No | ( a <. , c >. | ( ( a e. ~P No /\ b e. ( < |
| 4 |
2 3
|
eqtri |
|- |s = { <. <. a , b >. , c >. | ( ( a e. ~P No /\ b e. ( < |
| 5 |
4
|
dmeqi |
|- dom |s = dom { <. <. a , b >. , c >. | ( ( a e. ~P No /\ b e. ( < |
| 6 |
|
df-sslt |
|- <. | ( a C_ No /\ b C_ No /\ A. x e. a A. y e. b x |
| 7 |
6
|
relopabiv |
|- Rel < |
| 8 |
|
19.42v |
|- ( E. c ( ( a e. ~P No /\ b e. ( < ( ( a e. ~P No /\ b e. ( < |
| 9 |
|
ssltss1 |
|- ( a < a C_ No ) |
| 10 |
|
velpw |
|- ( a e. ~P No <-> a C_ No ) |
| 11 |
9 10
|
sylibr |
|- ( a < a e. ~P No ) |
| 12 |
11
|
pm4.71ri |
|- ( a < ( a e. ~P No /\ a < |
| 13 |
|
vex |
|- a e. _V |
| 14 |
|
vex |
|- b e. _V |
| 15 |
13 14
|
elimasn |
|- ( b e. ( < <. a , b >. e. < |
| 16 |
|
df-br |
|- ( a < <. a , b >. e. < |
| 17 |
15 16
|
bitr4i |
|- ( b e. ( < a < |
| 18 |
17
|
anbi2i |
|- ( ( a e. ~P No /\ b e. ( < ( a e. ~P No /\ a < |
| 19 |
|
riotaex |
|- ( iota_ x e. { y e. No | ( a < |
| 20 |
19
|
isseti |
|- E. c c = ( iota_ x e. { y e. No | ( a < |
| 21 |
20
|
biantru |
|- ( ( a e. ~P No /\ b e. ( < ( ( a e. ~P No /\ b e. ( < |
| 22 |
12 18 21
|
3bitr2i |
|- ( a < ( ( a e. ~P No /\ b e. ( < |
| 23 |
8 22 16
|
3bitr2ri |
|- ( <. a , b >. e. < E. c ( ( a e. ~P No /\ b e. ( < |
| 24 |
23
|
a1i |
|- ( T. -> ( <. a , b >. e. < E. c ( ( a e. ~P No /\ b e. ( < |
| 25 |
7 24
|
opabbi2dv |
|- ( T. -> <. | E. c ( ( a e. ~P No /\ b e. ( < |
| 26 |
25
|
mptru |
|- <. | E. c ( ( a e. ~P No /\ b e. ( < |
| 27 |
1 5 26
|
3eqtr4i |
|- dom |s = < |