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

Proof

Step Hyp Ref Expression
1 findcard3.1 ⊢x=y→φ↔χ
2 findcard3.2 ⊢x=A→φ↔τ
3 findcard3.3 ⊢y∈Fin→∀xx⊂y→φ→χ
4 isfi ⊢A∈Fin↔∃w∈ωA≈w
5 nnon ⊢w∈ω→w∈On
6 eleq1w ⊢w=z→w∈ω↔z∈ω
7 breq2 ⊢w=z→x≈w↔x≈z
8 7 imbi1d ⊢w=z→x≈w→φ↔x≈z→φ
9 8 albidv ⊢w=z→∀xx≈w→φ↔∀xx≈z→φ
10 6 9 imbi12d ⊢w=z→w∈ω→∀xx≈w→φ↔z∈ω→∀xx≈z→φ
11 rspe ⊢w∈ω∧y≈w→∃w∈ωy≈w
12 isfi ⊢y∈Fin↔∃w∈ωy≈w
13 11 12 sylibr ⊢w∈ω∧y≈w→y∈Fin
14 19.21v ⊢∀xz∈ω→x≈z→φ↔z∈ω→∀xx≈z→φ
15 14 ralbii ⊢∀z∈w∀xz∈ω→x≈z→φ↔∀z∈wz∈ω→∀xx≈z→φ
16 ralcom4 ⊢∀z∈w∀xz∈ω→x≈z→φ↔∀x∀z∈wz∈ω→x≈z→φ
17 15 16 bitr3i ⊢∀z∈wz∈ω→∀xx≈z→φ↔∀x∀z∈wz∈ω→x≈z→φ
18 pssss ⊢x⊂y→x⊆y
19 ssfi ⊢y∈Fin∧x⊆y→x∈Fin
20 isfi ⊢x∈Fin↔∃z∈ωx≈z
21 19 20 sylib ⊢y∈Fin∧x⊆y→∃z∈ωx≈z
22 13 18 21 syl2an ⊢w∈ω∧y≈w∧x⊂y→∃z∈ωx≈z
23 simprl ⊢w∈ω∧y≈w∧x⊂y∧z∈ω∧x≈z→z∈ω
24 nnfi ⊢z∈ω→z∈Fin
25 ensymfib ⊢z∈Fin→z≈x↔x≈z
26 24 25 syl ⊢z∈ω→z≈x↔x≈z
27 26 biimpar ⊢z∈ω∧x≈z→z≈x
28 27 adantl ⊢w∈ω∧y≈w∧x⊂y∧z∈ω∧x≈z→z≈x
29 simplll ⊢w∈ω∧y≈w∧x⊂y∧z∈ω∧x≈z→w∈ω
30 php3 ⊢y∈Fin∧x⊂y→x≺y
31 13 30 sylan ⊢w∈ω∧y≈w∧x⊂y→x≺y
32 31 adantr ⊢w∈ω∧y≈w∧x⊂y∧z∈ω∧x≈z→x≺y
33 simpllr ⊢w∈ω∧y≈w∧x⊂y∧z∈ω∧x≈z→y≈w
34 endom ⊢y≈w→y≼w
35 nnfi ⊢w∈ω→w∈Fin
36 domfi ⊢w∈Fin∧y≼w→y∈Fin
37 35 36 sylan ⊢w∈ω∧y≼w→y∈Fin
38 37 3adant2 ⊢w∈ω∧x≺y∧y≼w→y∈Fin
39 sdomdom ⊢x≺y→x≼y
40 domfi ⊢y∈Fin∧x≼y→x∈Fin
41 39 40 sylan2 ⊢y∈Fin∧x≺y→x∈Fin
42 41 3adant3 ⊢y∈Fin∧x≺y∧y≼w→x∈Fin
43 38 42 syld3an1 ⊢w∈ω∧x≺y∧y≼w→x∈Fin
44 sdomdomtrfi ⊢x∈Fin∧x≺y∧y≼w→x≺w
45 43 44 syld3an1 ⊢w∈ω∧x≺y∧y≼w→x≺w
46 34 45 syl3an3 ⊢w∈ω∧x≺y∧y≈w→x≺w
47 29 32 33 46 syl3anc ⊢w∈ω∧y≈w∧x⊂y∧z∈ω∧x≈z→x≺w
48 endom ⊢z≈x→z≼x
49 domsdomtrfi ⊢z∈Fin∧z≼x∧x≺w→z≺w
50 24 49 syl3an1 ⊢z∈ω∧z≼x∧x≺w→z≺w
51 48 50 syl3an2 ⊢z∈ω∧z≈x∧x≺w→z≺w
52 23 28 47 51 syl3anc ⊢w∈ω∧y≈w∧x⊂y∧z∈ω∧x≈z→z≺w
53 nnsdomo ⊢z∈ω∧w∈ω→z≺w↔z⊂w
54 nnord ⊢z∈ω→Ord⁡z
55 nnord ⊢w∈ω→Ord⁡w
56 ordelpss ⊢Ord⁡z∧Ord⁡w→z∈w↔z⊂w
57 54 55 56 syl2an ⊢z∈ω∧w∈ω→z∈w↔z⊂w
58 53 57 bitr4d ⊢z∈ω∧w∈ω→z≺w↔z∈w
59 23 29 58 syl2anc ⊢w∈ω∧y≈w∧x⊂y∧z∈ω∧x≈z→z≺w↔z∈w
60 52 59 mpbid ⊢w∈ω∧y≈w∧x⊂y∧z∈ω∧x≈z→z∈w
61 60 ex ⊢w∈ω∧y≈w∧x⊂y→z∈ω∧x≈z→z∈w
62 simpr ⊢z∈ω∧x≈z→x≈z
63 61 62 jca2 ⊢w∈ω∧y≈w∧x⊂y→z∈ω∧x≈z→z∈w∧x≈z
64 63 reximdv2 ⊢w∈ω∧y≈w∧x⊂y→∃z∈ωx≈z→∃z∈wx≈z
65 22 64 mpd ⊢w∈ω∧y≈w∧x⊂y→∃z∈wx≈z
66 r19.29 ⊢∀z∈wz∈ω→x≈z→φ∧∃z∈wx≈z→∃z∈wz∈ω→x≈z→φ∧x≈z
67 66 expcom ⊢∃z∈wx≈z→∀z∈wz∈ω→x≈z→φ→∃z∈wz∈ω→x≈z→φ∧x≈z
68 65 67 syl ⊢w∈ω∧y≈w∧x⊂y→∀z∈wz∈ω→x≈z→φ→∃z∈wz∈ω→x≈z→φ∧x≈z
69 ordom ⊢Ord⁡ω
70 ordelss ⊢Ord⁡ω∧w∈ω→w⊆ω
71 69 70 mpan ⊢w∈ω→w⊆ω
72 71 ad2antrr ⊢w∈ω∧y≈w∧x⊂y→w⊆ω
73 72 sseld ⊢w∈ω∧y≈w∧x⊂y→z∈w→z∈ω
74 pm2.27 ⊢z∈ω→z∈ω→x≈z→φ→x≈z→φ
75 74 impd ⊢z∈ω→z∈ω→x≈z→φ∧x≈z→φ
76 73 75 syl6 ⊢w∈ω∧y≈w∧x⊂y→z∈w→z∈ω→x≈z→φ∧x≈z→φ
77 76 rexlimdv ⊢w∈ω∧y≈w∧x⊂y→∃z∈wz∈ω→x≈z→φ∧x≈z→φ
78 68 77 syld ⊢w∈ω∧y≈w∧x⊂y→∀z∈wz∈ω→x≈z→φ→φ
79 78 ex ⊢w∈ω∧y≈w→x⊂y→∀z∈wz∈ω→x≈z→φ→φ
80 79 com23 ⊢w∈ω∧y≈w→∀z∈wz∈ω→x≈z→φ→x⊂y→φ
81 80 alimdv ⊢w∈ω∧y≈w→∀x∀z∈wz∈ω→x≈z→φ→∀xx⊂y→φ
82 17 81 biimtrid ⊢w∈ω∧y≈w→∀z∈wz∈ω→∀xx≈z→φ→∀xx⊂y→φ
83 13 82 3 sylsyld ⊢w∈ω∧y≈w→∀z∈wz∈ω→∀xx≈z→φ→χ
84 83 impancom ⊢w∈ω∧∀z∈wz∈ω→∀xx≈z→φ→y≈w→χ
85 84 alrimiv ⊢w∈ω∧∀z∈wz∈ω→∀xx≈z→φ→∀yy≈w→χ
86 85 expcom ⊢∀z∈wz∈ω→∀xx≈z→φ→w∈ω→∀yy≈w→χ
87 breq1 ⊢x=y→x≈w↔y≈w
88 87 1 imbi12d ⊢x=y→x≈w→φ↔y≈w→χ
89 88 cbvalvw ⊢∀xx≈w→φ↔∀yy≈w→χ
90 86 89 imbitrrdi ⊢∀z∈wz∈ω→∀xx≈z→φ→w∈ω→∀xx≈w→φ
91 90 a1i ⊢w∈On→∀z∈wz∈ω→∀xx≈z→φ→w∈ω→∀xx≈w→φ
92 10 91 tfis2 ⊢w∈On→w∈ω→∀xx≈w→φ
93 5 92 mpcom ⊢w∈ω→∀xx≈w→φ
94 93 rgen ⊢∀w∈ω∀xx≈w→φ
95 r19.29 ⊢∀w∈ω∀xx≈w→φ∧∃w∈ωA≈w→∃w∈ω∀xx≈w→φ∧A≈w
96 94 95 mpan ⊢∃w∈ωA≈w→∃w∈ω∀xx≈w→φ∧A≈w
97 4 96 sylbi ⊢A∈Fin→∃w∈ω∀xx≈w→φ∧A≈w
98 breq1 ⊢x=A→x≈w↔A≈w
99 98 2 imbi12d ⊢x=A→x≈w→φ↔A≈w→τ
100 99 spcgv ⊢A∈Fin→∀xx≈w→φ→A≈w→τ
101 100 impd ⊢A∈Fin→∀xx≈w→φ∧A≈w→τ
102 101 rexlimdvw ⊢A∈Fin→∃w∈ω∀xx≈w→φ∧A≈w→τ
103 97 102 mpd ⊢A∈Fin→τ