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