Step |
Hyp |
Ref |
Expression |
1 |
|
df-smo |
|- ( Smo F <-> ( F : dom F --> On /\ Ord dom F /\ A. y e. dom F A. x e. dom F ( y e. x -> ( F ` y ) e. ( F ` x ) ) ) ) |
2 |
|
ralcom |
|- ( A. y e. dom F A. x e. dom F ( y e. x -> ( F ` y ) e. ( F ` x ) ) <-> A. x e. dom F A. y e. dom F ( y e. x -> ( F ` y ) e. ( F ` x ) ) ) |
3 |
|
impexp |
|- ( ( ( y e. dom F /\ y e. x ) -> ( F ` y ) e. ( F ` x ) ) <-> ( y e. dom F -> ( y e. x -> ( F ` y ) e. ( F ` x ) ) ) ) |
4 |
|
simpr |
|- ( ( y e. dom F /\ y e. x ) -> y e. x ) |
5 |
|
ordtr1 |
|- ( Ord dom F -> ( ( y e. x /\ x e. dom F ) -> y e. dom F ) ) |
6 |
5
|
3impib |
|- ( ( Ord dom F /\ y e. x /\ x e. dom F ) -> y e. dom F ) |
7 |
6
|
3com23 |
|- ( ( Ord dom F /\ x e. dom F /\ y e. x ) -> y e. dom F ) |
8 |
|
simp3 |
|- ( ( Ord dom F /\ x e. dom F /\ y e. x ) -> y e. x ) |
9 |
7 8
|
jca |
|- ( ( Ord dom F /\ x e. dom F /\ y e. x ) -> ( y e. dom F /\ y e. x ) ) |
10 |
9
|
3expia |
|- ( ( Ord dom F /\ x e. dom F ) -> ( y e. x -> ( y e. dom F /\ y e. x ) ) ) |
11 |
4 10
|
impbid2 |
|- ( ( Ord dom F /\ x e. dom F ) -> ( ( y e. dom F /\ y e. x ) <-> y e. x ) ) |
12 |
11
|
imbi1d |
|- ( ( Ord dom F /\ x e. dom F ) -> ( ( ( y e. dom F /\ y e. x ) -> ( F ` y ) e. ( F ` x ) ) <-> ( y e. x -> ( F ` y ) e. ( F ` x ) ) ) ) |
13 |
3 12
|
bitr3id |
|- ( ( Ord dom F /\ x e. dom F ) -> ( ( y e. dom F -> ( y e. x -> ( F ` y ) e. ( F ` x ) ) ) <-> ( y e. x -> ( F ` y ) e. ( F ` x ) ) ) ) |
14 |
13
|
ralbidv2 |
|- ( ( Ord dom F /\ x e. dom F ) -> ( A. y e. dom F ( y e. x -> ( F ` y ) e. ( F ` x ) ) <-> A. y e. x ( F ` y ) e. ( F ` x ) ) ) |
15 |
14
|
ralbidva |
|- ( Ord dom F -> ( A. x e. dom F A. y e. dom F ( y e. x -> ( F ` y ) e. ( F ` x ) ) <-> A. x e. dom F A. y e. x ( F ` y ) e. ( F ` x ) ) ) |
16 |
2 15
|
syl5bb |
|- ( Ord dom F -> ( A. y e. dom F A. x e. dom F ( y e. x -> ( F ` y ) e. ( F ` x ) ) <-> A. x e. dom F A. y e. x ( F ` y ) e. ( F ` x ) ) ) |
17 |
16
|
pm5.32i |
|- ( ( Ord dom F /\ A. y e. dom F A. x e. dom F ( y e. x -> ( F ` y ) e. ( F ` x ) ) ) <-> ( Ord dom F /\ A. x e. dom F A. y e. x ( F ` y ) e. ( F ` x ) ) ) |
18 |
17
|
anbi2i |
|- ( ( F : dom F --> On /\ ( Ord dom F /\ A. y e. dom F A. x e. dom F ( y e. x -> ( F ` y ) e. ( F ` x ) ) ) ) <-> ( F : dom F --> On /\ ( Ord dom F /\ A. x e. dom F A. y e. x ( F ` y ) e. ( F ` x ) ) ) ) |
19 |
|
3anass |
|- ( ( F : dom F --> On /\ Ord dom F /\ A. y e. dom F A. x e. dom F ( y e. x -> ( F ` y ) e. ( F ` x ) ) ) <-> ( F : dom F --> On /\ ( Ord dom F /\ A. y e. dom F A. x e. dom F ( y e. x -> ( F ` y ) e. ( F ` x ) ) ) ) ) |
20 |
|
3anass |
|- ( ( F : dom F --> On /\ Ord dom F /\ A. x e. dom F A. y e. x ( F ` y ) e. ( F ` x ) ) <-> ( F : dom F --> On /\ ( Ord dom F /\ A. x e. dom F A. y e. x ( F ` y ) e. ( F ` x ) ) ) ) |
21 |
18 19 20
|
3bitr4i |
|- ( ( F : dom F --> On /\ Ord dom F /\ A. y e. dom F A. x e. dom F ( y e. x -> ( F ` y ) e. ( F ` x ) ) ) <-> ( F : dom F --> On /\ Ord dom F /\ A. x e. dom F A. y e. x ( F ` y ) e. ( F ` x ) ) ) |
22 |
1 21
|
bitri |
|- ( Smo F <-> ( F : dom F --> On /\ Ord dom F /\ A. x e. dom F A. y e. x ( F ` y ) e. ( F ` x ) ) ) |