Metamath Proof Explorer

Theorem findcard4

Description: Schema for strong induction on the cardinality of a finite set. The inductive hypothesis is that the result is true on any set with less elements. The result is then proven to be true for all finite sets. (Contributed by Thomas van Maaren, 14-Aug-2026)

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

Proof

Step Hyp Ref Expression
1 findcard4.1 
 |-  ( x = y -> ( ph <-> ch ) )
2 findcard4.2 
 |-  ( x = A -> ( ph <-> ta ) )
3 findcard4.3 
 |-  ( y e. Fin -> ( A. x ( ( # ` x ) < ( # ` y ) -> ph ) -> ch ) )
4 ficardom 
 |-  ( A e. Fin -> ( card ` A ) e. _om )
5 nnfi 
 |-  ( ( card ` A ) e. _om -> ( card ` A ) e. Fin )
6 4 5 syl 
 |-  ( A e. Fin -> ( card ` A ) e. Fin )
7 fveq2 
 |-  ( x = y -> ( card ` x ) = ( card ` y ) )
8 7 adantl 
 |-  ( ( w = z /\ x = y ) -> ( card ` x ) = ( card ` y ) )
9 simpl 
 |-  ( ( w = z /\ x = y ) -> w = z )
10 8 9 eqeq12d 
 |-  ( ( w = z /\ x = y ) -> ( ( card ` x ) = w <-> ( card ` y ) = z ) )
11 1 adantl 
 |-  ( ( w = z /\ x = y ) -> ( ph <-> ch ) )
12 10 11 imbi12d 
 |-  ( ( w = z /\ x = y ) -> ( ( ( card ` x ) = w -> ph ) <-> ( ( card ` y ) = z -> ch ) ) )
13 12 cbvaldvaw 
 |-  ( w = z -> ( A. x ( ( card ` x ) = w -> ph ) <-> A. y ( ( card ` y ) = z -> ch ) ) )
14 eqeq2 
 |-  ( w = ( card ` A ) -> ( ( card ` x ) = w <-> ( card ` x ) = ( card ` A ) ) )
15 14 imbi1d 
 |-  ( w = ( card ` A ) -> ( ( ( card ` x ) = w -> ph ) <-> ( ( card ` x ) = ( card ` A ) -> ph ) ) )
16 15 albidv 
 |-  ( w = ( card ` A ) -> ( A. x ( ( card ` x ) = w -> ph ) <-> A. x ( ( card ` x ) = ( card ` A ) -> ph ) ) )
17 eleq1 
 |-  ( ( card ` y ) = z -> ( ( card ` y ) e. Fin <-> z e. Fin ) )
18 vex 
 |-  y e. _V
19 18 cardid 
 |-  ( card ` y ) ~~ y
20 enfi 
 |-  ( ( card ` y ) ~~ y -> ( ( card ` y ) e. Fin <-> y e. Fin ) )
21 19 20 ax-mp 
 |-  ( ( card ` y ) e. Fin <-> y e. Fin )
22 17 21 bitr3di 
 |-  ( ( card ` y ) = z -> ( z e. Fin <-> y e. Fin ) )
23 22 biimpd 
 |-  ( ( card ` y ) = z -> ( z e. Fin -> y e. Fin ) )
24 psseq2 
 |-  ( ( card ` y ) = z -> ( w C. ( card ` y ) <-> w C. z ) )
25 24 bicomd 
 |-  ( ( card ` y ) = z -> ( w C. z <-> w C. ( card ` y ) ) )
26 25 imbi1d 
 |-  ( ( card ` y ) = z -> ( ( w C. z -> A. x ( ( card ` x ) = w -> ph ) ) <-> ( w C. ( card ` y ) -> A. x ( ( card ` x ) = w -> ph ) ) ) )
27 sp 
 |-  ( A. x w C. ( card ` y ) -> w C. ( card ` y ) )
28 27 imim1i 
 |-  ( ( w C. ( card ` y ) -> A. x ( ( card ` x ) = w -> ph ) ) -> ( A. x w C. ( card ` y ) -> A. x ( ( card ` x ) = w -> ph ) ) )
29 axi5r 
 |-  ( ( A. x w C. ( card ` y ) -> A. x ( ( card ` x ) = w -> ph ) ) -> A. x ( A. x w C. ( card ` y ) -> ( ( card ` x ) = w -> ph ) ) )
