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) Avoid ax-pow . (Revised by BTernaryTau, 7-Jan-2025)

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 simprl 
 |-  ( ( ( ( w e. _om /\ y ~~ w ) /\ x C. y ) /\ ( z e. _om /\ x ~~ z ) ) -> z e. _om )
24 nnfi 
 |-  ( z e. _om -> z e. Fin )
25 ensymfib 
 |-  ( z e. Fin -> ( z ~~ x <-> x ~~ z ) )
26 24 25 syl 
 |-  ( z e. _om -> ( z ~~ x <-> x ~~ z ) )
27 26 biimpar 
 |-  ( ( z e. _om /\ x ~~ z ) -> z ~~ x )
28 27 adantl 
 |-  ( ( ( ( w e. _om /\ y ~~ w ) /\ x C. y ) /\ ( z e. _om /\ x ~~ z ) ) -> z ~~ x )
29 simplll 
 |-  ( ( ( ( w e. _om /\ y ~~ w ) /\ x C. y ) /\ ( z e. _om /\ x ~~ z ) ) -> w e. _om )
30 php3 
 |-  ( ( y e. Fin /\ x C. y ) -> x ~< y )
31 13 30 sylan 
 |-  ( ( ( w e. _om /\ y ~~ w ) /\ x C. y ) -> x ~< y )
32 31 adantr 
 |-  ( ( ( ( w e. _om /\ y ~~ w ) /\ x C. y ) /\ ( z e. _om /\ x ~~ z ) ) -> x ~< y )
33 simpllr 
 |-  ( ( ( ( w e. _om /\ y ~~ w ) /\ x C. y ) /\ ( z e. _om /\ x ~~ z ) ) -> y ~~ w )
34 endom 
 |-  ( y ~~ w -> y ~<_ w )
35 nnfi 
 |-  ( w e. _om -> w e. Fin )
36 domfi 
 |-  ( ( w e. Fin /\ y ~<_ w ) -> y e. Fin )
37 35 36 sylan 
 |-  ( ( w e. _om /\ y ~<_ w ) -> y e. Fin )
38 37 3adant2 
 |-  ( ( w e. _om /\ x ~< y /\ y ~<_ w ) -> y e. Fin )
39 sdomdom 
 |-  ( x ~< y -> x ~<_ y )
40 domfi 
 |-  ( ( y e. Fin /\ x ~<_ y ) -> x e. Fin )
41 39 40 sylan2 
 |-  ( ( y e. Fin /\ x ~< y ) -> x e. Fin )
42 41 3adant3 
 |-  ( ( y e. Fin /\ x ~< y /\ y ~<_ w ) -> x e. Fin )
43 38 42 syld3an1 
 |-  ( ( w e. _om /\ x ~< y /\ y ~<_ w ) -> x e. Fin )
44 sdomdomtrfi 
 |-  ( ( x e. Fin /\ x ~< y /\ y ~<_ w ) -> x ~< w )
45 43 44 syld3an1 
 |-  ( ( w e. _om /\ x ~< y /\ y ~<_ w ) -> x ~< w )
46 34 45 syl3an3 
 |-  ( ( w e. _om /\ x ~< y /\ y ~~ w ) -> x ~< w )
47 29 32 33 46 syl3anc 
 |-  ( ( ( ( w e. _om /\ y ~~ w ) /\ x C. y ) /\ ( z e. _om /\ x ~~ z ) ) -> x ~< w )
48 endom 
 |-  ( z ~~ x -> z ~<_ x )
49 domsdomtrfi 
 |-  ( ( z e. Fin /\ z ~<_ x /\ x ~< w ) -> z ~< w )
50 24 49 syl3an1 
 |-  ( ( z e. _om /\ z ~<_ x /\ x ~< w ) -> z ~< w )
51 48 50 syl3an2 
 |-  ( ( z e. _om /\ z ~~ x /\ x ~< w ) -> z ~< w )
