Step |
Hyp |
Ref |
Expression |
1 |
|
unsnen.1 |
|- A e. _V |
2 |
|
unsnen.2 |
|- B e. _V |
3 |
|
disjsn |
|- ( ( A i^i { B } ) = (/) <-> -. B e. A ) |
4 |
|
cardon |
|- ( card ` A ) e. On |
5 |
4
|
onordi |
|- Ord ( card ` A ) |
6 |
|
orddisj |
|- ( Ord ( card ` A ) -> ( ( card ` A ) i^i { ( card ` A ) } ) = (/) ) |
7 |
5 6
|
ax-mp |
|- ( ( card ` A ) i^i { ( card ` A ) } ) = (/) |
8 |
1
|
cardid |
|- ( card ` A ) ~~ A |
9 |
8
|
ensymi |
|- A ~~ ( card ` A ) |
10 |
|
fvex |
|- ( card ` A ) e. _V |
11 |
|
en2sn |
|- ( ( B e. _V /\ ( card ` A ) e. _V ) -> { B } ~~ { ( card ` A ) } ) |
12 |
2 10 11
|
mp2an |
|- { B } ~~ { ( card ` A ) } |
13 |
|
unen |
|- ( ( ( A ~~ ( card ` A ) /\ { B } ~~ { ( card ` A ) } ) /\ ( ( A i^i { B } ) = (/) /\ ( ( card ` A ) i^i { ( card ` A ) } ) = (/) ) ) -> ( A u. { B } ) ~~ ( ( card ` A ) u. { ( card ` A ) } ) ) |
14 |
9 12 13
|
mpanl12 |
|- ( ( ( A i^i { B } ) = (/) /\ ( ( card ` A ) i^i { ( card ` A ) } ) = (/) ) -> ( A u. { B } ) ~~ ( ( card ` A ) u. { ( card ` A ) } ) ) |
15 |
7 14
|
mpan2 |
|- ( ( A i^i { B } ) = (/) -> ( A u. { B } ) ~~ ( ( card ` A ) u. { ( card ` A ) } ) ) |
16 |
3 15
|
sylbir |
|- ( -. B e. A -> ( A u. { B } ) ~~ ( ( card ` A ) u. { ( card ` A ) } ) ) |
17 |
|
df-suc |
|- suc ( card ` A ) = ( ( card ` A ) u. { ( card ` A ) } ) |
18 |
16 17
|
breqtrrdi |
|- ( -. B e. A -> ( A u. { B } ) ~~ suc ( card ` A ) ) |