Metamath Proof Explorer

Theorem findcard3

Description: Schema for strong induction on the cardinality of a finite set. The inductive hypothesis is that the result is true on any proper subset. The result is then proven to be true for all finite sets. (Contributed by Mario Carneiro, 13-Dec-2013)

Ref Expression
Hypotheses findcard3.1 
|- ( x = y -> ( ph <-> ch ) )
findcard3.2 
|- ( x = A -> ( ph <-> ta ) )
findcard3.3 
|- ( y e. Fin -> ( A. x ( x C. y -> ph ) -> ch ) )
Assertion findcard3 
|- ( A e. Fin -> ta )

Proof

Step Hyp Ref Expression
1 findcard3.1 
 |-  ( x = y -> ( ph <-> ch ) )
2 findcard3.2 
 |-  ( x = A -> ( ph <-> ta ) )
3 findcard3.3 
 |-  ( y e. Fin -> ( A. x ( x C. y -> ph ) -> ch ) )
4 isfi 
 |-  ( A e. Fin <-> E. w e. _om A ~~ w )
5 nnon 
 |-  ( w e. _om -> w e. On )
6 eleq1w 
 |-  ( w = z -> ( w e. _om <-> z e. _om ) )
7 breq2 
 |-  ( w = z -> ( x ~~ w <-> x ~~ z ) )
8 7 imbi1d 
 |-  ( w = z -> ( ( x ~~ w -> ph ) <-> ( x ~~ z -> ph ) ) )
9 8 albidv 
 |-  ( w = z -> ( A. x ( x ~~ w -> ph ) <-> A. x ( x ~~ z -> ph ) ) )
10 6 9 imbi12d 
 |-  ( w = z -> ( ( w e. _om -> A. x ( x ~~ w -> ph ) ) <-> ( z e. _om -> A. x ( x ~~ z -> ph ) ) ) )
11 rspe 
 |-  ( ( w e. _om /\ y ~~ w ) -> E. w e. _om y ~~ w )
12 isfi 
 |-  ( y e. Fin <-> E. w e. _om y ~~ w )
13 11 12 sylibr 
 |-  ( ( w e. _om /\ y ~~ w ) -> y e. Fin )
14 19.21v 
 |-  ( A. x ( z e. _om -> ( x ~~ z -> ph ) ) <-> ( z e. _om -> A. x ( x ~~ z -> ph ) ) )
15 14 ralbii 
 |-  ( A. z e. w A. x ( z e. _om -> ( x ~~ z -> ph ) ) <-> A. z e. w ( z e. _om -> A. x ( x ~~ z -> ph ) ) )
16 ralcom4 
 |-  ( A. z e. w A. x ( z e. _om -> ( x ~~ z -> ph ) ) <-> A. x A. z e. w ( z e. _om -> ( x ~~ z -> ph ) ) )
17 15 16 bitr3i 
 |-  ( A. z e. w ( z e. _om -> A. x ( x ~~ z -> ph ) ) <-> A. x A. z e. w ( z e. _om -> ( x ~~ z -> ph ) ) )
18 pssss 
 |-  ( x C. y -> x C_ y )
19 ssfi 
 |-  ( ( y e. Fin /\ x C_ y ) -> x e. Fin )
20 isfi 
 |-  ( x e. Fin <-> E. z e. _om x ~~ z )
21 19 20 sylib 
 |-  ( ( y e. Fin /\ x C_ y ) -> E. z e. _om x ~~ z )
22 13 18 21 syl2an 
 |-  ( ( ( w e. _om /\ y ~~ w ) /\ x C. y ) -> E. z e. _om x ~~ z )
23 ensym 
 |-  ( x ~~ z -> z ~~ x )
24 23 ad2antll 
 |-  ( ( ( ( w e. _om /\ y ~~ w ) /\ x C. y ) /\ ( z e. _om /\ x ~~ z ) ) -> z ~~ x )
25 php3 
 |-  ( ( y e. Fin /\ x C. y ) -> x ~< y )
26 13 25 sylan 
 |-  ( ( ( w e. _om /\ y ~~ w ) /\ x C. y ) -> x ~< y )
27 simpllr 
 |-  ( ( ( ( w e. _om /\ y ~~ w ) /\ x C. y ) /\ ( z e. _om /\ x ~~ z ) ) -> y ~~ w )
28 sdomentr 
 |-  ( ( x ~< y /\ y ~~ w ) -> x ~< w )
29 26 27 28 syl2an2r 
 |-  ( ( ( ( w e. _om /\ y ~~ w ) /\ x C. y ) /\ ( z e. _om /\ x ~~ z ) ) -> x ~< w )