30 ax-5 
 |-  ( w C. ( card ` y ) -> A. x w C. ( card ` y ) )
31 30 imim1i 
 |-  ( ( A. x w C. ( card ` y ) -> ( ( card ` x ) = w -> ph ) ) -> ( w C. ( card ` y ) -> ( ( card ` x ) = w -> ph ) ) )
32 eqcom 
 |-  ( w = ( card ` x ) <-> ( card ` x ) = w )
33 pm2.04 
 |-  ( ( w C. ( card ` y ) -> ( ( card ` x ) = w -> ph ) ) -> ( ( card ` x ) = w -> ( w C. ( card ` y ) -> ph ) ) )
34 32 33 biimtrid 
 |-  ( ( w C. ( card ` y ) -> ( ( card ` x ) = w -> ph ) ) -> ( w = ( card ` x ) -> ( w C. ( card ` y ) -> ph ) ) )
35 31 34 syl 
 |-  ( ( A. x w C. ( card ` y ) -> ( ( card ` x ) = w -> ph ) ) -> ( w = ( card ` x ) -> ( w C. ( card ` y ) -> ph ) ) )
36 35 alimi 
 |-  ( A. x ( A. x w C. ( card ` y ) -> ( ( card ` x ) = w -> ph ) ) -> A. x ( w = ( card ` x ) -> ( w C. ( card ` y ) -> ph ) ) )
37 28 29 36 3syl 
 |-  ( ( w C. ( card ` y ) -> A. x ( ( card ` x ) = w -> ph ) ) -> A. x ( w = ( card ` x ) -> ( w C. ( card ` y ) -> ph ) ) )
38 26 37 biimtrdi 
 |-  ( ( card ` y ) = z -> ( ( w C. z -> A. x ( ( card ` x ) = w -> ph ) ) -> A. x ( w = ( card ` x ) -> ( w C. ( card ` y ) -> ph ) ) ) )
39 38 alimdv 
 |-  ( ( card ` y ) = z -> ( A. w ( w C. z -> A. x ( ( card ` x ) = w -> ph ) ) -> A. w A. x ( w = ( card ` x ) -> ( w C. ( card ` y ) -> ph ) ) ) )
40 ax-11 
 |-  ( A. w A. x ( w = ( card ` x ) -> ( w C. ( card ` y ) -> ph ) ) -> A. x A. w ( w = ( card ` x ) -> ( w C. ( card ` y ) -> ph ) ) )
41 40 a1i 
 |-  ( ( card ` y ) = z -> ( A. w A. x ( w = ( card ` x ) -> ( w C. ( card ` y ) -> ph ) ) -> A. x A. w ( w = ( card ` x ) -> ( w C. ( card ` y ) -> ph ) ) ) )
42 nfvd 
 |-  ( ( card ` y ) = z -> F/ w ( ( card ` x ) C. ( card ` y ) -> ph ) )
43 psseq1 
 |-  ( w = ( card ` x ) -> ( w C. ( card ` y ) <-> ( card ` x ) C. ( card ` y ) ) )
44 43 imbi1d 
 |-  ( w = ( card ` x ) -> ( ( w C. ( card ` y ) -> ph ) <-> ( ( card ` x ) C. ( card ` y ) -> ph ) ) )
45 44 a1i 
 |-  ( ( card ` y ) = z -> ( w = ( card ` x ) -> ( ( w C. ( card ` y ) -> ph ) <-> ( ( card ` x ) C. ( card ` y ) -> ph ) ) ) )
46 45 alrimiv 
 |-  ( ( card ` y ) = z -> A. w ( w = ( card ` x ) -> ( ( w C. ( card ` y ) -> ph ) <-> ( ( card ` x ) C. ( card ` y ) -> ph ) ) ) )
47 fvexd 
 |-  ( ( card ` y ) = z -> ( card ` x ) e. _V )
