Metamath Proof Explorer


Theorem dfsmo2

Description: Alternate definition of a strictly monotone ordinal function. (Contributed by Mario Carneiro, 4-Mar-2013)

Ref Expression
Assertion dfsmo2
|- ( Smo F <-> ( F : dom F --> On /\ Ord dom F /\ A. x e. dom F A. y e. x ( F ` y ) e. ( F ` x ) ) )

Proof

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 ) ) )