Step |
Hyp |
Ref |
Expression |
0 |
|
cA |
|- A |
1 |
0
|
wsmo |
|- Smo A |
2 |
0
|
cdm |
|- dom A |
3 |
|
con0 |
|- On |
4 |
2 3 0
|
wf |
|- A : dom A --> On |
5 |
2
|
word |
|- Ord dom A |
6 |
|
vx |
|- x |
7 |
|
vy |
|- y |
8 |
6
|
cv |
|- x |
9 |
7
|
cv |
|- y |
10 |
8 9
|
wcel |
|- x e. y |
11 |
8 0
|
cfv |
|- ( A ` x ) |
12 |
9 0
|
cfv |
|- ( A ` y ) |
13 |
11 12
|
wcel |
|- ( A ` x ) e. ( A ` y ) |
14 |
10 13
|
wi |
|- ( x e. y -> ( A ` x ) e. ( A ` y ) ) |
15 |
14 7 2
|
wral |
|- A. y e. dom A ( x e. y -> ( A ` x ) e. ( A ` y ) ) |
16 |
15 6 2
|
wral |
|- A. x e. dom A A. y e. dom A ( x e. y -> ( A ` x ) e. ( A ` y ) ) |
17 |
4 5 16
|
w3a |
|- ( A : dom A --> On /\ Ord dom A /\ A. x e. dom A A. y e. dom A ( x e. y -> ( A ` x ) e. ( A ` y ) ) ) |
18 |
1 17
|
wb |
|- ( Smo A <-> ( A : dom A --> On /\ Ord dom A /\ A. x e. dom A A. y e. dom A ( x e. y -> ( A ` x ) e. ( A ` y ) ) ) ) |