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 (φ \leftrightarrow χ)$
	findcard3.2	$⊢ x = A \to (φ \leftrightarrow τ)$
	findcard3.3	$⊢ y \in Fin \to (\forall x (x \subset y \to φ) \to χ)$
Assertion	findcard3	$⊢ A \in Fin \to τ$

Proof

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

Metamath Proof Explorer

Theorem findcard3

Proof