48 ceqsalt 
 |-  ( ( F/ w ( ( card ` x ) C. ( card ` y ) -> ph ) /\ A. w ( w = ( card ` x ) -> ( ( w C. ( card ` y ) -> ph ) <-> ( ( card ` x ) C. ( card ` y ) -> ph ) ) ) /\ ( card ` x ) e. _V ) -> ( A. w ( w = ( card ` x ) -> ( w C. ( card ` y ) -> ph ) ) <-> ( ( card ` x ) C. ( card ` y ) -> ph ) ) )
49 48 biimpd 
 |-  ( ( F/ w ( ( card ` x ) C. ( card ` y ) -> ph ) /\ A. w ( w = ( card ` x ) -> ( ( w C. ( card ` y ) -> ph ) <-> ( ( card ` x ) C. ( card ` y ) -> ph ) ) ) /\ ( card ` x ) e. _V ) -> ( A. w ( w = ( card ` x ) -> ( w C. ( card ` y ) -> ph ) ) -> ( ( card ` x ) C. ( card ` y ) -> ph ) ) )
50 42 46 47 49 syl3anc 
 |-  ( ( card ` y ) = z -> ( A. w ( w = ( card ` x ) -> ( w C. ( card ` y ) -> ph ) ) -> ( ( card ` x ) C. ( card ` y ) -> ph ) ) )
51 50 alimdv 
 |-  ( ( card ` y ) = z -> ( A. x A. w ( w = ( card ` x ) -> ( w C. ( card ` y ) -> ph ) ) -> A. x ( ( card ` x ) C. ( card ` y ) -> ph ) ) )
52 39 41 51 3syld 
 |-  ( ( card ` y ) = z -> ( A. w ( w C. z -> A. x ( ( card ` x ) = w -> ph ) ) -> A. x ( ( card ` x ) C. ( card ` y ) -> ph ) ) )
