Step |
Hyp |
Ref |
Expression |
1 |
|
snex |
|- { (/) } e. _V |
2 |
1
|
xpdom2 |
|- ( A ~<_ B -> ( { (/) } X. A ) ~<_ ( { (/) } X. B ) ) |
3 |
|
snex |
|- { 1o } e. _V |
4 |
|
xpexg |
|- ( ( { 1o } e. _V /\ C e. V ) -> ( { 1o } X. C ) e. _V ) |
5 |
3 4
|
mpan |
|- ( C e. V -> ( { 1o } X. C ) e. _V ) |
6 |
|
domrefg |
|- ( ( { 1o } X. C ) e. _V -> ( { 1o } X. C ) ~<_ ( { 1o } X. C ) ) |
7 |
5 6
|
syl |
|- ( C e. V -> ( { 1o } X. C ) ~<_ ( { 1o } X. C ) ) |
8 |
|
xp01disjl |
|- ( ( { (/) } X. B ) i^i ( { 1o } X. C ) ) = (/) |
9 |
|
undom |
|- ( ( ( ( { (/) } X. A ) ~<_ ( { (/) } X. B ) /\ ( { 1o } X. C ) ~<_ ( { 1o } X. C ) ) /\ ( ( { (/) } X. B ) i^i ( { 1o } X. C ) ) = (/) ) -> ( ( { (/) } X. A ) u. ( { 1o } X. C ) ) ~<_ ( ( { (/) } X. B ) u. ( { 1o } X. C ) ) ) |
10 |
8 9
|
mpan2 |
|- ( ( ( { (/) } X. A ) ~<_ ( { (/) } X. B ) /\ ( { 1o } X. C ) ~<_ ( { 1o } X. C ) ) -> ( ( { (/) } X. A ) u. ( { 1o } X. C ) ) ~<_ ( ( { (/) } X. B ) u. ( { 1o } X. C ) ) ) |
11 |
2 7 10
|
syl2an |
|- ( ( A ~<_ B /\ C e. V ) -> ( ( { (/) } X. A ) u. ( { 1o } X. C ) ) ~<_ ( ( { (/) } X. B ) u. ( { 1o } X. C ) ) ) |
12 |
|
df-dju |
|- ( A |_| C ) = ( ( { (/) } X. A ) u. ( { 1o } X. C ) ) |
13 |
|
df-dju |
|- ( B |_| C ) = ( ( { (/) } X. B ) u. ( { 1o } X. C ) ) |
14 |
11 12 13
|
3brtr4g |
|- ( ( A ~<_ B /\ C e. V ) -> ( A |_| C ) ~<_ ( B |_| C ) ) |