30 ensdomtr 
 |-  ( ( z ~~ x /\ x ~< w ) -> z ~< w )
31 24 29 30 syl2anc 
 |-  ( ( ( ( w e. _om /\ y ~~ w ) /\ x C. y ) /\ ( z e. _om /\ x ~~ z ) ) -> z ~< w )
32 nnon 
 |-  ( z e. _om -> z e. On )
33 32 ad2antrl 
 |-  ( ( ( ( w e. _om /\ y ~~ w ) /\ x C. y ) /\ ( z e. _om /\ x ~~ z ) ) -> z e. On )
34 5 ad3antrrr 
 |-  ( ( ( ( w e. _om /\ y ~~ w ) /\ x C. y ) /\ ( z e. _om /\ x ~~ z ) ) -> w e. On )
35 sdomel 
 |-  ( ( z e. On /\ w e. On ) -> ( z ~< w -> z e. w ) )
36 33 34 35 syl2anc 
 |-  ( ( ( ( w e. _om /\ y ~~ w ) /\ x C. y ) /\ ( z e. _om /\ x ~~ z ) ) -> ( z ~< w -> z e. w ) )
37 31 36 mpd 
 |-  ( ( ( ( w e. _om /\ y ~~ w ) /\ x C. y ) /\ ( z e. _om /\ x ~~ z ) ) -> z e. w )
38 37 ex 
 |-  ( ( ( w e. _om /\ y ~~ w ) /\ x C. y ) -> ( ( z e. _om /\ x ~~ z ) -> z e. w ) )
39 simpr 
 |-  ( ( z e. _om /\ x ~~ z ) -> x ~~ z )
40 38 39 jca2 
 |-  ( ( ( w e. _om /\ y ~~ w ) /\ x C. y ) -> ( ( z e. _om /\ x ~~ z ) -> ( z e. w /\ x ~~ z ) ) )
41 40 reximdv2 
 |-  ( ( ( w e. _om /\ y ~~ w ) /\ x C. y ) -> ( E. z e. _om x ~~ z -> E. z e. w x ~~ z ) )
42 22 41 mpd 
 |-  ( ( ( w e. _om /\ y ~~ w ) /\ x C. y ) -> E. z e. w x ~~ z )
43 r19.29 
 |-  ( ( A. z e. w ( z e. _om -> ( x ~~ z -> ph ) ) /\ E. z e. w x ~~ z ) -> E. z e. w ( ( z e. _om -> ( x ~~ z -> ph ) ) /\ x ~~ z ) )
44 43 expcom 
 |-  ( E. z e. w x ~~ z -> ( A. z e. w ( z e. _om -> ( x ~~ z -> ph ) ) -> E. z e. w ( ( z e. _om -> ( x ~~ z -> ph ) ) /\ x ~~ z ) ) )
45 42 44 syl 
 |-  ( ( ( w e. _om /\ y ~~ w ) /\ x C. y ) -> ( A. z e. w ( z e. _om -> ( x ~~ z -> ph ) ) -> E. z e. w ( ( z e. _om -> ( x ~~ z -> ph ) ) /\ x ~~ z ) ) )
46 ordom 
 |-  Ord _om
47 ordelss 
 |-  ( ( Ord _om /\ w e. _om ) -> w C_ _om )
48 46 47 mpan 
 |-  ( w e. _om -> w C_ _om )
49 48 ad2antrr 
 |-  ( ( ( w e. _om /\ y ~~ w ) /\ x C. y ) -> w C_ _om )
50 49 sseld 
 |-  ( ( ( w e. _om /\ y ~~ w ) /\ x C. y ) -> ( z e. w -> z e. _om ) )
51 pm2.27 
 |-  ( z e. _om -> ( ( z e. _om -> ( x ~~ z -> ph ) ) -> ( x ~~ z -> ph ) ) )
52 51 impd 
 |-  ( z e. _om -> ( ( ( z e. _om -> ( x ~~ z -> ph ) ) /\ x ~~ z ) -> ph ) )
53 50 52 syl6 
 |-  ( ( ( w e. _om /\ y ~~ w ) /\ x C. y ) -> ( z e. w -> ( ( ( z e. _om -> ( x ~~ z -> ph ) ) /\ x ~~ z ) -> ph ) ) )
54 53 rexlimdv 
 |-  ( ( ( w e. _om /\ y ~~ w ) /\ x C. y ) -> ( E. z e. w ( ( z e. _om -> ( x ~~ z -> ph ) ) /\ x ~~ z ) -> ph ) )