53 hashxnn0 
 |-  ( x e. _V -> ( # ` x ) e. NN0* )
54 53 elv 
 |-  ( # ` x ) e. NN0*
55 hashcl 
 |-  ( y e. Fin -> ( # ` y ) e. NN0 )
56 hashxrcl 
 |-  ( x e. _V -> ( # ` x ) e. RR* )
57 56 elv 
 |-  ( # ` x ) e. RR*
58 hashxrcl 
 |-  ( y e. _V -> ( # ` y ) e. RR* )
59 58 elv 
 |-  ( # ` y ) e. RR*
60 xrltle 
 |-  ( ( ( # ` x ) e. RR* /\ ( # ` y ) e. RR* ) -> ( ( # ` x ) < ( # ` y ) -> ( # ` x ) <_ ( # ` y ) ) )
61 57 59 60 mp2an 
 |-  ( ( # ` x ) < ( # ` y ) -> ( # ` x ) <_ ( # ` y ) )
62 xnn0lenn0nn0 
 |-  ( ( ( # ` x ) e. NN0* /\ ( # ` y ) e. NN0 /\ ( # ` x ) <_ ( # ` y ) ) -> ( # ` x ) e. NN0 )
63 54 55 61 62 mp3an3an 
 |-  ( ( y e. Fin /\ ( # ` x ) < ( # ` y ) ) -> ( # ` x ) e. NN0 )
64 hashclb 
 |-  ( x e. _V -> ( x e. Fin <-> ( # ` x ) e. NN0 ) )
65 64 elv 
 |-  ( x e. Fin <-> ( # ` x ) e. NN0 )
66 63 65 sylibr 
 |-  ( ( y e. Fin /\ ( # ` x ) < ( # ` y ) ) -> x e. Fin )
67 hashsdom 
 |-  ( ( x e. Fin /\ y e. Fin ) -> ( ( # ` x ) < ( # ` y ) <-> x ~< y ) )
68 cardsdom 
 |-  ( ( x e. _V /\ y e. _V ) -> ( ( card ` x ) e. ( card ` y ) <-> x ~< y ) )
69 68 el2v 
 |-  ( ( card ` x ) e. ( card ` y ) <-> x ~< y )
70 67 69 bitr4di 
 |-  ( ( x e. Fin /\ y e. Fin ) -> ( ( # ` x ) < ( # ` y ) <-> ( card ` x ) e. ( card ` y ) ) )
71 70 biimpd 
 |-  ( ( x e. Fin /\ y e. Fin ) -> ( ( # ` x ) < ( # ` y ) -> ( card ` x ) e. ( card ` y ) ) )
72 71 expimpd 
 |-  ( x e. Fin -> ( ( y e. Fin /\ ( # ` x ) < ( # ` y ) ) -> ( card ` x ) e. ( card ` y ) ) )
73 66 72 mpcom 
 |-  ( ( y e. Fin /\ ( # ` x ) < ( # ` y ) ) -> ( card ` x ) e. ( card ` y ) )
74 73 ex 
 |-  ( y e. Fin -> ( ( # ` x ) < ( # ` y ) -> ( card ` x ) e. ( card ` y ) ) )
75 cardon 
 |-  ( card ` x ) e. On
76 75 onordi 
 |-  Ord ( card ` x )
77 cardon 
 |-  ( card ` y ) e. On
78 77 onordi 
 |-  Ord ( card ` y )
79 ordelpss 
 |-  ( ( Ord ( card ` x ) /\ Ord ( card ` y ) ) -> ( ( card ` x ) e. ( card ` y ) <-> ( card ` x ) C. ( card ` y ) ) )
80 76 78 79 mp2an 
 |-  ( ( card ` x ) e. ( card ` y ) <-> ( card ` x ) C. ( card ` y ) )
81 74 80 imbitrdi 
 |-  ( y e. Fin -> ( ( # ` x ) < ( # ` y ) -> ( card ` x ) C. ( card ` y ) ) )
82 81 imim1d 
 |-  ( y e. Fin -> ( ( ( card ` x ) C. ( card ` y ) -> ph ) -> ( ( # ` x ) < ( # ` y ) -> ph ) ) )
83 82 alimdv 
 |-  ( y e. Fin -> ( A. x ( ( card ` x ) C. ( card ` y ) -> ph ) -> A. x ( ( # ` x ) < ( # ` y ) -> ph ) ) )
84 83 3 syld 
 |-  ( y e. Fin -> ( A. x ( ( card ` x ) C. ( card ` y ) -> ph ) -> ch ) )
85 84 imp 
 |-  ( ( y e. Fin /\ A. x ( ( card ` x ) C. ( card ` y ) -> ph ) ) -> ch )
86 85 a1i 
 |-  ( ( card ` y ) = z -> ( ( y e. Fin /\ A. x ( ( card ` x ) C. ( card ` y ) -> ph ) ) -> ch ) )
87 23 52 86 syl2and 
 |-  ( ( card ` y ) = z -> ( ( z e. Fin /\ A. w ( w C. z -> A. x ( ( card ` x ) = w -> ph ) ) ) -> ch ) )
88 87 com12 
 |-  ( ( z e. Fin /\ A. w ( w C. z -> A. x ( ( card ` x ) = w -> ph ) ) ) -> ( ( card ` y ) = z -> ch ) )
89 88 alrimiv 
 |-  ( ( z e. Fin /\ A. w ( w C. z -> A. x ( ( card ` x ) = w -> ph ) ) ) -> A. y ( ( card ` y ) = z -> ch ) )
90 89 ex 
 |-  ( z e. Fin -> ( A. w ( w C. z -> A. x ( ( card ` x ) = w -> ph ) ) -> A. y ( ( card ` y ) = z -> ch ) ) )
91 13 16 90 findcard3 
 |-  ( ( card ` A ) e. Fin -> A. x ( ( card ` x ) = ( card ` A ) -> ph ) )
92 fveq2 
 |-  ( x = A -> ( card ` x ) = ( card ` A ) )
93 92 imim1i 
 |-  ( ( ( card ` x ) = ( card ` A ) -> ph ) -> ( x = A -> ph ) )
94 93 alimi 
 |-  ( A. x ( ( card ` x ) = ( card ` A ) -> ph ) -> A. x ( x = A -> ph ) )
95 6 91 94 3syl 
 |-  ( A e. Fin -> A. x ( x = A -> ph ) )
96 nfvd 
 |-  ( A e. Fin -> F/ x ta )
97 2 ax-gen 
 |-  A. x ( x = A -> ( ph <-> ta ) )
98 97 a1i 
 |-  ( A e. Fin -> A. x ( x = A -> ( ph <-> ta ) ) )
99 id 
 |-  ( A e. Fin -> A e. Fin )
100 ceqsalt 
 |-  ( ( F/ x ta /\ A. x ( x = A -> ( ph <-> ta ) ) /\ A e. Fin ) -> ( A. x ( x = A -> ph ) <-> ta ) )
101 96 98 99 100 syl3anc 
 |-  ( A e. Fin -> ( A. x ( x = A -> ph ) <-> ta ) )
102 95 101 mpbid 
 |-  ( A e. Fin -> ta )