Step |
Hyp |
Ref |
Expression |
1 |
|
elin |
|- ( x e. ( ~P A i^i On ) <-> ( x e. ~P A /\ x e. On ) ) |
2 |
|
velpw |
|- ( x e. ~P A <-> x C_ A ) |
3 |
2
|
anbi2ci |
|- ( ( x e. ~P A /\ x e. On ) <-> ( x e. On /\ x C_ A ) ) |
4 |
1 3
|
bitri |
|- ( x e. ( ~P A i^i On ) <-> ( x e. On /\ x C_ A ) ) |
5 |
|
ordsssuc |
|- ( ( x e. On /\ Ord A ) -> ( x C_ A <-> x e. suc A ) ) |
6 |
5
|
expcom |
|- ( Ord A -> ( x e. On -> ( x C_ A <-> x e. suc A ) ) ) |
7 |
6
|
pm5.32d |
|- ( Ord A -> ( ( x e. On /\ x C_ A ) <-> ( x e. On /\ x e. suc A ) ) ) |
8 |
|
simpr |
|- ( ( x e. On /\ x e. suc A ) -> x e. suc A ) |
9 |
|
ordsuc |
|- ( Ord A <-> Ord suc A ) |
10 |
|
ordelon |
|- ( ( Ord suc A /\ x e. suc A ) -> x e. On ) |
11 |
10
|
ex |
|- ( Ord suc A -> ( x e. suc A -> x e. On ) ) |
12 |
9 11
|
sylbi |
|- ( Ord A -> ( x e. suc A -> x e. On ) ) |
13 |
12
|
ancrd |
|- ( Ord A -> ( x e. suc A -> ( x e. On /\ x e. suc A ) ) ) |
14 |
8 13
|
impbid2 |
|- ( Ord A -> ( ( x e. On /\ x e. suc A ) <-> x e. suc A ) ) |
15 |
7 14
|
bitrd |
|- ( Ord A -> ( ( x e. On /\ x C_ A ) <-> x e. suc A ) ) |
16 |
4 15
|
syl5bb |
|- ( Ord A -> ( x e. ( ~P A i^i On ) <-> x e. suc A ) ) |
17 |
16
|
eqrdv |
|- ( Ord A -> ( ~P A i^i On ) = suc A ) |