55 45 54 syld 
 |-  ( ( ( w e. _om /\ y ~~ w ) /\ x C. y ) -> ( A. z e. w ( z e. _om -> ( x ~~ z -> ph ) ) -> ph ) )
56 55 ex 
 |-  ( ( w e. _om /\ y ~~ w ) -> ( x C. y -> ( A. z e. w ( z e. _om -> ( x ~~ z -> ph ) ) -> ph ) ) )
57 56 com23 
 |-  ( ( w e. _om /\ y ~~ w ) -> ( A. z e. w ( z e. _om -> ( x ~~ z -> ph ) ) -> ( x C. y -> ph ) ) )
58 57 alimdv 
 |-  ( ( w e. _om /\ y ~~ w ) -> ( A. x A. z e. w ( z e. _om -> ( x ~~ z -> ph ) ) -> A. x ( x C. y -> ph ) ) )
59 17 58 syl5bi 
 |-  ( ( w e. _om /\ y ~~ w ) -> ( A. z e. w ( z e. _om -> A. x ( x ~~ z -> ph ) ) -> A. x ( x C. y -> ph ) ) )
60 13 59 3 sylsyld 
 |-  ( ( w e. _om /\ y ~~ w ) -> ( A. z e. w ( z e. _om -> A. x ( x ~~ z -> ph ) ) -> ch ) )
61 60 impancom 
 |-  ( ( w e. _om /\ A. z e. w ( z e. _om -> A. x ( x ~~ z -> ph ) ) ) -> ( y ~~ w -> ch ) )
62 61 alrimiv 
 |-  ( ( w e. _om /\ A. z e. w ( z e. _om -> A. x ( x ~~ z -> ph ) ) ) -> A. y ( y ~~ w -> ch ) )
63 62 expcom 
 |-  ( A. z e. w ( z e. _om -> A. x ( x ~~ z -> ph ) ) -> ( w e. _om -> A. y ( y ~~ w -> ch ) ) )
64 breq1 
 |-  ( x = y -> ( x ~~ w <-> y ~~ w ) )
65 64 1 imbi12d 
 |-  ( x = y -> ( ( x ~~ w -> ph ) <-> ( y ~~ w -> ch ) ) )
66 65 cbvalvw 
 |-  ( A. x ( x ~~ w -> ph ) <-> A. y ( y ~~ w -> ch ) )
67 63 66 syl6ibr 
 |-  ( A. z e. w ( z e. _om -> A. x ( x ~~ z -> ph ) ) -> ( w e. _om -> A. x ( x ~~ w -> ph ) ) )
68 67 a1i 
 |-  ( w e. On -> ( A. z e. w ( z e. _om -> A. x ( x ~~ z -> ph ) ) -> ( w e. _om -> A. x ( x ~~ w -> ph ) ) ) )
69 10 68 tfis2 
 |-  ( w e. On -> ( w e. _om -> A. x ( x ~~ w -> ph ) ) )
70 5 69 mpcom 
 |-  ( w e. _om -> A. x ( x ~~ w -> ph ) )
71 70 rgen 
 |-  A. w e. _om A. x ( x ~~ w -> ph )
72 r19.29 
 |-  ( ( A. w e. _om A. x ( x ~~ w -> ph ) /\ E. w e. _om A ~~ w ) -> E. w e. _om ( A. x ( x ~~ w -> ph ) /\ A ~~ w ) )
73 71 72 mpan 
 |-  ( E. w e. _om A ~~ w -> E. w e. _om ( A. x ( x ~~ w -> ph ) /\ A ~~ w ) )
74 4 73 sylbi 
 |-  ( A e. Fin -> E. w e. _om ( A. x ( x ~~ w -> ph ) /\ A ~~ w ) )
75 breq1 
 |-  ( x = A -> ( x ~~ w <-> A ~~ w ) )
76 75 2 imbi12d 
 |-  ( x = A -> ( ( x ~~ w -> ph ) <-> ( A ~~ w -> ta ) ) )
77 76 spcgv 
 |-  ( A e. Fin -> ( A. x ( x ~~ w -> ph ) -> ( A ~~ w -> ta ) ) )
78 77 impd 
 |-  ( A e. Fin -> ( ( A. x ( x ~~ w -> ph ) /\ A ~~ w ) -> ta ) )
79 78 rexlimdvw 
 |-  ( A e. Fin -> ( E. w e. _om ( A. x ( x ~~ w -> ph ) /\ A ~~ w ) -> ta ) )
80 74 79 mpd 
 |-  ( A e. Fin -> ta )