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 → φ ↔ χ
findcard4.2 ⊢ x = A → φ ↔ τ
findcard4.3 ⊢ y ∈ Fin → ∀ x x < y → φ → χ
Assertion findcard4 ⊢ A ∈ Fin → τ

Proof

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