| Step |
Hyp |
Ref |
Expression |
| 1 |
|
id |
|- ( x = (/) -> x = (/) ) |
| 2 |
1 1
|
breq12d |
|- ( x = (/) -> ( x ~~ x <-> (/) ~~ (/) ) ) |
| 3 |
|
id |
|- ( x = y -> x = y ) |
| 4 |
3 3
|
breq12d |
|- ( x = y -> ( x ~~ x <-> y ~~ y ) ) |
| 5 |
|
id |
|- ( x = suc y -> x = suc y ) |
| 6 |
5 5
|
breq12d |
|- ( x = suc y -> ( x ~~ x <-> suc y ~~ suc y ) ) |
| 7 |
|
id |
|- ( x = A -> x = A ) |
| 8 |
7 7
|
breq12d |
|- ( x = A -> ( x ~~ x <-> A ~~ A ) ) |
| 9 |
|
eqid |
|- (/) = (/) |
| 10 |
|
en0 |
|- ( (/) ~~ (/) <-> (/) = (/) ) |
| 11 |
9 10
|
mpbir |
|- (/) ~~ (/) |
| 12 |
|
en2sn |
|- ( ( y e. _V /\ y e. _V ) -> { y } ~~ { y } ) |
| 13 |
12
|
el2v |
|- { y } ~~ { y } |
| 14 |
13
|
jctr |
|- ( y ~~ y -> ( y ~~ y /\ { y } ~~ { y } ) ) |
| 15 |
|
nnord |
|- ( y e. _om -> Ord y ) |
| 16 |
|
orddisj |
|- ( Ord y -> ( y i^i { y } ) = (/) ) |
| 17 |
15 16
|
syl |
|- ( y e. _om -> ( y i^i { y } ) = (/) ) |
| 18 |
17 17
|
jca |
|- ( y e. _om -> ( ( y i^i { y } ) = (/) /\ ( y i^i { y } ) = (/) ) ) |
| 19 |
|
unen |
|- ( ( ( y ~~ y /\ { y } ~~ { y } ) /\ ( ( y i^i { y } ) = (/) /\ ( y i^i { y } ) = (/) ) ) -> ( y u. { y } ) ~~ ( y u. { y } ) ) |
| 20 |
14 18 19
|
syl2anr |
|- ( ( y e. _om /\ y ~~ y ) -> ( y u. { y } ) ~~ ( y u. { y } ) ) |
| 21 |
|
df-suc |
|- suc y = ( y u. { y } ) |
| 22 |
20 21 21
|
3brtr4g |
|- ( ( y e. _om /\ y ~~ y ) -> suc y ~~ suc y ) |
| 23 |
22
|
ex |
|- ( y e. _om -> ( y ~~ y -> suc y ~~ suc y ) ) |
| 24 |
2 4 6 8 11 23
|
finds |
|- ( A e. _om -> A ~~ A ) |