findcard2

Description: Schema for induction on the cardinality of a finite set. The inductive step shows that the result is true if one more element is added to the set. The result is then proven to be true for all finite sets. (Contributed by Jeff Madsen, 8-Jul-2010)

	Ref	Expression
Hypotheses	findcard2.1	$⊢ x = \emptyset \to (φ \leftrightarrow ψ)$
	findcard2.2	$⊢ x = y \to (φ \leftrightarrow χ)$
	findcard2.3	$⊢ x = y \cup \{z\} \to (φ \leftrightarrow θ)$
	findcard2.4	$⊢ x = A \to (φ \leftrightarrow τ)$
	findcard2.5	$⊢ ψ$
	findcard2.6	$⊢ y \in Fin \to (χ \to θ)$
Assertion	findcard2	$⊢ A \in Fin \to τ$

Proof

Step	Hyp	Ref	Expression
1		findcard2.1	$⊢ x = \emptyset \to (φ \leftrightarrow ψ)$
2		findcard2.2	$⊢ x = y \to (φ \leftrightarrow χ)$
3		findcard2.3	$⊢ x = y \cup \{z\} \to (φ \leftrightarrow θ)$
4		findcard2.4	$⊢ x = A \to (φ \leftrightarrow τ)$
5		findcard2.5	$⊢ ψ$
6		findcard2.6	$⊢ y \in Fin \to (χ \to θ)$
7		isfi	$⊢ x \in Fin \leftrightarrow \exists w \in ω x \approx w$
8		breq2	$⊢ w = \emptyset \to (x \approx w \leftrightarrow x \approx \emptyset)$
9	8	imbi1d	$⊢ w = \emptyset \to ((x \approx w \to φ) \leftrightarrow (x \approx \emptyset \to φ))$
10	9	albidv	$⊢ w = \emptyset \to (\forall x (x \approx w \to φ) \leftrightarrow \forall x (x \approx \emptyset \to φ))$
11		breq2	$⊢ w = v \to (x \approx w \leftrightarrow x \approx v)$
12	11	imbi1d	$⊢ w = v \to ((x \approx w \to φ) \leftrightarrow (x \approx v \to φ))$
13	12	albidv	$⊢ w = v \to (\forall x (x \approx w \to φ) \leftrightarrow \forall x (x \approx v \to φ))$
14		breq2	$⊢ w = suc v \to (x \approx w \leftrightarrow x \approx suc v)$
15	14	imbi1d	$⊢ w = suc v \to ((x \approx w \to φ) \leftrightarrow (x \approx suc v \to φ))$
16	15	albidv	$⊢ w = suc v \to (\forall x (x \approx w \to φ) \leftrightarrow \forall x (x \approx suc v \to φ))$
17		en0	$⊢ x \approx \emptyset \leftrightarrow x = \emptyset$
18	5 1	mpbiri	$⊢ x = \emptyset \to φ$
19	17 18	sylbi	$⊢ x \approx \emptyset \to φ$
20	19	ax-gen	$⊢ \forall x (x \approx \emptyset \to φ)$
21		nsuceq0	$⊢ suc v \neq \emptyset$
22		breq1	$⊢ w = \emptyset \to (w \approx suc v \leftrightarrow \emptyset \approx suc v)$
23	22	anbi2d	$⊢ w = \emptyset \to ((v \in ω \land w \approx suc v) \leftrightarrow (v \in ω \land \emptyset \approx suc v))$
24		peano1	$⊢ \emptyset \in ω$
25		peano2	$⊢ v \in ω \to suc v \in ω$
26		nneneq	$⊢ (\emptyset \in ω \land suc v \in ω) \to (\emptyset \approx suc v \leftrightarrow \emptyset = suc v)$
27	24 25 26	sylancr	$⊢ v \in ω \to (\emptyset \approx suc v \leftrightarrow \emptyset = suc v)$
28	27	biimpa	$⊢ (v \in ω \land \emptyset \approx suc v) \to \emptyset = suc v$
29	28	eqcomd	$⊢ (v \in ω \land \emptyset \approx suc v) \to suc v = \emptyset$
30	23 29	syl6bi	$⊢ w = \emptyset \to ((v \in ω \land w \approx suc v) \to suc v = \emptyset)$
31	30	com12	$⊢ (v \in ω \land w \approx suc v) \to (w = \emptyset \to suc v = \emptyset)$
32	31	necon3d	$⊢ (v \in ω \land w \approx suc v) \to (suc v \neq \emptyset \to w \neq \emptyset)$
33	21 32	mpi	$⊢ (v \in ω \land w \approx suc v) \to w \neq \emptyset$
34	33	ex	$⊢ v \in ω \to (w \approx suc v \to w \neq \emptyset)$
35		n0	$⊢ w \neq \emptyset \leftrightarrow \exists z z \in w$
36		dif1en	$⊢ (v \in ω \land w \approx suc v \land z \in w) \to (w ∖ \{z\}) \approx v$
37	36	3expia	$⊢ (v \in ω \land w \approx suc v) \to (z \in w \to (w ∖ \{z\}) \approx v)$
38		snssi	$⊢ z \in w \to \{z\} \subseteq w$
39		uncom	$⊢ (w ∖ \{z\}) \cup \{z\} = \{z\} \cup (w ∖ \{z\})$
40		undif	$⊢ \{z\} \subseteq w \leftrightarrow \{z\} \cup (w ∖ \{z\}) = w$
41	40	biimpi	$⊢ \{z\} \subseteq w \to \{z\} \cup (w ∖ \{z\}) = w$
42	39 41	syl5eq	$⊢ \{z\} \subseteq w \to (w ∖ \{z\}) \cup \{z\} = w$
43		vex	$⊢ w \in V$
44	43	difexi	$⊢ w ∖ \{z\} \in V$
45		breq1	$⊢ y = w ∖ \{z\} \to (y \approx v \leftrightarrow (w ∖ \{z\}) \approx v)$
46	45	anbi2d	$⊢ y = w ∖ \{z\} \to ((v \in ω \land y \approx v) \leftrightarrow (v \in ω \land (w ∖ \{z\}) \approx v))$
47		uneq1	$⊢ y = w ∖ \{z\} \to y \cup \{z\} = (w ∖ \{z\}) \cup \{z\}$
48	47	sbceq1d	$⊢ y = w ∖ \{z\} \to (\underset{˙}{[} (y \cup \{z\}) / x \underset{˙}{]} φ \leftrightarrow \underset{˙}{[} ((w ∖ \{z\}) \cup \{z\}) / x \underset{˙}{]} φ)$
49	48	imbi2d	$⊢ y = w ∖ \{z\} \to ((\forall x (x \approx v \to φ) \to \underset{˙}{[} (y \cup \{z\}) / x \underset{˙}{]} φ) \leftrightarrow (\forall x (x \approx v \to φ) \to \underset{˙}{[} ((w ∖ \{z\}) \cup \{z\}) / x \underset{˙}{]} φ))$
50	46 49	imbi12d	$⊢ y = w ∖ \{z\} \to (((v \in ω \land y \approx v) \to (\forall x (x \approx v \to φ) \to \underset{˙}{[} (y \cup \{z\}) / x \underset{˙}{]} φ)) \leftrightarrow ((v \in ω \land (w ∖ \{z\}) \approx v) \to (\forall x (x \approx v \to φ) \to \underset{˙}{[} ((w ∖ \{z\}) \cup \{z\}) / x \underset{˙}{]} φ)))$
51		breq1	$⊢ x = y \to (x \approx v \leftrightarrow y \approx v)$
52	51 2	imbi12d	$⊢ x = y \to ((x \approx v \to φ) \leftrightarrow (y \approx v \to χ))$
53	52	spvv	$⊢ \forall x (x \approx v \to φ) \to (y \approx v \to χ)$
54		rspe	$⊢ (v \in ω \land y \approx v) \to \exists v \in ω y \approx v$
55		isfi	$⊢ y \in Fin \leftrightarrow \exists v \in ω y \approx v$
56	54 55	sylibr	$⊢ (v \in ω \land y \approx v) \to y \in Fin$
57		pm2.27	$⊢ y \approx v \to ((y \approx v \to χ) \to χ)$
58	57	adantl	$⊢ (v \in ω \land y \approx v) \to ((y \approx v \to χ) \to χ)$
59	56 58 6	sylsyld	$⊢ (v \in ω \land y \approx v) \to ((y \approx v \to χ) \to θ)$
60	53 59	syl5	$⊢ (v \in ω \land y \approx v) \to (\forall x (x \approx v \to φ) \to θ)$
61		vex	$⊢ y \in V$
62		snex	$⊢ \{z\} \in V$
63	61 62	unex	$⊢ y \cup \{z\} \in V$
64	63 3	sbcie	$⊢ \underset{˙}{[} (y \cup \{z\}) / x \underset{˙}{]} φ \leftrightarrow θ$
65	60 64	syl6ibr	$⊢ (v \in ω \land y \approx v) \to (\forall x (x \approx v \to φ) \to \underset{˙}{[} (y \cup \{z\}) / x \underset{˙}{]} φ)$
66	44 50 65	vtocl	$⊢ (v \in ω \land (w ∖ \{z\}) \approx v) \to (\forall x (x \approx v \to φ) \to \underset{˙}{[} ((w ∖ \{z\}) \cup \{z\}) / x \underset{˙}{]} φ)$
67		dfsbcq	$⊢ (w ∖ \{z\}) \cup \{z\} = w \to (\underset{˙}{[} ((w ∖ \{z\}) \cup \{z\}) / x \underset{˙}{]} φ \leftrightarrow \underset{˙}{[} w / x \underset{˙}{]} φ)$
68	67	imbi2d	$⊢ (w ∖ \{z\}) \cup \{z\} = w \to ((\forall x (x \approx v \to φ) \to \underset{˙}{[} ((w ∖ \{z\}) \cup \{z\}) / x \underset{˙}{]} φ) \leftrightarrow (\forall x (x \approx v \to φ) \to \underset{˙}{[} w / x \underset{˙}{]} φ))$
69	66 68	syl5ib	$⊢ (w ∖ \{z\}) \cup \{z\} = w \to ((v \in ω \land (w ∖ \{z\}) \approx v) \to (\forall x (x \approx v \to φ) \to \underset{˙}{[} w / x \underset{˙}{]} φ))$
70	38 42 69	3syl	$⊢ z \in w \to ((v \in ω \land (w ∖ \{z\}) \approx v) \to (\forall x (x \approx v \to φ) \to \underset{˙}{[} w / x \underset{˙}{]} φ))$
71	70	expd	$⊢ z \in w \to (v \in ω \to ((w ∖ \{z\}) \approx v \to (\forall x (x \approx v \to φ) \to \underset{˙}{[} w / x \underset{˙}{]} φ)))$
72	71	com12	$⊢ v \in ω \to (z \in w \to ((w ∖ \{z\}) \approx v \to (\forall x (x \approx v \to φ) \to \underset{˙}{[} w / x \underset{˙}{]} φ)))$
73	72	adantr	$⊢ (v \in ω \land w \approx suc v) \to (z \in w \to ((w ∖ \{z\}) \approx v \to (\forall x (x \approx v \to φ) \to \underset{˙}{[} w / x \underset{˙}{]} φ)))$
74	37 73	mpdd	$⊢ (v \in ω \land w \approx suc v) \to (z \in w \to (\forall x (x \approx v \to φ) \to \underset{˙}{[} w / x \underset{˙}{]} φ))$
75	74	exlimdv	$⊢ (v \in ω \land w \approx suc v) \to (\exists z z \in w \to (\forall x (x \approx v \to φ) \to \underset{˙}{[} w / x \underset{˙}{]} φ))$
76	35 75	syl5bi	$⊢ (v \in ω \land w \approx suc v) \to (w \neq \emptyset \to (\forall x (x \approx v \to φ) \to \underset{˙}{[} w / x \underset{˙}{]} φ))$
77	76	ex	$⊢ v \in ω \to (w \approx suc v \to (w \neq \emptyset \to (\forall x (x \approx v \to φ) \to \underset{˙}{[} w / x \underset{˙}{]} φ)))$
78	34 77	mpdd	$⊢ v \in ω \to (w \approx suc v \to (\forall x (x \approx v \to φ) \to \underset{˙}{[} w / x \underset{˙}{]} φ))$
79	78	com23	$⊢ v \in ω \to (\forall x (x \approx v \to φ) \to (w \approx suc v \to \underset{˙}{[} w / x \underset{˙}{]} φ))$
80	79	alrimdv	$⊢ v \in ω \to (\forall x (x \approx v \to φ) \to \forall w (w \approx suc v \to \underset{˙}{[} w / x \underset{˙}{]} φ))$
81		nfv	$⊢ Ⅎ w (x \approx suc v \to φ)$
82		nfv	$⊢ Ⅎ x w \approx suc v$
83		nfsbc1v	$⊢ Ⅎ x \underset{˙}{[} w / x \underset{˙}{]} φ$
84	82 83	nfim	$⊢ Ⅎ x (w \approx suc v \to \underset{˙}{[} w / x \underset{˙}{]} φ)$
85		breq1	$⊢ x = w \to (x \approx suc v \leftrightarrow w \approx suc v)$
86		sbceq1a	$⊢ x = w \to (φ \leftrightarrow \underset{˙}{[} w / x \underset{˙}{]} φ)$
87	85 86	imbi12d	$⊢ x = w \to ((x \approx suc v \to φ) \leftrightarrow (w \approx suc v \to \underset{˙}{[} w / x \underset{˙}{]} φ))$
88	81 84 87	cbvalv1	$⊢ \forall x (x \approx suc v \to φ) \leftrightarrow \forall w (w \approx suc v \to \underset{˙}{[} w / x \underset{˙}{]} φ)$
89	80 88	syl6ibr	$⊢ v \in ω \to (\forall x (x \approx v \to φ) \to \forall x (x \approx suc v \to φ))$
90	10 13 16 20 89	finds1	$⊢ w \in ω \to \forall x (x \approx w \to φ)$
91	90	19.21bi	$⊢ w \in ω \to (x \approx w \to φ)$
92	91	rexlimiv	$⊢ \exists w \in ω x \approx w \to φ$
93	7 92	sylbi	$⊢ x \in Fin \to φ$
94	4 93	vtoclga	$⊢ A \in Fin \to τ$

Metamath Proof Explorer

Theorem findcard2

Proof