Metamath Proof Explorer

Theorem indcardi

Description: Indirect strong induction on the cardinality of a finite or numerable set. (Contributed by Stefan O'Rear, 24-Aug-2015)

Ref Expression
Hypotheses indcardi.a 
|- ( ph -> A e. V )
indcardi.b 
|- ( ph -> T e. dom card )
indcardi.c 
|- ( ( ph /\ R ~<_ T /\ A. y ( S ~< R -> ch ) ) -> ps )
indcardi.d 
|- ( x = y -> ( ps <-> ch ) )
indcardi.e 
|- ( x = A -> ( ps <-> th ) )
indcardi.f 
|- ( x = y -> R = S )
indcardi.g 
|- ( x = A -> R = T )
Assertion indcardi 
|- ( ph -> th )

Proof

Step Hyp Ref Expression
1 indcardi.a 
 |-  ( ph -> A e. V )
2 indcardi.b 
 |-  ( ph -> T e. dom card )
3 indcardi.c 
 |-  ( ( ph /\ R ~<_ T /\ A. y ( S ~< R -> ch ) ) -> ps )
4 indcardi.d 
 |-  ( x = y -> ( ps <-> ch ) )
5 indcardi.e 
 |-  ( x = A -> ( ps <-> th ) )
6 indcardi.f 
 |-  ( x = y -> R = S )
7 indcardi.g 
 |-  ( x = A -> R = T )
8 domrefg 
 |-  ( T e. dom card -> T ~<_ T )
9 2 8 syl 
 |-  ( ph -> T ~<_ T )
10 cardon 
 |-  ( card ` T ) e. On
11 10 a1i 
 |-  ( ph -> ( card ` T ) e. On )
12 simpl1 
 |-  ( ( ( ph /\ ( ( card ` R ) e. On /\ ( card ` R ) C_ ( card ` T ) ) /\ A. y ( ( card ` S ) e. ( card ` R ) -> ( S ~<_ T -> ch ) ) ) /\ R ~<_ T ) -> ph )
13 simpr 
 |-  ( ( ( ph /\ ( ( card ` R ) e. On /\ ( card ` R ) C_ ( card ` T ) ) /\ A. y ( ( card ` S ) e. ( card ` R ) -> ( S ~<_ T -> ch ) ) ) /\ R ~<_ T ) -> R ~<_ T )
14 simpr 
 |-  ( ( ( ph /\ ( ( card ` R ) e. On /\ ( card ` R ) C_ ( card ` T ) ) /\ R ~<_ T ) /\ S ~< R ) -> S ~< R )
15 simpl1 
 |-  ( ( ( ph /\ ( ( card ` R ) e. On /\ ( card ` R ) C_ ( card ` T ) ) /\ R ~<_ T ) /\ S ~< R ) -> ph )
16 15 2 syl 
 |-  ( ( ( ph /\ ( ( card ` R ) e. On /\ ( card ` R ) C_ ( card ` T ) ) /\ R ~<_ T ) /\ S ~< R ) -> T e. dom card )
17 sdomdom 
 |-  ( S ~< R -> S ~<_ R )
18 simpl3 
 |-  ( ( ( ph /\ ( ( card ` R ) e. On /\ ( card ` R ) C_ ( card ` T ) ) /\ R ~<_ T ) /\ S ~< R ) -> R ~<_ T )
19 domtr 
 |-  ( ( S ~<_ R /\ R ~<_ T ) -> S ~<_ T )
20 17 18 19 syl2an2 
 |-  ( ( ( ph /\ ( ( card ` R ) e. On /\ ( card ` R ) C_ ( card ` T ) ) /\ R ~<_ T ) /\ S ~< R ) -> S ~<_ T )
21 numdom 
 |-  ( ( T e. dom card /\ S ~<_ T ) -> S e. dom card )
22 16 20 21 syl2anc 
 |-  ( ( ( ph /\ ( ( card ` R ) e. On /\ ( card ` R ) C_ ( card ` T ) ) /\ R ~<_ T ) /\ S ~< R ) -> S e. dom card )
23 numdom 
 |-  ( ( T e. dom card /\ R ~<_ T ) -> R e. dom card )
24 16 18 23 syl2anc 
 |-  ( ( ( ph /\ ( ( card ` R ) e. On /\ ( card ` R ) C_ ( card ` T ) ) /\ R ~<_ T ) /\ S ~< R ) -> R e. dom card )
25 cardsdom2 
 |-  ( ( S e. dom card /\ R e. dom card ) -> ( ( card ` S ) e. ( card ` R ) <-> S ~< R ) )
26 22 24 25 syl2anc 
 |-  ( ( ( ph /\ ( ( card ` R ) e. On /\ ( card ` R ) C_ ( card ` T ) ) /\ R ~<_ T ) /\ S ~< R ) -> ( ( card ` S ) e. ( card ` R ) <-> S ~< R ) )
