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 \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		simprl	$⊢ (((w \in ω \land y \approx w) \land x \subset y) \land (z \in ω \land x \approx z)) \to z \in ω$
24		nnfi	$⊢ z \in ω \to z \in Fin$
25		ensymfib	$⊢ z \in Fin \to (z \approx x \leftrightarrow x \approx z)$
26	24 25	syl	$⊢ z \in ω \to (z \approx x \leftrightarrow x \approx z)$
27	26	biimpar	$⊢ (z \in ω \land x \approx z) \to z \approx x$
28	27	adantl	$⊢ (((w \in ω \land y \approx w) \land x \subset y) \land (z \in ω \land x \approx z)) \to z \approx x$
29		simplll	$⊢ (((w \in ω \land y \approx w) \land x \subset y) \land (z \in ω \land x \approx z)) \to w \in ω$
30		php3	$⊢ (y \in Fin \land x \subset y) \to x ≺ y$
31	13 30	sylan	$⊢ ((w \in ω \land y \approx w) \land x \subset y) \to x ≺ y$
32	31	adantr	$⊢ (((w \in ω \land y \approx w) \land x \subset y) \land (z \in ω \land x \approx z)) \to x ≺ y$
33		simpllr	$⊢ (((w \in ω \land y \approx w) \land x \subset y) \land (z \in ω \land x \approx z)) \to y \approx w$
34		endom	$⊢ y \approx w \to y ≼ w$
35		nnfi	$⊢ w \in ω \to w \in Fin$
36		domfi	$⊢ (w \in Fin \land y ≼ w) \to y \in Fin$
37	35 36	sylan	$⊢ (w \in ω \land y ≼ w) \to y \in Fin$
38	37	3adant2	$⊢ (w \in ω \land x ≺ y \land y ≼ w) \to y \in Fin$
39		sdomdom	$⊢ x ≺ y \to x ≼ y$
40		domfi	$⊢ (y \in Fin \land x ≼ y) \to x \in Fin$
41	39 40	sylan2	$⊢ (y \in Fin \land x ≺ y) \to x \in Fin$
42	41	3adant3	$⊢ (y \in Fin \land x ≺ y \land y ≼ w) \to x \in Fin$
43	38 42	syld3an1	$⊢ (w \in ω \land x ≺ y \land y ≼ w) \to x \in Fin$
44		sdomdomtrfi	$⊢ (x \in Fin \land x ≺ y \land y ≼ w) \to x ≺ w$
45	43 44	syld3an1	$⊢ (w \in ω \land x ≺ y \land y ≼ w) \to x ≺ w$
46	34 45	syl3an3	$⊢ (w \in ω \land x ≺ y \land y \approx w) \to x ≺ w$
47	29 32 33 46	syl3anc	$⊢ (((w \in ω \land y \approx w) \land x \subset y) \land (z \in ω \land x \approx z)) \to x ≺ w$
48		endom	$⊢ z \approx x \to z ≼ x$
49		domsdomtrfi	$⊢ (z \in Fin \land z ≼ x \land x ≺ w) \to z ≺ w$
50	24 49	syl3an1	$⊢ (z \in ω \land z ≼ x \land x ≺ w) \to z ≺ w$
51	48 50	syl3an2	$⊢ (z \in ω \land z \approx x \land x ≺ w) \to z ≺ w$
52	23 28 47 51	syl3anc	$⊢ (((w \in ω \land y \approx w) \land x \subset y) \land (z \in ω \land x \approx z)) \to z ≺ w$
53		nnsdomo	$⊢ (z \in ω \land w \in ω) \to (z ≺ w \leftrightarrow z \subset w)$
54		nnord	$⊢ z \in ω \to Ord z$
55		nnord	$⊢ w \in ω \to Ord w$
56		ordelpss	$⊢ (Ord z \land Ord w) \to (z \in w \leftrightarrow z \subset w)$
57	54 55 56	syl2an	$⊢ (z \in ω \land w \in ω) \to (z \in w \leftrightarrow z \subset w)$
58	53 57	bitr4d	$⊢ (z \in ω \land w \in ω) \to (z ≺ w \leftrightarrow z \in w)$
59	23 29 58	syl2anc	$⊢ (((w \in ω \land y \approx w) \land x \subset y) \land (z \in ω \land x \approx z)) \to (z ≺ w \leftrightarrow z \in w)$
60	52 59	mpbid	$⊢ (((w \in ω \land y \approx w) \land x \subset y) \land (z \in ω \land x \approx z)) \to z \in w$
61	60	ex	$⊢ ((w \in ω \land y \approx w) \land x \subset y) \to ((z \in ω \land x \approx z) \to z \in w)$
62		simpr	$⊢ (z \in ω \land x \approx z) \to x \approx z$
63	61 62	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))$
64	63	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)$
65	22 64	mpd	$⊢ ((w \in ω \land y \approx w) \land x \subset y) \to \exists z \in w x \approx z$
66		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)$
67	66	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))$
68	65 67	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))$
69		ordom	$⊢ Ord ω$
70		ordelss	$⊢ (Ord ω \land w \in ω) \to w \subseteq ω$
71	69 70	mpan	$⊢ w \in ω \to w \subseteq ω$
72	71	ad2antrr	$⊢ ((w \in ω \land y \approx w) \land x \subset y) \to w \subseteq ω$
73	72	sseld	$⊢ ((w \in ω \land y \approx w) \land x \subset y) \to (z \in w \to z \in ω)$
74		pm2.27	$⊢ z \in ω \to ((z \in ω \to (x \approx z \to φ)) \to (x \approx z \to φ))$
75	74	impd	$⊢ z \in ω \to (((z \in ω \to (x \approx z \to φ)) \land x \approx z) \to φ)$
76	73 75	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 φ))$
77	76	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 φ)$
78	68 77	syld	$⊢ ((w \in ω \land y \approx w) \land x \subset y) \to (\forall z \in w (z \in ω \to (x \approx z \to φ)) \to φ)$
79	78	ex	$⊢ (w \in ω \land y \approx w) \to (x \subset y \to (\forall z \in w (z \in ω \to (x \approx z \to φ)) \to φ))$
80	79	com23	$⊢ (w \in ω \land y \approx w) \to (\forall z \in w (z \in ω \to (x \approx z \to φ)) \to (x \subset y \to φ))$
81	80	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 φ))$
82	17 81	biimtrid	$⊢ (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 φ))$
83	13 82 3	sylsyld	$⊢ (w \in ω \land y \approx w) \to (\forall z \in w (z \in ω \to \forall x (x \approx z \to φ)) \to χ)$
84	83	impancom	$⊢ (w \in ω \land \forall z \in w (z \in ω \to \forall x (x \approx z \to φ))) \to (y \approx w \to χ)$
85	84	alrimiv	$⊢ (w \in ω \land \forall z \in w (z \in ω \to \forall x (x \approx z \to φ))) \to \forall y (y \approx w \to χ)$
86	85	expcom	$⊢ \forall z \in w (z \in ω \to \forall x (x \approx z \to φ)) \to (w \in ω \to \forall y (y \approx w \to χ))$
87		breq1	$⊢ x = y \to (x \approx w \leftrightarrow y \approx w)$
88	87 1	imbi12d	$⊢ x = y \to ((x \approx w \to φ) \leftrightarrow (y \approx w \to χ))$
89	88	cbvalvw	$⊢ \forall x (x \approx w \to φ) \leftrightarrow \forall y (y \approx w \to χ)$
90	86 89	imbitrrdi	$⊢ \forall z \in w (z \in ω \to \forall x (x \approx z \to φ)) \to (w \in ω \to \forall x (x \approx w \to φ))$
91	90	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 φ)))$
92	10 91	tfis2	$⊢ w \in On \to (w \in ω \to \forall x (x \approx w \to φ))$
93	5 92	mpcom	$⊢ w \in ω \to \forall x (x \approx w \to φ)$
94	93	rgen	$⊢ \forall w \in ω \forall x (x \approx w \to φ)$
95		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)$
96	94 95	mpan	$⊢ \exists w \in ω A \approx w \to \exists w \in ω (\forall x (x \approx w \to φ) \land A \approx w)$
97	4 96	sylbi	$⊢ A \in Fin \to \exists w \in ω (\forall x (x \approx w \to φ) \land A \approx w)$
98		breq1	$⊢ x = A \to (x \approx w \leftrightarrow A \approx w)$
99	98 2	imbi12d	$⊢ x = A \to ((x \approx w \to φ) \leftrightarrow (A \approx w \to τ))$
100	99	spcgv	$⊢ A \in Fin \to (\forall x (x \approx w \to φ) \to (A \approx w \to τ))$
101	100	impd	$⊢ A \in Fin \to ((\forall x (x \approx w \to φ) \land A \approx w) \to τ)$
102	101	rexlimdvw	$⊢ A \in Fin \to (\exists w \in ω (\forall x (x \approx w \to φ) \land A \approx w) \to τ)$
103	97 102	mpd	$⊢ A \in Fin \to τ$

Metamath Proof Explorer

Theorem findcard3

Proof