52 23 28 47 51 syl3anc 
 |-  ( ( ( ( w e. _om /\ y ~~ w ) /\ x C. y ) /\ ( z e. _om /\ x ~~ z ) ) -> z ~< w )
53 nnsdomo 
 |-  ( ( z e. _om /\ w e. _om ) -> ( z ~< w <-> z C. w ) )
54 nnord 
 |-  ( z e. _om -> Ord z )
55 nnord 
 |-  ( w e. _om -> Ord w )
56 ordelpss 
 |-  ( ( Ord z /\ Ord w ) -> ( z e. w <-> z C. w ) )
57 54 55 56 syl2an 
 |-  ( ( z e. _om /\ w e. _om ) -> ( z e. w <-> z C. w ) )
58 53 57 bitr4d 
 |-  ( ( z e. _om /\ w e. _om ) -> ( z ~< w <-> z e. w ) )
59 23 29 58 syl2anc 
 |-  ( ( ( ( w e. _om /\ y ~~ w ) /\ x C. y ) /\ ( z e. _om /\ x ~~ z ) ) -> ( z ~< w <-> z e. w ) )
60 52 59 mpbid 
 |-  ( ( ( ( w e. _om /\ y ~~ w ) /\ x C. y ) /\ ( z e. _om /\ x ~~ z ) ) -> z e. w )
61 60 ex 
 |-  ( ( ( w e. _om /\ y ~~ w ) /\ x C. y ) -> ( ( z e. _om /\ x ~~ z ) -> z e. w ) )
62 simpr 
 |-  ( ( z e. _om /\ x ~~ z ) -> x ~~ z )
63 61 62 jca2 
 |-  ( ( ( w e. _om /\ y ~~ w ) /\ x C. y ) -> ( ( z e. _om /\ x ~~ z ) -> ( z e. w /\ x ~~ z ) ) )
64 63 reximdv2 
 |-  ( ( ( w e. _om /\ y ~~ w ) /\ x C. y ) -> ( E. z e. _om x ~~ z -> E. z e. w x ~~ z ) )
65 22 64 mpd 
 |-  ( ( ( w e. _om /\ y ~~ w ) /\ x C. y ) -> E. z e. w x ~~ z )
66 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 ) )
67 66 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 ) ) )
68 65 67 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 ) ) )
69 ordom 
 |-  Ord _om
70 ordelss 
 |-  ( ( Ord _om /\ w e. _om ) -> w C_ _om )
71 69 70 mpan 
 |-  ( w e. _om -> w C_ _om )
72 71 ad2antrr 
 |-  ( ( ( w e. _om /\ y ~~ w ) /\ x C. y ) -> w C_ _om )
73 72 sseld 
 |-  ( ( ( w e. _om /\ y ~~ w ) /\ x C. y ) -> ( z e. w -> z e. _om ) )
74 pm2.27 
 |-  ( z e. _om -> ( ( z e. _om -> ( x ~~ z -> ph ) ) -> ( x ~~ z -> ph ) ) )
75 74 impd 
 |-  ( z e. _om -> ( ( ( z e. _om -> ( x ~~ z -> ph ) ) /\ x ~~ z ) -> ph ) )
76 73 75 syl6 
 |-  ( ( ( w e. _om /\ y ~~ w ) /\ x C. y ) -> ( z e. w -> ( ( ( z e. _om -> ( x ~~ z -> ph ) ) /\ x ~~ z ) -> ph ) ) )
77 76 rexlimdv 
 |-  ( ( ( w e. _om /\ y ~~ w ) /\ x C. y ) -> ( E. z e. w ( ( z e. _om -> ( x ~~ z -> ph ) ) /\ x ~~ z ) -> ph ) )
78 68 77 syld 
 |-  ( ( ( w e. _om /\ y ~~ w ) /\ x C. y ) -> ( A. z e. w ( z e. _om -> ( x ~~ z -> ph ) ) -> ph ) )
79 78 ex 
 |-  ( ( w e. _om /\ y ~~ w ) -> ( x C. y -> ( A. z e. w ( z e. _om -> ( x ~~ z -> ph ) ) -> ph ) ) )