27 14 26 mpbird 
 |-  ( ( ( ph /\ ( ( card ` R ) e. On /\ ( card ` R ) C_ ( card ` T ) ) /\ R ~<_ T ) /\ S ~< R ) -> ( card ` S ) e. ( card ` R ) )
28 id 
 |-  ( ( ( card ` S ) e. ( card ` R ) -> ( S ~<_ T -> ch ) ) -> ( ( card ` S ) e. ( card ` R ) -> ( S ~<_ T -> ch ) ) )
29 28 com3l 
 |-  ( ( card ` S ) e. ( card ` R ) -> ( S ~<_ T -> ( ( ( card ` S ) e. ( card ` R ) -> ( S ~<_ T -> ch ) ) -> ch ) ) )
30 27 20 29 sylc 
 |-  ( ( ( ph /\ ( ( card ` R ) e. On /\ ( card ` R ) C_ ( card ` T ) ) /\ R ~<_ T ) /\ S ~< R ) -> ( ( ( card ` S ) e. ( card ` R ) -> ( S ~<_ T -> ch ) ) -> ch ) )
31 30 ex 
 |-  ( ( ph /\ ( ( card ` R ) e. On /\ ( card ` R ) C_ ( card ` T ) ) /\ R ~<_ T ) -> ( S ~< R -> ( ( ( card ` S ) e. ( card ` R ) -> ( S ~<_ T -> ch ) ) -> ch ) ) )
32 31 com23 
 |-  ( ( ph /\ ( ( card ` R ) e. On /\ ( card ` R ) C_ ( card ` T ) ) /\ R ~<_ T ) -> ( ( ( card ` S ) e. ( card ` R ) -> ( S ~<_ T -> ch ) ) -> ( S ~< R -> ch ) ) )
33 32 alimdv 
 |-  ( ( ph /\ ( ( card ` R ) e. On /\ ( card ` R ) C_ ( card ` T ) ) /\ R ~<_ T ) -> ( A. y ( ( card ` S ) e. ( card ` R ) -> ( S ~<_ T -> ch ) ) -> A. y ( S ~< R -> ch ) ) )
34 33 3exp 
 |-  ( ph -> ( ( ( card ` R ) e. On /\ ( card ` R ) C_ ( card ` T ) ) -> ( R ~<_ T -> ( A. y ( ( card ` S ) e. ( card ` R ) -> ( S ~<_ T -> ch ) ) -> A. y ( S ~< R -> ch ) ) ) ) )
35 34 com34 
 |-  ( ph -> ( ( ( card ` R ) e. On /\ ( card ` R ) C_ ( card ` T ) ) -> ( A. y ( ( card ` S ) e. ( card ` R ) -> ( S ~<_ T -> ch ) ) -> ( R ~<_ T -> A. y ( S ~< R -> ch ) ) ) ) )
36 35 3imp1 
 |-  ( ( ( ph /\ ( ( card ` R ) e. On /\ ( card ` R ) C_ ( card ` T ) ) /\ A. y ( ( card ` S ) e. ( card ` R ) -> ( S ~<_ T -> ch ) ) ) /\ R ~<_ T ) -> A. y ( S ~< R -> ch ) )
37 12 13 36 3 syl3anc 
 |-  ( ( ( ph /\ ( ( card ` R ) e. On /\ ( card ` R ) C_ ( card ` T ) ) /\ A. y ( ( card ` S ) e. ( card ` R ) -> ( S ~<_ T -> ch ) ) ) /\ R ~<_ T ) -> ps )
38 37 ex 
 |-  ( ( ph /\ ( ( card ` R ) e. On /\ ( card ` R ) C_ ( card ` T ) ) /\ A. y ( ( card ` S ) e. ( card ` R ) -> ( S ~<_ T -> ch ) ) ) -> ( R ~<_ T -> ps ) )
39 6 breq1d 
 |-  ( x = y -> ( R ~<_ T <-> S ~<_ T ) )
40 39 4 imbi12d 
 |-  ( x = y -> ( ( R ~<_ T -> ps ) <-> ( S ~<_ T -> ch ) ) )
41 7 breq1d 
 |-  ( x = A -> ( R ~<_ T <-> T ~<_ T ) )
42 41 5 imbi12d 
 |-  ( x = A -> ( ( R ~<_ T -> ps ) <-> ( T ~<_ T -> th ) ) )
43 6 fveq2d 
 |-  ( x = y -> ( card ` R ) = ( card ` S ) )
44 7 fveq2d 
 |-  ( x = A -> ( card ` R ) = ( card ` T ) )
45 1 11 38 40 42 43 44 tfisi 
 |-  ( ph -> ( T ~<_ T -> th ) )
46 9 45 mpd 
 |-  ( ph -> th )