# 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}\to \left({\phi }↔{\chi }\right)$
findcard3.2 ${⊢}{x}={A}\to \left({\phi }↔{\tau }\right)$
findcard3.3 ${⊢}{y}\in \mathrm{Fin}\to \left(\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\subset {y}\to {\phi }\right)\to {\chi }\right)$
Assertion findcard3 ${⊢}{A}\in \mathrm{Fin}\to {\tau }$

### Proof

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