| Step |
Hyp |
Ref |
Expression |
| 1 |
|
incom |
|- ( ( inr " B ) i^i ( inl " A ) ) = ( ( inl " A ) i^i ( inr " B ) ) |
| 2 |
|
imassrn |
|- ( inr " B ) C_ ran inr |
| 3 |
|
djurf1o |
|- inr : _V -1-1-onto-> ( { 1o } X. _V ) |
| 4 |
|
f1of |
|- ( inr : _V -1-1-onto-> ( { 1o } X. _V ) -> inr : _V --> ( { 1o } X. _V ) ) |
| 5 |
|
frn |
|- ( inr : _V --> ( { 1o } X. _V ) -> ran inr C_ ( { 1o } X. _V ) ) |
| 6 |
3 4 5
|
mp2b |
|- ran inr C_ ( { 1o } X. _V ) |
| 7 |
2 6
|
sstri |
|- ( inr " B ) C_ ( { 1o } X. _V ) |
| 8 |
|
incom |
|- ( ( inl " A ) i^i ( { 1o } X. _V ) ) = ( ( { 1o } X. _V ) i^i ( inl " A ) ) |
| 9 |
|
imassrn |
|- ( inl " A ) C_ ran inl |
| 10 |
|
djulf1o |
|- inl : _V -1-1-onto-> ( { (/) } X. _V ) |
| 11 |
|
f1of |
|- ( inl : _V -1-1-onto-> ( { (/) } X. _V ) -> inl : _V --> ( { (/) } X. _V ) ) |
| 12 |
|
frn |
|- ( inl : _V --> ( { (/) } X. _V ) -> ran inl C_ ( { (/) } X. _V ) ) |
| 13 |
10 11 12
|
mp2b |
|- ran inl C_ ( { (/) } X. _V ) |
| 14 |
9 13
|
sstri |
|- ( inl " A ) C_ ( { (/) } X. _V ) |
| 15 |
|
1n0 |
|- 1o =/= (/) |
| 16 |
15
|
necomi |
|- (/) =/= 1o |
| 17 |
|
disjsn2 |
|- ( (/) =/= 1o -> ( { (/) } i^i { 1o } ) = (/) ) |
| 18 |
|
xpdisj1 |
|- ( ( { (/) } i^i { 1o } ) = (/) -> ( ( { (/) } X. _V ) i^i ( { 1o } X. _V ) ) = (/) ) |
| 19 |
16 17 18
|
mp2b |
|- ( ( { (/) } X. _V ) i^i ( { 1o } X. _V ) ) = (/) |
| 20 |
|
ssdisj |
|- ( ( ( inl " A ) C_ ( { (/) } X. _V ) /\ ( ( { (/) } X. _V ) i^i ( { 1o } X. _V ) ) = (/) ) -> ( ( inl " A ) i^i ( { 1o } X. _V ) ) = (/) ) |
| 21 |
14 19 20
|
mp2an |
|- ( ( inl " A ) i^i ( { 1o } X. _V ) ) = (/) |
| 22 |
8 21
|
eqtr3i |
|- ( ( { 1o } X. _V ) i^i ( inl " A ) ) = (/) |
| 23 |
|
ssdisj |
|- ( ( ( inr " B ) C_ ( { 1o } X. _V ) /\ ( ( { 1o } X. _V ) i^i ( inl " A ) ) = (/) ) -> ( ( inr " B ) i^i ( inl " A ) ) = (/) ) |
| 24 |
7 22 23
|
mp2an |
|- ( ( inr " B ) i^i ( inl " A ) ) = (/) |
| 25 |
1 24
|
eqtr3i |
|- ( ( inl " A ) i^i ( inr " B ) ) = (/) |