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 φAV
uzindi.b φTL
uzindi.c φRLTySL..^Rχψ
uzindi.d x=yψχ
uzindi.e x=Aψθ
uzindi.f x=yR=S
uzindi.g x=AR=T
Assertion uzindi φθ

Proof

Step Hyp Ref Expression
1 uzindi.a φAV
2 uzindi.b φTL
3 uzindi.c φRLTySL..^Rχψ
4 uzindi.d x=yψχ
5 uzindi.e x=Aψθ
6 uzindi.f x=yR=S
7 uzindi.g x=AR=T
8 eluzfz2 TLTLT
9 2 8 syl φTLT
10 fzofi L..^TFin
11 finnum L..^TFinL..^Tdomcard
12 10 11 mp1i φL..^Tdomcard
13 simpll φyL..^SL..^RSLTχRLTφ
14 simpr φyL..^SL..^RSLTχRLTRLT
15 elfzuz3 RLTTR
16 15 adantl φRLTTR
17 fzoss2 TRL..^RL..^T
18 fzossfz L..^TLT
19 17 18 sstrdi TRL..^RLT
20 16 19 syl φRLTL..^RLT
21 20 sselda φRLTSL..^RSLT
22 fzofi L..^RFin
23 elfzofz SL..^RSLR
24 23 adantl φRLTSL..^RSLR
25 elfzuz3 SLRRS
26 fzoss2 RSL..^SL..^R
27 24 25 26 3syl φRLTSL..^RL..^SL..^R
28 fzonel ¬SL..^S
29 28 jctr SL..^RSL..^R¬SL..^S
30 29 adantl φRLTSL..^RSL..^R¬SL..^S
31 ssnelpss L..^SL..^RSL..^R¬SL..^SL..^SL..^R
32 27 30 31 sylc φRLTSL..^RL..^SL..^R
33 php3 L..^RFinL..^SL..^RL..^SL..^R
34 22 32 33 sylancr φRLTSL..^RL..^SL..^R
35 id L..^SL..^RSLTχL..^SL..^RSLTχ
36 35 com13 SLTL..^SL..^RL..^SL..^RSLTχχ
37 21 34 36 sylc φRLTSL..^RL..^SL..^RSLTχχ
38 37 ex φRLTSL..^RL..^SL..^RSLTχχ
39 38 com23 φRLTL..^SL..^RSLTχSL..^Rχ
40 39 alimdv φRLTyL..^SL..^RSLTχySL..^Rχ
41 40 ex φRLTyL..^SL..^RSLTχySL..^Rχ
42 41 com23 φyL..^SL..^RSLTχRLTySL..^Rχ
43 42 imp31 φyL..^SL..^RSLTχRLTySL..^Rχ
44 13 14 43 3 syl3anc φyL..^SL..^RSLTχRLTψ
45 44 ex φyL..^SL..^RSLTχRLTψ
46 45 3adant2 φL..^RL..^TyL..^SL..^RSLTχRLTψ
47 6 eleq1d x=yRLTSLT
48 47 4 imbi12d x=yRLTψSLTχ
49 7 eleq1d x=ARLTTLT
50 49 5 imbi12d x=ARLTψTLTθ
51 6 oveq2d x=yL..^R=L..^S
52 7 oveq2d x=AL..^R=L..^T
53 1 12 46 48 50 51 52 indcardi φTLTθ
54 9 53 mpd φθ