Step |
Hyp |
Ref |
Expression |
1 |
|
unwf |
|- ( ( A e. U. ( R1 " On ) /\ B e. U. ( R1 " On ) ) <-> ( A u. B ) e. U. ( R1 " On ) ) |
2 |
|
rankval3b |
|- ( ( A u. B ) e. U. ( R1 " On ) -> ( rank ` ( A u. B ) ) = |^| { y e. On | A. x e. ( A u. B ) ( rank ` x ) e. y } ) |
3 |
1 2
|
sylbi |
|- ( ( A e. U. ( R1 " On ) /\ B e. U. ( R1 " On ) ) -> ( rank ` ( A u. B ) ) = |^| { y e. On | A. x e. ( A u. B ) ( rank ` x ) e. y } ) |
4 |
3
|
eleq2d |
|- ( ( A e. U. ( R1 " On ) /\ B e. U. ( R1 " On ) ) -> ( x e. ( rank ` ( A u. B ) ) <-> x e. |^| { y e. On | A. x e. ( A u. B ) ( rank ` x ) e. y } ) ) |
5 |
|
vex |
|- x e. _V |
6 |
5
|
elintrab |
|- ( x e. |^| { y e. On | A. x e. ( A u. B ) ( rank ` x ) e. y } <-> A. y e. On ( A. x e. ( A u. B ) ( rank ` x ) e. y -> x e. y ) ) |
7 |
4 6
|
bitrdi |
|- ( ( A e. U. ( R1 " On ) /\ B e. U. ( R1 " On ) ) -> ( x e. ( rank ` ( A u. B ) ) <-> A. y e. On ( A. x e. ( A u. B ) ( rank ` x ) e. y -> x e. y ) ) ) |
8 |
|
elun |
|- ( x e. ( A u. B ) <-> ( x e. A \/ x e. B ) ) |
9 |
|
rankelb |
|- ( A e. U. ( R1 " On ) -> ( x e. A -> ( rank ` x ) e. ( rank ` A ) ) ) |
10 |
|
elun1 |
|- ( ( rank ` x ) e. ( rank ` A ) -> ( rank ` x ) e. ( ( rank ` A ) u. ( rank ` B ) ) ) |
11 |
9 10
|
syl6 |
|- ( A e. U. ( R1 " On ) -> ( x e. A -> ( rank ` x ) e. ( ( rank ` A ) u. ( rank ` B ) ) ) ) |
12 |
|
rankelb |
|- ( B e. U. ( R1 " On ) -> ( x e. B -> ( rank ` x ) e. ( rank ` B ) ) ) |
13 |
|
elun2 |
|- ( ( rank ` x ) e. ( rank ` B ) -> ( rank ` x ) e. ( ( rank ` A ) u. ( rank ` B ) ) ) |
14 |
12 13
|
syl6 |
|- ( B e. U. ( R1 " On ) -> ( x e. B -> ( rank ` x ) e. ( ( rank ` A ) u. ( rank ` B ) ) ) ) |
15 |
11 14
|
jaao |
|- ( ( A e. U. ( R1 " On ) /\ B e. U. ( R1 " On ) ) -> ( ( x e. A \/ x e. B ) -> ( rank ` x ) e. ( ( rank ` A ) u. ( rank ` B ) ) ) ) |
16 |
8 15
|
syl5bi |
|- ( ( A e. U. ( R1 " On ) /\ B e. U. ( R1 " On ) ) -> ( x e. ( A u. B ) -> ( rank ` x ) e. ( ( rank ` A ) u. ( rank ` B ) ) ) ) |
17 |
16
|
ralrimiv |
|- ( ( A e. U. ( R1 " On ) /\ B e. U. ( R1 " On ) ) -> A. x e. ( A u. B ) ( rank ` x ) e. ( ( rank ` A ) u. ( rank ` B ) ) ) |
18 |
|
rankon |
|- ( rank ` A ) e. On |
19 |
|
rankon |
|- ( rank ` B ) e. On |
20 |
18 19
|
onun2i |
|- ( ( rank ` A ) u. ( rank ` B ) ) e. On |
21 |
|
eleq2 |
|- ( y = ( ( rank ` A ) u. ( rank ` B ) ) -> ( ( rank ` x ) e. y <-> ( rank ` x ) e. ( ( rank ` A ) u. ( rank ` B ) ) ) ) |
22 |
21
|
ralbidv |
|- ( y = ( ( rank ` A ) u. ( rank ` B ) ) -> ( A. x e. ( A u. B ) ( rank ` x ) e. y <-> A. x e. ( A u. B ) ( rank ` x ) e. ( ( rank ` A ) u. ( rank ` B ) ) ) ) |
23 |
|
eleq2 |
|- ( y = ( ( rank ` A ) u. ( rank ` B ) ) -> ( x e. y <-> x e. ( ( rank ` A ) u. ( rank ` B ) ) ) ) |
24 |
22 23
|
imbi12d |
|- ( y = ( ( rank ` A ) u. ( rank ` B ) ) -> ( ( A. x e. ( A u. B ) ( rank ` x ) e. y -> x e. y ) <-> ( A. x e. ( A u. B ) ( rank ` x ) e. ( ( rank ` A ) u. ( rank ` B ) ) -> x e. ( ( rank ` A ) u. ( rank ` B ) ) ) ) ) |
25 |
24
|
rspcv |
|- ( ( ( rank ` A ) u. ( rank ` B ) ) e. On -> ( A. y e. On ( A. x e. ( A u. B ) ( rank ` x ) e. y -> x e. y ) -> ( A. x e. ( A u. B ) ( rank ` x ) e. ( ( rank ` A ) u. ( rank ` B ) ) -> x e. ( ( rank ` A ) u. ( rank ` B ) ) ) ) ) |
26 |
20 25
|
ax-mp |
|- ( A. y e. On ( A. x e. ( A u. B ) ( rank ` x ) e. y -> x e. y ) -> ( A. x e. ( A u. B ) ( rank ` x ) e. ( ( rank ` A ) u. ( rank ` B ) ) -> x e. ( ( rank ` A ) u. ( rank ` B ) ) ) ) |
27 |
17 26
|
syl5com |
|- ( ( A e. U. ( R1 " On ) /\ B e. U. ( R1 " On ) ) -> ( A. y e. On ( A. x e. ( A u. B ) ( rank ` x ) e. y -> x e. y ) -> x e. ( ( rank ` A ) u. ( rank ` B ) ) ) ) |
28 |
7 27
|
sylbid |
|- ( ( A e. U. ( R1 " On ) /\ B e. U. ( R1 " On ) ) -> ( x e. ( rank ` ( A u. B ) ) -> x e. ( ( rank ` A ) u. ( rank ` B ) ) ) ) |
29 |
28
|
ssrdv |
|- ( ( A e. U. ( R1 " On ) /\ B e. U. ( R1 " On ) ) -> ( rank ` ( A u. B ) ) C_ ( ( rank ` A ) u. ( rank ` B ) ) ) |
30 |
|
ssun1 |
|- A C_ ( A u. B ) |
31 |
|
rankssb |
|- ( ( A u. B ) e. U. ( R1 " On ) -> ( A C_ ( A u. B ) -> ( rank ` A ) C_ ( rank ` ( A u. B ) ) ) ) |
32 |
30 31
|
mpi |
|- ( ( A u. B ) e. U. ( R1 " On ) -> ( rank ` A ) C_ ( rank ` ( A u. B ) ) ) |
33 |
|
ssun2 |
|- B C_ ( A u. B ) |
34 |
|
rankssb |
|- ( ( A u. B ) e. U. ( R1 " On ) -> ( B C_ ( A u. B ) -> ( rank ` B ) C_ ( rank ` ( A u. B ) ) ) ) |
35 |
33 34
|
mpi |
|- ( ( A u. B ) e. U. ( R1 " On ) -> ( rank ` B ) C_ ( rank ` ( A u. B ) ) ) |
36 |
32 35
|
unssd |
|- ( ( A u. B ) e. U. ( R1 " On ) -> ( ( rank ` A ) u. ( rank ` B ) ) C_ ( rank ` ( A u. B ) ) ) |
37 |
1 36
|
sylbi |
|- ( ( A e. U. ( R1 " On ) /\ B e. U. ( R1 " On ) ) -> ( ( rank ` A ) u. ( rank ` B ) ) C_ ( rank ` ( A u. B ) ) ) |
38 |
29 37
|
eqssd |
|- ( ( A e. U. ( R1 " On ) /\ B e. U. ( R1 " On ) ) -> ( rank ` ( A u. B ) ) = ( ( rank ` A ) u. ( rank ` B ) ) ) |