Metamath Proof Explorer

Theorem uzindi

Description: Indirect strong induction on the upper integers. (Contributed by Stefan O'Rear, 25-Aug-2015)

Ref Expression
Hypotheses uzindi.a 
|- ( ph -> A e. V )
uzindi.b 
|- ( ph -> T e. ( ZZ>= ` L ) )
uzindi.c 
|- ( ( ph /\ R e. ( L ... T ) /\ A. y ( S e. ( L ..^ R ) -> ch ) ) -> ps )
uzindi.d 
|- ( x = y -> ( ps <-> ch ) )
uzindi.e 
|- ( x = A -> ( ps <-> th ) )
uzindi.f 
|- ( x = y -> R = S )
uzindi.g 
|- ( x = A -> R = T )
Assertion uzindi 
|- ( ph -> th )

Proof

Step Hyp Ref Expression
1 uzindi.a 
 |-  ( ph -> A e. V )
2 uzindi.b 
 |-  ( ph -> T e. ( ZZ>= ` L ) )
3 uzindi.c 
 |-  ( ( ph /\ R e. ( L ... T ) /\ A. y ( S e. ( L ..^ R ) -> ch ) ) -> ps )
4 uzindi.d 
 |-  ( x = y -> ( ps <-> ch ) )
5 uzindi.e 
 |-  ( x = A -> ( ps <-> th ) )
6 uzindi.f 
 |-  ( x = y -> R = S )
7 uzindi.g 
 |-  ( x = A -> R = T )
8 eluzfz2 
 |-  ( T e. ( ZZ>= ` L ) -> T e. ( L ... T ) )
9 2 8 syl 
 |-  ( ph -> T e. ( L ... T ) )
10 fzofi 
 |-  ( L ..^ T ) e. Fin
11 finnum 
 |-  ( ( L ..^ T ) e. Fin -> ( L ..^ T ) e. dom card )
12 10 11 mp1i 
 |-  ( ph -> ( L ..^ T ) e. dom card )
13 simpll 
 |-  ( ( ( ph /\ A. y ( ( L ..^ S ) ~< ( L ..^ R ) -> ( S e. ( L ... T ) -> ch ) ) ) /\ R e. ( L ... T ) ) -> ph )
14 simpr 
 |-  ( ( ( ph /\ A. y ( ( L ..^ S ) ~< ( L ..^ R ) -> ( S e. ( L ... T ) -> ch ) ) ) /\ R e. ( L ... T ) ) -> R e. ( L ... T ) )
15 elfzuz3 
 |-  ( R e. ( L ... T ) -> T e. ( ZZ>= ` R ) )
16 15 adantl 
 |-  ( ( ph /\ R e. ( L ... T ) ) -> T e. ( ZZ>= ` R ) )
17 fzoss2 
 |-  ( T e. ( ZZ>= ` R ) -> ( L ..^ R ) C_ ( L ..^ T ) )
18 fzossfz 
 |-  ( L ..^ T ) C_ ( L ... T )
19 17 18 sstrdi 
 |-  ( T e. ( ZZ>= ` R ) -> ( L ..^ R ) C_ ( L ... T ) )
20 16 19 syl 
 |-  ( ( ph /\ R e. ( L ... T ) ) -> ( L ..^ R ) C_ ( L ... T ) )
21 20 sselda 
 |-  ( ( ( ph /\ R e. ( L ... T ) ) /\ S e. ( L ..^ R ) ) -> S e. ( L ... T ) )
22 fzofi 
 |-  ( L ..^ R ) e. Fin
23 elfzofz 
 |-  ( S e. ( L ..^ R ) -> S e. ( L ... R ) )
24 23 adantl 
 |-  ( ( ( ph /\ R e. ( L ... T ) ) /\ S e. ( L ..^ R ) ) -> S e. ( L ... R ) )
25 elfzuz3 
 |-  ( S e. ( L ... R ) -> R e. ( ZZ>= ` S ) )
26 fzoss2 
 |-  ( R e. ( ZZ>= ` S ) -> ( L ..^ S ) C_ ( L ..^ R ) )
27 24 25 26 3syl 
 |-  ( ( ( ph /\ R e. ( L ... T ) ) /\ S e. ( L ..^ R ) ) -> ( L ..^ S ) C_ ( L ..^ R ) )
28 fzonel 
 |-  -. S e. ( L ..^ S )
29 28 jctr 
 |-  ( S e. ( L ..^ R ) -> ( S e. ( L ..^ R ) /\ -. S e. ( L ..^ S ) ) )
30 29 adantl 
 |-  ( ( ( ph /\ R e. ( L ... T ) ) /\ S e. ( L ..^ R ) ) -> ( S e. ( L ..^ R ) /\ -. S e. ( L ..^ S ) ) )
31 ssnelpss 
 |-  ( ( L ..^ S ) C_ ( L ..^ R ) -> ( ( S e. ( L ..^ R ) /\ -. S e. ( L ..^ S ) ) -> ( L ..^ S ) C. ( L ..^ R ) ) )
32 27 30 31 sylc 
 |-  ( ( ( ph /\ R e. ( L ... T ) ) /\ S e. ( L ..^ R ) ) -> ( L ..^ S ) C. ( L ..^ R ) )
33 php3 
 |-  ( ( ( L ..^ R ) e. Fin /\ ( L ..^ S ) C. ( L ..^ R ) ) -> ( L ..^ S ) ~< ( L ..^ R ) )
34 22 32 33 sylancr 
 |-  ( ( ( ph /\ R e. ( L ... T ) ) /\ S e. ( L ..^ R ) ) -> ( L ..^ S ) ~< ( L ..^ R ) )
35 id 
 |-  ( ( ( L ..^ S ) ~< ( L ..^ R ) -> ( S e. ( L ... T ) -> ch ) ) -> ( ( L ..^ S ) ~< ( L ..^ R ) -> ( S e. ( L ... T ) -> ch ) ) )
36 35 com13 
 |-  ( S e. ( L ... T ) -> ( ( L ..^ S ) ~< ( L ..^ R ) -> ( ( ( L ..^ S ) ~< ( L ..^ R ) -> ( S e. ( L ... T ) -> ch ) ) -> ch ) ) )
37 21 34 36 sylc 
 |-  ( ( ( ph /\ R e. ( L ... T ) ) /\ S e. ( L ..^ R ) ) -> ( ( ( L ..^ S ) ~< ( L ..^ R ) -> ( S e. ( L ... T ) -> ch ) ) -> ch ) )
38 37 ex 
 |-  ( ( ph /\ R e. ( L ... T ) ) -> ( S e. ( L ..^ R ) -> ( ( ( L ..^ S ) ~< ( L ..^ R ) -> ( S e. ( L ... T ) -> ch ) ) -> ch ) ) )
39 38 com23 
 |-  ( ( ph /\ R e. ( L ... T ) ) -> ( ( ( L ..^ S ) ~< ( L ..^ R ) -> ( S e. ( L ... T ) -> ch ) ) -> ( S e. ( L ..^ R ) -> ch ) ) )
40 39 alimdv 
 |-  ( ( ph /\ R e. ( L ... T ) ) -> ( A. y ( ( L ..^ S ) ~< ( L ..^ R ) -> ( S e. ( L ... T ) -> ch ) ) -> A. y ( S e. ( L ..^ R ) -> ch ) ) )
41 40 ex 
 |-  ( ph -> ( R e. ( L ... T ) -> ( A. y ( ( L ..^ S ) ~< ( L ..^ R ) -> ( S e. ( L ... T ) -> ch ) ) -> A. y ( S e. ( L ..^ R ) -> ch ) ) ) )
42 41 com23 
 |-  ( ph -> ( A. y ( ( L ..^ S ) ~< ( L ..^ R ) -> ( S e. ( L ... T ) -> ch ) ) -> ( R e. ( L ... T ) -> A. y ( S e. ( L ..^ R ) -> ch ) ) ) )
43 42 imp31 
 |-  ( ( ( ph /\ A. y ( ( L ..^ S ) ~< ( L ..^ R ) -> ( S e. ( L ... T ) -> ch ) ) ) /\ R e. ( L ... T ) ) -> A. y ( S e. ( L ..^ R ) -> ch ) )
44 13 14 43 3 syl3anc 
 |-  ( ( ( ph /\ A. y ( ( L ..^ S ) ~< ( L ..^ R ) -> ( S e. ( L ... T ) -> ch ) ) ) /\ R e. ( L ... T ) ) -> ps )
45 44 ex 
 |-  ( ( ph /\ A. y ( ( L ..^ S ) ~< ( L ..^ R ) -> ( S e. ( L ... T ) -> ch ) ) ) -> ( R e. ( L ... T ) -> ps ) )
46 45 3adant2 
 |-  ( ( ph /\ ( L ..^ R ) ~<_ ( L ..^ T ) /\ A. y ( ( L ..^ S ) ~< ( L ..^ R ) -> ( S e. ( L ... T ) -> ch ) ) ) -> ( R e. ( L ... T ) -> ps ) )
47 6 eleq1d 
 |-  ( x = y -> ( R e. ( L ... T ) <-> S e. ( L ... T ) ) )
48 47 4 imbi12d 
 |-  ( x = y -> ( ( R e. ( L ... T ) -> ps ) <-> ( S e. ( L ... T ) -> ch ) ) )
49 7 eleq1d 
 |-  ( x = A -> ( R e. ( L ... T ) <-> T e. ( L ... T ) ) )
50 49 5 imbi12d 
 |-  ( x = A -> ( ( R e. ( L ... T ) -> ps ) <-> ( T e. ( L ... T ) -> th ) ) )
51 6 oveq2d 
 |-  ( x = y -> ( L ..^ R ) = ( L ..^ S ) )
52 7 oveq2d 
 |-  ( x = A -> ( L ..^ R ) = ( L ..^ T ) )
53 1 12 46 48 50 51 52 indcardi 
 |-  ( ph -> ( T e. ( L ... T ) -> th ) )
54 9 53 mpd 
 |-  ( ph -> th )