Step |
Hyp |
Ref |
Expression |
1 |
|
enrefg |
|- ( A e. V -> A ~~ A ) |
2 |
1
|
adantr |
|- ( ( A e. V /\ -. A e. A ) -> A ~~ A ) |
3 |
|
ensn1g |
|- ( A e. V -> { A } ~~ 1o ) |
4 |
3
|
ensymd |
|- ( A e. V -> 1o ~~ { A } ) |
5 |
4
|
adantr |
|- ( ( A e. V /\ -. A e. A ) -> 1o ~~ { A } ) |
6 |
|
simpr |
|- ( ( A e. V /\ -. A e. A ) -> -. A e. A ) |
7 |
|
disjsn |
|- ( ( A i^i { A } ) = (/) <-> -. A e. A ) |
8 |
6 7
|
sylibr |
|- ( ( A e. V /\ -. A e. A ) -> ( A i^i { A } ) = (/) ) |
9 |
|
djuenun |
|- ( ( A ~~ A /\ 1o ~~ { A } /\ ( A i^i { A } ) = (/) ) -> ( A |_| 1o ) ~~ ( A u. { A } ) ) |
10 |
2 5 8 9
|
syl3anc |
|- ( ( A e. V /\ -. A e. A ) -> ( A |_| 1o ) ~~ ( A u. { A } ) ) |
11 |
|
df-suc |
|- suc A = ( A u. { A } ) |
12 |
10 11
|
breqtrrdi |
|- ( ( A e. V /\ -. A e. A ) -> ( A |_| 1o ) ~~ suc A ) |