80 79 com23 
 |-  ( ( w e. _om /\ y ~~ w ) -> ( A. z e. w ( z e. _om -> ( x ~~ z -> ph ) ) -> ( x C. y -> ph ) ) )
81 80 alimdv 
 |-  ( ( w e. _om /\ y ~~ w ) -> ( A. x A. z e. w ( z e. _om -> ( x ~~ z -> ph ) ) -> A. x ( x C. y -> ph ) ) )
82 17 81 biimtrid 
 |-  ( ( w e. _om /\ y ~~ w ) -> ( A. z e. w ( z e. _om -> A. x ( x ~~ z -> ph ) ) -> A. x ( x C. y -> ph ) ) )
83 13 82 3 sylsyld 
 |-  ( ( w e. _om /\ y ~~ w ) -> ( A. z e. w ( z e. _om -> A. x ( x ~~ z -> ph ) ) -> ch ) )
84 83 impancom 
 |-  ( ( w e. _om /\ A. z e. w ( z e. _om -> A. x ( x ~~ z -> ph ) ) ) -> ( y ~~ w -> ch ) )
85 84 alrimiv 
 |-  ( ( w e. _om /\ A. z e. w ( z e. _om -> A. x ( x ~~ z -> ph ) ) ) -> A. y ( y ~~ w -> ch ) )
86 85 expcom 
 |-  ( A. z e. w ( z e. _om -> A. x ( x ~~ z -> ph ) ) -> ( w e. _om -> A. y ( y ~~ w -> ch ) ) )
87 breq1 
 |-  ( x = y -> ( x ~~ w <-> y ~~ w ) )
88 87 1 imbi12d 
 |-  ( x = y -> ( ( x ~~ w -> ph ) <-> ( y ~~ w -> ch ) ) )
89 88 cbvalvw 
 |-  ( A. x ( x ~~ w -> ph ) <-> A. y ( y ~~ w -> ch ) )
90 86 89 imbitrrdi 
 |-  ( A. z e. w ( z e. _om -> A. x ( x ~~ z -> ph ) ) -> ( w e. _om -> A. x ( x ~~ w -> ph ) ) )
91 90 a1i 
 |-  ( w e. On -> ( A. z e. w ( z e. _om -> A. x ( x ~~ z -> ph ) ) -> ( w e. _om -> A. x ( x ~~ w -> ph ) ) ) )
92 10 91 tfis2 
 |-  ( w e. On -> ( w e. _om -> A. x ( x ~~ w -> ph ) ) )
93 5 92 mpcom 
 |-  ( w e. _om -> A. x ( x ~~ w -> ph ) )
94 93 rgen 
 |-  A. w e. _om A. x ( x ~~ w -> ph )
95 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 ) )
96 94 95 mpan 
 |-  ( E. w e. _om A ~~ w -> E. w e. _om ( A. x ( x ~~ w -> ph ) /\ A ~~ w ) )
97 4 96 sylbi 
 |-  ( A e. Fin -> E. w e. _om ( A. x ( x ~~ w -> ph ) /\ A ~~ w ) )
98 breq1 
 |-  ( x = A -> ( x ~~ w <-> A ~~ w ) )
99 98 2 imbi12d 
 |-  ( x = A -> ( ( x ~~ w -> ph ) <-> ( A ~~ w -> ta ) ) )
100 99 spcgv 
 |-  ( A e. Fin -> ( A. x ( x ~~ w -> ph ) -> ( A ~~ w -> ta ) ) )
101 100 impd 
 |-  ( A e. Fin -> ( ( A. x ( x ~~ w -> ph ) /\ A ~~ w ) -> ta ) )
102 101 rexlimdvw 
 |-  ( A e. Fin -> ( E. w e. _om ( A. x ( x ~~ w -> ph ) /\ A ~~ w ) -> ta ) )
103 97 102 mpd 
 |-  ( A e. Fin -> ta )