| Step |
Hyp |
Ref |
Expression |
| 1 |
|
df-xrn |
|- ( A |X. B ) = ( ( `' ( 1st |` ( _V X. _V ) ) o. A ) i^i ( `' ( 2nd |` ( _V X. _V ) ) o. B ) ) |
| 2 |
|
inss1 |
|- ( ( `' ( 1st |` ( _V X. _V ) ) o. A ) i^i ( `' ( 2nd |` ( _V X. _V ) ) o. B ) ) C_ ( `' ( 1st |` ( _V X. _V ) ) o. A ) |
| 3 |
|
relco |
|- Rel ( `' ( 1st |` ( _V X. _V ) ) o. A ) |
| 4 |
|
vex |
|- z e. _V |
| 5 |
|
vex |
|- y e. _V |
| 6 |
4 5
|
brcnv |
|- ( z `' ( 1st |` ( _V X. _V ) ) y <-> y ( 1st |` ( _V X. _V ) ) z ) |
| 7 |
4
|
brresi |
|- ( y ( 1st |` ( _V X. _V ) ) z <-> ( y e. ( _V X. _V ) /\ y 1st z ) ) |
| 8 |
7
|
simplbi |
|- ( y ( 1st |` ( _V X. _V ) ) z -> y e. ( _V X. _V ) ) |
| 9 |
6 8
|
sylbi |
|- ( z `' ( 1st |` ( _V X. _V ) ) y -> y e. ( _V X. _V ) ) |
| 10 |
9
|
adantl |
|- ( ( x A z /\ z `' ( 1st |` ( _V X. _V ) ) y ) -> y e. ( _V X. _V ) ) |
| 11 |
10
|
exlimiv |
|- ( E. z ( x A z /\ z `' ( 1st |` ( _V X. _V ) ) y ) -> y e. ( _V X. _V ) ) |
| 12 |
|
vex |
|- x e. _V |
| 13 |
12 5
|
opelco |
|- ( <. x , y >. e. ( `' ( 1st |` ( _V X. _V ) ) o. A ) <-> E. z ( x A z /\ z `' ( 1st |` ( _V X. _V ) ) y ) ) |
| 14 |
|
opelxp |
|- ( <. x , y >. e. ( _V X. ( _V X. _V ) ) <-> ( x e. _V /\ y e. ( _V X. _V ) ) ) |
| 15 |
12 14
|
mpbiran |
|- ( <. x , y >. e. ( _V X. ( _V X. _V ) ) <-> y e. ( _V X. _V ) ) |
| 16 |
11 13 15
|
3imtr4i |
|- ( <. x , y >. e. ( `' ( 1st |` ( _V X. _V ) ) o. A ) -> <. x , y >. e. ( _V X. ( _V X. _V ) ) ) |
| 17 |
3 16
|
relssi |
|- ( `' ( 1st |` ( _V X. _V ) ) o. A ) C_ ( _V X. ( _V X. _V ) ) |
| 18 |
2 17
|
sstri |
|- ( ( `' ( 1st |` ( _V X. _V ) ) o. A ) i^i ( `' ( 2nd |` ( _V X. _V ) ) o. B ) ) C_ ( _V X. ( _V X. _V ) ) |
| 19 |
1 18
|
eqsstri |
|- ( A |X. B ) C_ ( _V X. ( _V X. _V ) ) |