Step |
Hyp |
Ref |
Expression |
1 |
|
ordun |
|- ( ( Ord A /\ Ord B ) -> Ord ( A u. B ) ) |
2 |
|
ordsuc |
|- ( Ord ( A u. B ) <-> Ord suc ( A u. B ) ) |
3 |
|
ordelon |
|- ( ( Ord suc ( A u. B ) /\ x e. suc ( A u. B ) ) -> x e. On ) |
4 |
3
|
ex |
|- ( Ord suc ( A u. B ) -> ( x e. suc ( A u. B ) -> x e. On ) ) |
5 |
2 4
|
sylbi |
|- ( Ord ( A u. B ) -> ( x e. suc ( A u. B ) -> x e. On ) ) |
6 |
1 5
|
syl |
|- ( ( Ord A /\ Ord B ) -> ( x e. suc ( A u. B ) -> x e. On ) ) |
7 |
|
ordsuc |
|- ( Ord A <-> Ord suc A ) |
8 |
|
ordsuc |
|- ( Ord B <-> Ord suc B ) |
9 |
|
ordun |
|- ( ( Ord suc A /\ Ord suc B ) -> Ord ( suc A u. suc B ) ) |
10 |
|
ordelon |
|- ( ( Ord ( suc A u. suc B ) /\ x e. ( suc A u. suc B ) ) -> x e. On ) |
11 |
10
|
ex |
|- ( Ord ( suc A u. suc B ) -> ( x e. ( suc A u. suc B ) -> x e. On ) ) |
12 |
9 11
|
syl |
|- ( ( Ord suc A /\ Ord suc B ) -> ( x e. ( suc A u. suc B ) -> x e. On ) ) |
13 |
7 8 12
|
syl2anb |
|- ( ( Ord A /\ Ord B ) -> ( x e. ( suc A u. suc B ) -> x e. On ) ) |
14 |
|
ordssun |
|- ( ( Ord A /\ Ord B ) -> ( x C_ ( A u. B ) <-> ( x C_ A \/ x C_ B ) ) ) |
15 |
14
|
adantl |
|- ( ( x e. On /\ ( Ord A /\ Ord B ) ) -> ( x C_ ( A u. B ) <-> ( x C_ A \/ x C_ B ) ) ) |
16 |
|
ordsssuc |
|- ( ( x e. On /\ Ord ( A u. B ) ) -> ( x C_ ( A u. B ) <-> x e. suc ( A u. B ) ) ) |
17 |
1 16
|
sylan2 |
|- ( ( x e. On /\ ( Ord A /\ Ord B ) ) -> ( x C_ ( A u. B ) <-> x e. suc ( A u. B ) ) ) |
18 |
|
ordsssuc |
|- ( ( x e. On /\ Ord A ) -> ( x C_ A <-> x e. suc A ) ) |
19 |
18
|
adantrr |
|- ( ( x e. On /\ ( Ord A /\ Ord B ) ) -> ( x C_ A <-> x e. suc A ) ) |
20 |
|
ordsssuc |
|- ( ( x e. On /\ Ord B ) -> ( x C_ B <-> x e. suc B ) ) |
21 |
20
|
adantrl |
|- ( ( x e. On /\ ( Ord A /\ Ord B ) ) -> ( x C_ B <-> x e. suc B ) ) |
22 |
19 21
|
orbi12d |
|- ( ( x e. On /\ ( Ord A /\ Ord B ) ) -> ( ( x C_ A \/ x C_ B ) <-> ( x e. suc A \/ x e. suc B ) ) ) |
23 |
15 17 22
|
3bitr3d |
|- ( ( x e. On /\ ( Ord A /\ Ord B ) ) -> ( x e. suc ( A u. B ) <-> ( x e. suc A \/ x e. suc B ) ) ) |
24 |
|
elun |
|- ( x e. ( suc A u. suc B ) <-> ( x e. suc A \/ x e. suc B ) ) |
25 |
23 24
|
bitr4di |
|- ( ( x e. On /\ ( Ord A /\ Ord B ) ) -> ( x e. suc ( A u. B ) <-> x e. ( suc A u. suc B ) ) ) |
26 |
25
|
expcom |
|- ( ( Ord A /\ Ord B ) -> ( x e. On -> ( x e. suc ( A u. B ) <-> x e. ( suc A u. suc B ) ) ) ) |
27 |
6 13 26
|
pm5.21ndd |
|- ( ( Ord A /\ Ord B ) -> ( x e. suc ( A u. B ) <-> x e. ( suc A u. suc B ) ) ) |
28 |
27
|
eqrdv |
|- ( ( Ord A /\ Ord B ) -> suc ( A u. B ) = ( suc A u. suc B ) ) |