Step |
Hyp |
Ref |
Expression |
1 |
|
rankxpl.1 |
|- A e. _V |
2 |
|
rankxpl.2 |
|- B e. _V |
3 |
|
xpsspw |
|- ( A X. B ) C_ ~P ~P ( A u. B ) |
4 |
1 2
|
unex |
|- ( A u. B ) e. _V |
5 |
4
|
pwex |
|- ~P ( A u. B ) e. _V |
6 |
5
|
pwex |
|- ~P ~P ( A u. B ) e. _V |
7 |
6
|
rankss |
|- ( ( A X. B ) C_ ~P ~P ( A u. B ) -> ( rank ` ( A X. B ) ) C_ ( rank ` ~P ~P ( A u. B ) ) ) |
8 |
3 7
|
ax-mp |
|- ( rank ` ( A X. B ) ) C_ ( rank ` ~P ~P ( A u. B ) ) |
9 |
5
|
rankpw |
|- ( rank ` ~P ~P ( A u. B ) ) = suc ( rank ` ~P ( A u. B ) ) |
10 |
4
|
rankpw |
|- ( rank ` ~P ( A u. B ) ) = suc ( rank ` ( A u. B ) ) |
11 |
|
suceq |
|- ( ( rank ` ~P ( A u. B ) ) = suc ( rank ` ( A u. B ) ) -> suc ( rank ` ~P ( A u. B ) ) = suc suc ( rank ` ( A u. B ) ) ) |
12 |
10 11
|
ax-mp |
|- suc ( rank ` ~P ( A u. B ) ) = suc suc ( rank ` ( A u. B ) ) |
13 |
9 12
|
eqtri |
|- ( rank ` ~P ~P ( A u. B ) ) = suc suc ( rank ` ( A u. B ) ) |
14 |
8 13
|
sseqtri |
|- ( rank ` ( A X. B ) ) C_ suc suc ( rank ` ( A u. B ) ) |