hashbclem

Description: Lemma for hashbc : inductive step. (Contributed by Mario Carneiro, 13-Jul-2014)

	Ref	Expression
Hypotheses	hashbc.1	$⊢ φ \to A \in Fin$
	hashbc.2	$⊢ φ \to \neg z \in A$
	hashbc.3	$⊢ φ \to \forall j \in ℤ (\binom{\|A\|}{j}) = \|\{x \in 𝒫 A \| \|x\| = j\}\|$
	hashbc.4	$⊢ φ \to K \in ℤ$
Assertion	hashbclem	$⊢ φ \to (\binom{\|A \cup \{z\}\|}{K}) = \|\{x \in 𝒫 (A \cup \{z\}) \| \|x\| = K\}\|$

Proof

Step	Hyp	Ref	Expression
1		hashbc.1	$⊢ φ \to A \in Fin$
2		hashbc.2	$⊢ φ \to \neg z \in A$
3		hashbc.3	$⊢ φ \to \forall j \in ℤ (\binom{\|A\|}{j}) = \|\{x \in 𝒫 A \| \|x\| = j\}\|$
4		hashbc.4	$⊢ φ \to K \in ℤ$
5		oveq2	$⊢ j = K \to (\binom{\|A\|}{j}) = (\binom{\|A\|}{K})$
6		eqeq2	$⊢ j = K \to (\|x\| = j \leftrightarrow \|x\| = K)$
7	6	rabbidv	$⊢ j = K \to \{x \in 𝒫 A \| \|x\| = j\} = \{x \in 𝒫 A \| \|x\| = K\}$
8	7	fveq2d	$⊢ j = K \to \|\{x \in 𝒫 A \| \|x\| = j\}\| = \|\{x \in 𝒫 A \| \|x\| = K\}\|$
9	5 8	eqeq12d	$⊢ j = K \to ((\binom{\|A\|}{j}) = \|\{x \in 𝒫 A \| \|x\| = j\}\| \leftrightarrow (\binom{\|A\|}{K}) = \|\{x \in 𝒫 A \| \|x\| = K\}\|)$
10	9 3 4	rspcdva	$⊢ φ \to (\binom{\|A\|}{K}) = \|\{x \in 𝒫 A \| \|x\| = K\}\|$
11		ssun1	$⊢ A \subseteq A \cup \{z\}$
12	11	sspwi	$⊢ 𝒫 A \subseteq 𝒫 (A \cup \{z\})$
13	12	sseli	$⊢ x \in 𝒫 A \to x \in 𝒫 (A \cup \{z\})$
14	13	adantl	$⊢ (φ \land x \in 𝒫 A) \to x \in 𝒫 (A \cup \{z\})$
15		elpwi	$⊢ x \in 𝒫 A \to x \subseteq A$
16	15	ssneld	$⊢ x \in 𝒫 A \to (\neg z \in A \to \neg z \in x)$
17	2 16	mpan9	$⊢ (φ \land x \in 𝒫 A) \to \neg z \in x$
18	14 17	jca	$⊢ (φ \land x \in 𝒫 A) \to (x \in 𝒫 (A \cup \{z\}) \land \neg z \in x)$
19		elpwi	$⊢ x \in 𝒫 (A \cup \{z\}) \to x \subseteq A \cup \{z\}$
20		uncom	$⊢ A \cup \{z\} = \{z\} \cup A$
21	19 20	sseqtrdi	$⊢ x \in 𝒫 (A \cup \{z\}) \to x \subseteq \{z\} \cup A$
22	21	adantr	$⊢ (x \in 𝒫 (A \cup \{z\}) \land \neg z \in x) \to x \subseteq \{z\} \cup A$
23		disjsn	$⊢ x \cap \{z\} = \emptyset \leftrightarrow \neg z \in x$
24	23	bilanri	$⊢ (x \in 𝒫 (A \cup \{z\}) \land \neg z \in x) \to x \cap \{z\} = \emptyset$
25		disjssun	$⊢ x \cap \{z\} = \emptyset \to (x \subseteq \{z\} \cup A \leftrightarrow x \subseteq A)$
26	24 25	syl	$⊢ (x \in 𝒫 (A \cup \{z\}) \land \neg z \in x) \to (x \subseteq \{z\} \cup A \leftrightarrow x \subseteq A)$
27	22 26	mpbid	$⊢ (x \in 𝒫 (A \cup \{z\}) \land \neg z \in x) \to x \subseteq A$
28		vex	$⊢ x \in V$
29	28	elpw	$⊢ x \in 𝒫 A \leftrightarrow x \subseteq A$
30	27 29	sylibr	$⊢ (x \in 𝒫 (A \cup \{z\}) \land \neg z \in x) \to x \in 𝒫 A$
31	30	adantl	$⊢ (φ \land (x \in 𝒫 (A \cup \{z\}) \land \neg z \in x)) \to x \in 𝒫 A$
32	18 31	impbida	$⊢ φ \to (x \in 𝒫 A \leftrightarrow (x \in 𝒫 (A \cup \{z\}) \land \neg z \in x))$
33	32	anbi1d	$⊢ φ \to ((x \in 𝒫 A \land \|x\| = K) \leftrightarrow ((x \in 𝒫 (A \cup \{z\}) \land \neg z \in x) \land \|x\| = K))$
34		anass	$⊢ ((x \in 𝒫 (A \cup \{z\}) \land \neg z \in x) \land \|x\| = K) \leftrightarrow (x \in 𝒫 (A \cup \{z\}) \land (\neg z \in x \land \|x\| = K))$
35	33 34	bitrdi	$⊢ φ \to ((x \in 𝒫 A \land \|x\| = K) \leftrightarrow (x \in 𝒫 (A \cup \{z\}) \land (\neg z \in x \land \|x\| = K)))$
36	35	rabbidva2	$⊢ φ \to \{x \in 𝒫 A \| \|x\| = K\} = \{x \in 𝒫 (A \cup \{z\}) \| (\neg z \in x \land \|x\| = K)\}$
37	36	fveq2d	$⊢ φ \to \|\{x \in 𝒫 A \| \|x\| = K\}\| = \|\{x \in 𝒫 (A \cup \{z\}) \| (\neg z \in x \land \|x\| = K)\}\|$
38	10 37	eqtrd	$⊢ φ \to (\binom{\|A\|}{K}) = \|\{x \in 𝒫 (A \cup \{z\}) \| (\neg z \in x \land \|x\| = K)\}\|$
39		oveq2	$⊢ j = K - 1 \to (\binom{\|A\|}{j}) = (\binom{\|A\|}{K - 1})$
40		eqeq2	$⊢ j = K - 1 \to (\|x\| = j \leftrightarrow \|x\| = K - 1)$
41	40	rabbidv	$⊢ j = K - 1 \to \{x \in 𝒫 A \| \|x\| = j\} = \{x \in 𝒫 A \| \|x\| = K - 1\}$
42	41	fveq2d	$⊢ j = K - 1 \to \|\{x \in 𝒫 A \| \|x\| = j\}\| = \|\{x \in 𝒫 A \| \|x\| = K - 1\}\|$
43	39 42	eqeq12d	$⊢ j = K - 1 \to ((\binom{\|A\|}{j}) = \|\{x \in 𝒫 A \| \|x\| = j\}\| \leftrightarrow (\binom{\|A\|}{K - 1}) = \|\{x \in 𝒫 A \| \|x\| = K - 1\}\|)$
44		peano2zm	$⊢ K \in ℤ \to K - 1 \in ℤ$
45	4 44	syl	$⊢ φ \to K - 1 \in ℤ$
46	43 3 45	rspcdva	$⊢ φ \to (\binom{\|A\|}{K - 1}) = \|\{x \in 𝒫 A \| \|x\| = K - 1\}\|$
47		pwfi	$⊢ A \in Fin \leftrightarrow 𝒫 A \in Fin$
48	1 47	sylib	$⊢ φ \to 𝒫 A \in Fin$
49		rabexg	$⊢ 𝒫 A \in Fin \to \{x \in 𝒫 A \| \|x\| = K - 1\} \in V$
50	48 49	syl	$⊢ φ \to \{x \in 𝒫 A \| \|x\| = K - 1\} \in V$
51		snfi	$⊢ \{z\} \in Fin$
52		unfi	$⊢ (A \in Fin \land \{z\} \in Fin) \to A \cup \{z\} \in Fin$
53	1 51 52	sylancl	$⊢ φ \to A \cup \{z\} \in Fin$
54		pwfi	$⊢ A \cup \{z\} \in Fin \leftrightarrow 𝒫 (A \cup \{z\}) \in Fin$
55	53 54	sylib	$⊢ φ \to 𝒫 (A \cup \{z\}) \in Fin$
56		ssrab2	$⊢ \{x \in 𝒫 (A \cup \{z\}) \| (z \in x \land \|x\| = K)\} \subseteq 𝒫 (A \cup \{z\})$
57		ssfi	$⊢ (𝒫 (A \cup \{z\}) \in Fin \land \{x \in 𝒫 (A \cup \{z\}) \| (z \in x \land \|x\| = K)\} \subseteq 𝒫 (A \cup \{z\})) \to \{x \in 𝒫 (A \cup \{z\}) \| (z \in x \land \|x\| = K)\} \in Fin$
58	55 56 57	sylancl	$⊢ φ \to \{x \in 𝒫 (A \cup \{z\}) \| (z \in x \land \|x\| = K)\} \in Fin$
59		fveqeq2	$⊢ x = u \to (\|x\| = K - 1 \leftrightarrow \|u\| = K - 1)$
60	59	elrab	$⊢ u \in \{x \in 𝒫 A \| \|x\| = K - 1\} \leftrightarrow (u \in 𝒫 A \land \|u\| = K - 1)$
61		eleq2	$⊢ x = u \cup \{z\} \to (z \in x \leftrightarrow z \in (u \cup \{z\}))$
62		fveqeq2	$⊢ x = u \cup \{z\} \to (\|x\| = K \leftrightarrow \|u \cup \{z\}\| = K)$
63	61 62	anbi12d	$⊢ x = u \cup \{z\} \to ((z \in x \land \|x\| = K) \leftrightarrow (z \in (u \cup \{z\}) \land \|u \cup \{z\}\| = K))$
64		elpwi	$⊢ u \in 𝒫 A \to u \subseteq A$
65	64	ad2antrl	$⊢ (φ \land (u \in 𝒫 A \land \|u\| = K - 1)) \to u \subseteq A$
66		unss1	$⊢ u \subseteq A \to u \cup \{z\} \subseteq A \cup \{z\}$
67	65 66	syl	$⊢ (φ \land (u \in 𝒫 A \land \|u\| = K - 1)) \to u \cup \{z\} \subseteq A \cup \{z\}$
68		vex	$⊢ u \in V$
69		vsnex	$⊢ \{z\} \in V$
70	68 69	unex	$⊢ u \cup \{z\} \in V$
71	70	elpw	$⊢ u \cup \{z\} \in 𝒫 (A \cup \{z\}) \leftrightarrow u \cup \{z\} \subseteq A \cup \{z\}$
72	67 71	sylibr	$⊢ (φ \land (u \in 𝒫 A \land \|u\| = K - 1)) \to u \cup \{z\} \in 𝒫 (A \cup \{z\})$
73	1	adantr	$⊢ (φ \land (u \in 𝒫 A \land \|u\| = K - 1)) \to A \in Fin$
74	73 65	ssfid	$⊢ (φ \land (u \in 𝒫 A \land \|u\| = K - 1)) \to u \in Fin$
75	51	a1i	$⊢ (φ \land (u \in 𝒫 A \land \|u\| = K - 1)) \to \{z\} \in Fin$
76	2	adantr	$⊢ (φ \land (u \in 𝒫 A \land \|u\| = K - 1)) \to \neg z \in A$
77	65 76	ssneldd	$⊢ (φ \land (u \in 𝒫 A \land \|u\| = K - 1)) \to \neg z \in u$
78		disjsn	$⊢ u \cap \{z\} = \emptyset \leftrightarrow \neg z \in u$
79	77 78	sylibr	$⊢ (φ \land (u \in 𝒫 A \land \|u\| = K - 1)) \to u \cap \{z\} = \emptyset$
80		hashun	$⊢ (u \in Fin \land \{z\} \in Fin \land u \cap \{z\} = \emptyset) \to \|u \cup \{z\}\| = \|u\| + \|\{z\}\|$
81	74 75 79 80	syl3anc	$⊢ (φ \land (u \in 𝒫 A \land \|u\| = K - 1)) \to \|u \cup \{z\}\| = \|u\| + \|\{z\}\|$
82		simprr	$⊢ (φ \land (u \in 𝒫 A \land \|u\| = K - 1)) \to \|u\| = K - 1$
83		hashsng	$⊢ z \in V \to \|\{z\}\| = 1$
84	83	elv	$⊢ \|\{z\}\| = 1$
85	84	a1i	$⊢ (φ \land (u \in 𝒫 A \land \|u\| = K - 1)) \to \|\{z\}\| = 1$
86	82 85	oveq12d	$⊢ (φ \land (u \in 𝒫 A \land \|u\| = K - 1)) \to \|u\| + \|\{z\}\| = K - 1 + 1$
87	4	adantr	$⊢ (φ \land (u \in 𝒫 A \land \|u\| = K - 1)) \to K \in ℤ$
88	87	zcnd	$⊢ (φ \land (u \in 𝒫 A \land \|u\| = K - 1)) \to K \in ℂ$
89		ax-1cn	$⊢ 1 \in ℂ$
90		npcan	$⊢ (K \in ℂ \land 1 \in ℂ) \to K - 1 + 1 = K$
91	88 89 90	sylancl	$⊢ (φ \land (u \in 𝒫 A \land \|u\| = K - 1)) \to K - 1 + 1 = K$
92	81 86 91	3eqtrd	$⊢ (φ \land (u \in 𝒫 A \land \|u\| = K - 1)) \to \|u \cup \{z\}\| = K$
93		ssun2	$⊢ \{z\} \subseteq u \cup \{z\}$
94		vex	$⊢ z \in V$
95	94	snss	$⊢ z \in (u \cup \{z\}) \leftrightarrow \{z\} \subseteq u \cup \{z\}$
96	93 95	mpbir	$⊢ z \in (u \cup \{z\})$
97	92 96	jctil	$⊢ (φ \land (u \in 𝒫 A \land \|u\| = K - 1)) \to (z \in (u \cup \{z\}) \land \|u \cup \{z\}\| = K)$
98	63 72 97	elrabd	$⊢ (φ \land (u \in 𝒫 A \land \|u\| = K - 1)) \to u \cup \{z\} \in \{x \in 𝒫 (A \cup \{z\}) \| (z \in x \land \|x\| = K)\}$
99	98	ex	$⊢ φ \to ((u \in 𝒫 A \land \|u\| = K - 1) \to u \cup \{z\} \in \{x \in 𝒫 (A \cup \{z\}) \| (z \in x \land \|x\| = K)\})$
100	60 99	biimtrid	$⊢ φ \to (u \in \{x \in 𝒫 A \| \|x\| = K - 1\} \to u \cup \{z\} \in \{x \in 𝒫 (A \cup \{z\}) \| (z \in x \land \|x\| = K)\})$
101		eleq2	$⊢ x = v \to (z \in x \leftrightarrow z \in v)$
102		fveqeq2	$⊢ x = v \to (\|x\| = K \leftrightarrow \|v\| = K)$
103	101 102	anbi12d	$⊢ x = v \to ((z \in x \land \|x\| = K) \leftrightarrow (z \in v \land \|v\| = K))$
104	103	elrab	$⊢ v \in \{x \in 𝒫 (A \cup \{z\}) \| (z \in x \land \|x\| = K)\} \leftrightarrow (v \in 𝒫 (A \cup \{z\}) \land (z \in v \land \|v\| = K))$
105		fveqeq2	$⊢ x = v ∖ \{z\} \to (\|x\| = K - 1 \leftrightarrow \|v ∖ \{z\}\| = K - 1)$
106		elpwi	$⊢ v \in 𝒫 (A \cup \{z\}) \to v \subseteq A \cup \{z\}$
107	106	ad2antrl	$⊢ (φ \land (v \in 𝒫 (A \cup \{z\}) \land (z \in v \land \|v\| = K))) \to v \subseteq A \cup \{z\}$
108	107 20	sseqtrdi	$⊢ (φ \land (v \in 𝒫 (A \cup \{z\}) \land (z \in v \land \|v\| = K))) \to v \subseteq \{z\} \cup A$
109		ssundif	$⊢ v \subseteq \{z\} \cup A \leftrightarrow v ∖ \{z\} \subseteq A$
110	108 109	sylib	$⊢ (φ \land (v \in 𝒫 (A \cup \{z\}) \land (z \in v \land \|v\| = K))) \to v ∖ \{z\} \subseteq A$
111		vex	$⊢ v \in V$
112	111	difexi	$⊢ v ∖ \{z\} \in V$
113	112	elpw	$⊢ v ∖ \{z\} \in 𝒫 A \leftrightarrow v ∖ \{z\} \subseteq A$
114	110 113	sylibr	$⊢ (φ \land (v \in 𝒫 (A \cup \{z\}) \land (z \in v \land \|v\| = K))) \to v ∖ \{z\} \in 𝒫 A$
115	1	adantr	$⊢ (φ \land (v \in 𝒫 (A \cup \{z\}) \land (z \in v \land \|v\| = K))) \to A \in Fin$
116	115 110	ssfid	$⊢ (φ \land (v \in 𝒫 (A \cup \{z\}) \land (z \in v \land \|v\| = K))) \to v ∖ \{z\} \in Fin$
117		hashcl	$⊢ v ∖ \{z\} \in Fin \to \|v ∖ \{z\}\| \in ℕ_{0}$
118	116 117	syl	$⊢ (φ \land (v \in 𝒫 (A \cup \{z\}) \land (z \in v \land \|v\| = K))) \to \|v ∖ \{z\}\| \in ℕ_{0}$
119	118	nn0cnd	$⊢ (φ \land (v \in 𝒫 (A \cup \{z\}) \land (z \in v \land \|v\| = K))) \to \|v ∖ \{z\}\| \in ℂ$
120		pncan	$⊢ (\|v ∖ \{z\}\| \in ℂ \land 1 \in ℂ) \to \|v ∖ \{z\}\| + 1 - 1 = \|v ∖ \{z\}\|$
121	119 89 120	sylancl	$⊢ (φ \land (v \in 𝒫 (A \cup \{z\}) \land (z \in v \land \|v\| = K))) \to \|v ∖ \{z\}\| + 1 - 1 = \|v ∖ \{z\}\|$
122		undif1	$⊢ (v ∖ \{z\}) \cup \{z\} = v \cup \{z\}$
123		simprrl	$⊢ (φ \land (v \in 𝒫 (A \cup \{z\}) \land (z \in v \land \|v\| = K))) \to z \in v$
124	123	snssd	$⊢ (φ \land (v \in 𝒫 (A \cup \{z\}) \land (z \in v \land \|v\| = K))) \to \{z\} \subseteq v$
125		ssequn2	$⊢ \{z\} \subseteq v \leftrightarrow v \cup \{z\} = v$
126	124 125	sylib	$⊢ (φ \land (v \in 𝒫 (A \cup \{z\}) \land (z \in v \land \|v\| = K))) \to v \cup \{z\} = v$
127	122 126	eqtrid	$⊢ (φ \land (v \in 𝒫 (A \cup \{z\}) \land (z \in v \land \|v\| = K))) \to (v ∖ \{z\}) \cup \{z\} = v$
128	127	fveq2d	$⊢ (φ \land (v \in 𝒫 (A \cup \{z\}) \land (z \in v \land \|v\| = K))) \to \|(v ∖ \{z\}) \cup \{z\}\| = \|v\|$
129	51	a1i	$⊢ (φ \land (v \in 𝒫 (A \cup \{z\}) \land (z \in v \land \|v\| = K))) \to \{z\} \in Fin$
130		disjdifr	$⊢ (v ∖ \{z\}) \cap \{z\} = \emptyset$
131	130	a1i	$⊢ (φ \land (v \in 𝒫 (A \cup \{z\}) \land (z \in v \land \|v\| = K))) \to (v ∖ \{z\}) \cap \{z\} = \emptyset$
132		hashun	$⊢ (v ∖ \{z\} \in Fin \land \{z\} \in Fin \land (v ∖ \{z\}) \cap \{z\} = \emptyset) \to \|(v ∖ \{z\}) \cup \{z\}\| = \|v ∖ \{z\}\| + \|\{z\}\|$
133	116 129 131 132	syl3anc	$⊢ (φ \land (v \in 𝒫 (A \cup \{z\}) \land (z \in v \land \|v\| = K))) \to \|(v ∖ \{z\}) \cup \{z\}\| = \|v ∖ \{z\}\| + \|\{z\}\|$
134	84	oveq2i	$⊢ \|v ∖ \{z\}\| + \|\{z\}\| = \|v ∖ \{z\}\| + 1$
135	133 134	eqtrdi	$⊢ (φ \land (v \in 𝒫 (A \cup \{z\}) \land (z \in v \land \|v\| = K))) \to \|(v ∖ \{z\}) \cup \{z\}\| = \|v ∖ \{z\}\| + 1$
136		simprrr	$⊢ (φ \land (v \in 𝒫 (A \cup \{z\}) \land (z \in v \land \|v\| = K))) \to \|v\| = K$
137	128 135 136	3eqtr3d	$⊢ (φ \land (v \in 𝒫 (A \cup \{z\}) \land (z \in v \land \|v\| = K))) \to \|v ∖ \{z\}\| + 1 = K$
138	137	oveq1d	$⊢ (φ \land (v \in 𝒫 (A \cup \{z\}) \land (z \in v \land \|v\| = K))) \to \|v ∖ \{z\}\| + 1 - 1 = K - 1$
139	121 138	eqtr3d	$⊢ (φ \land (v \in 𝒫 (A \cup \{z\}) \land (z \in v \land \|v\| = K))) \to \|v ∖ \{z\}\| = K - 1$
140	105 114 139	elrabd	$⊢ (φ \land (v \in 𝒫 (A \cup \{z\}) \land (z \in v \land \|v\| = K))) \to v ∖ \{z\} \in \{x \in 𝒫 A \| \|x\| = K - 1\}$
141	140	ex	$⊢ φ \to ((v \in 𝒫 (A \cup \{z\}) \land (z \in v \land \|v\| = K)) \to v ∖ \{z\} \in \{x \in 𝒫 A \| \|x\| = K - 1\})$
142	104 141	biimtrid	$⊢ φ \to (v \in \{x \in 𝒫 (A \cup \{z\}) \| (z \in x \land \|x\| = K)\} \to v ∖ \{z\} \in \{x \in 𝒫 A \| \|x\| = K - 1\})$
143	60 104	anbi12i	$⊢ (u \in \{x \in 𝒫 A \| \|x\| = K - 1\} \land v \in \{x \in 𝒫 (A \cup \{z\}) \| (z \in x \land \|x\| = K)\}) \leftrightarrow ((u \in 𝒫 A \land \|u\| = K - 1) \land (v \in 𝒫 (A \cup \{z\}) \land (z \in v \land \|v\| = K)))$
144		simp3rl	$⊢ (φ \land (u \in 𝒫 A \land \|u\| = K - 1) \land (v \in 𝒫 (A \cup \{z\}) \land (z \in v \land \|v\| = K))) \to z \in v$
145	144	snssd	$⊢ (φ \land (u \in 𝒫 A \land \|u\| = K - 1) \land (v \in 𝒫 (A \cup \{z\}) \land (z \in v \land \|v\| = K))) \to \{z\} \subseteq v$
146		incom	$⊢ \{z\} \cap u = u \cap \{z\}$
147	79	3adant3	$⊢ (φ \land (u \in 𝒫 A \land \|u\| = K - 1) \land (v \in 𝒫 (A \cup \{z\}) \land (z \in v \land \|v\| = K))) \to u \cap \{z\} = \emptyset$
148	146 147	eqtrid	$⊢ (φ \land (u \in 𝒫 A \land \|u\| = K - 1) \land (v \in 𝒫 (A \cup \{z\}) \land (z \in v \land \|v\| = K))) \to \{z\} \cap u = \emptyset$
149		uneqdifeq	$⊢ (\{z\} \subseteq v \land \{z\} \cap u = \emptyset) \to (\{z\} \cup u = v \leftrightarrow v ∖ \{z\} = u)$
150	145 148 149	syl2anc	$⊢ (φ \land (u \in 𝒫 A \land \|u\| = K - 1) \land (v \in 𝒫 (A \cup \{z\}) \land (z \in v \land \|v\| = K))) \to (\{z\} \cup u = v \leftrightarrow v ∖ \{z\} = u)$
151	150	bicomd	$⊢ (φ \land (u \in 𝒫 A \land \|u\| = K - 1) \land (v \in 𝒫 (A \cup \{z\}) \land (z \in v \land \|v\| = K))) \to (v ∖ \{z\} = u \leftrightarrow \{z\} \cup u = v)$
152		eqcom	$⊢ u = v ∖ \{z\} \leftrightarrow v ∖ \{z\} = u$
153		eqcom	$⊢ v = u \cup \{z\} \leftrightarrow u \cup \{z\} = v$
154		uncom	$⊢ u \cup \{z\} = \{z\} \cup u$
155	154	eqeq1i	$⊢ u \cup \{z\} = v \leftrightarrow \{z\} \cup u = v$
156	153 155	bitri	$⊢ v = u \cup \{z\} \leftrightarrow \{z\} \cup u = v$
157	151 152 156	3bitr4g	$⊢ (φ \land (u \in 𝒫 A \land \|u\| = K - 1) \land (v \in 𝒫 (A \cup \{z\}) \land (z \in v \land \|v\| = K))) \to (u = v ∖ \{z\} \leftrightarrow v = u \cup \{z\})$
158	157	3expib	$⊢ φ \to (((u \in 𝒫 A \land \|u\| = K - 1) \land (v \in 𝒫 (A \cup \{z\}) \land (z \in v \land \|v\| = K))) \to (u = v ∖ \{z\} \leftrightarrow v = u \cup \{z\}))$
159	143 158	biimtrid	$⊢ φ \to ((u \in \{x \in 𝒫 A \| \|x\| = K - 1\} \land v \in \{x \in 𝒫 (A \cup \{z\}) \| (z \in x \land \|x\| = K)\}) \to (u = v ∖ \{z\} \leftrightarrow v = u \cup \{z\}))$
160	50 58 100 142 159	en3d	$⊢ φ \to \{x \in 𝒫 A \| \|x\| = K - 1\} \approx \{x \in 𝒫 (A \cup \{z\}) \| (z \in x \land \|x\| = K)\}$
161		ssrab2	$⊢ \{x \in 𝒫 A \| \|x\| = K - 1\} \subseteq 𝒫 A$
162		ssfi	$⊢ (𝒫 A \in Fin \land \{x \in 𝒫 A \| \|x\| = K - 1\} \subseteq 𝒫 A) \to \{x \in 𝒫 A \| \|x\| = K - 1\} \in Fin$
163	48 161 162	sylancl	$⊢ φ \to \{x \in 𝒫 A \| \|x\| = K - 1\} \in Fin$
164		hashen	$⊢ (\{x \in 𝒫 A \| \|x\| = K - 1\} \in Fin \land \{x \in 𝒫 (A \cup \{z\}) \| (z \in x \land \|x\| = K)\} \in Fin) \to (\|\{x \in 𝒫 A \| \|x\| = K - 1\}\| = \|\{x \in 𝒫 (A \cup \{z\}) \| (z \in x \land \|x\| = K)\}\| \leftrightarrow \{x \in 𝒫 A \| \|x\| = K - 1\} \approx \{x \in 𝒫 (A \cup \{z\}) \| (z \in x \land \|x\| = K)\})$
165	163 58 164	syl2anc	$⊢ φ \to (\|\{x \in 𝒫 A \| \|x\| = K - 1\}\| = \|\{x \in 𝒫 (A \cup \{z\}) \| (z \in x \land \|x\| = K)\}\| \leftrightarrow \{x \in 𝒫 A \| \|x\| = K - 1\} \approx \{x \in 𝒫 (A \cup \{z\}) \| (z \in x \land \|x\| = K)\})$
166	160 165	mpbird	$⊢ φ \to \|\{x \in 𝒫 A \| \|x\| = K - 1\}\| = \|\{x \in 𝒫 (A \cup \{z\}) \| (z \in x \land \|x\| = K)\}\|$
167	46 166	eqtrd	$⊢ φ \to (\binom{\|A\|}{K - 1}) = \|\{x \in 𝒫 (A \cup \{z\}) \| (z \in x \land \|x\| = K)\}\|$
168	38 167	oveq12d	$⊢ φ \to (\binom{\|A\|}{K}) + (\binom{\|A\|}{K - 1}) = \|\{x \in 𝒫 (A \cup \{z\}) \| (\neg z \in x \land \|x\| = K)\}\| + \|\{x \in 𝒫 (A \cup \{z\}) \| (z \in x \land \|x\| = K)\}\|$
169	51	a1i	$⊢ φ \to \{z\} \in Fin$
170		disjsn	$⊢ A \cap \{z\} = \emptyset \leftrightarrow \neg z \in A$
171	2 170	sylibr	$⊢ φ \to A \cap \{z\} = \emptyset$
172		hashun	$⊢ (A \in Fin \land \{z\} \in Fin \land A \cap \{z\} = \emptyset) \to \|A \cup \{z\}\| = \|A\| + \|\{z\}\|$
173	1 169 171 172	syl3anc	$⊢ φ \to \|A \cup \{z\}\| = \|A\| + \|\{z\}\|$
174	84	oveq2i	$⊢ \|A\| + \|\{z\}\| = \|A\| + 1$
175	173 174	eqtrdi	$⊢ φ \to \|A \cup \{z\}\| = \|A\| + 1$
176	175	oveq1d	$⊢ φ \to (\binom{\|A \cup \{z\}\|}{K}) = (\binom{\|A\| + 1}{K})$
177		hashcl	$⊢ A \in Fin \to \|A\| \in ℕ_{0}$
178	1 177	syl	$⊢ φ \to \|A\| \in ℕ_{0}$
179		bcpasc	$⊢ (\|A\| \in ℕ_{0} \land K \in ℤ) \to (\binom{\|A\|}{K}) + (\binom{\|A\|}{K - 1}) = (\binom{\|A\| + 1}{K})$
180	178 4 179	syl2anc	$⊢ φ \to (\binom{\|A\|}{K}) + (\binom{\|A\|}{K - 1}) = (\binom{\|A\| + 1}{K})$
181	176 180	eqtr4d	$⊢ φ \to (\binom{\|A \cup \{z\}\|}{K}) = (\binom{\|A\|}{K}) + (\binom{\|A\|}{K - 1})$
182		pm2.1	$⊢ (\neg z \in x \lor z \in x)$
183	182	biantrur	$⊢ \|x\| = K \leftrightarrow ((\neg z \in x \lor z \in x) \land \|x\| = K)$
184		andir	$⊢ ((\neg z \in x \lor z \in x) \land \|x\| = K) \leftrightarrow ((\neg z \in x \land \|x\| = K) \lor (z \in x \land \|x\| = K))$
185	183 184	bitri	$⊢ \|x\| = K \leftrightarrow ((\neg z \in x \land \|x\| = K) \lor (z \in x \land \|x\| = K))$
186	185	rabbii	$⊢ \{x \in 𝒫 (A \cup \{z\}) \| \|x\| = K\} = \{x \in 𝒫 (A \cup \{z\}) \| ((\neg z \in x \land \|x\| = K) \lor (z \in x \land \|x\| = K))\}$
187		unrab	$⊢ \{x \in 𝒫 (A \cup \{z\}) \| (\neg z \in x \land \|x\| = K)\} \cup \{x \in 𝒫 (A \cup \{z\}) \| (z \in x \land \|x\| = K)\} = \{x \in 𝒫 (A \cup \{z\}) \| ((\neg z \in x \land \|x\| = K) \lor (z \in x \land \|x\| = K))\}$
188	186 187	eqtr4i	$⊢ \{x \in 𝒫 (A \cup \{z\}) \| \|x\| = K\} = \{x \in 𝒫 (A \cup \{z\}) \| (\neg z \in x \land \|x\| = K)\} \cup \{x \in 𝒫 (A \cup \{z\}) \| (z \in x \land \|x\| = K)\}$
189	188	fveq2i	$⊢ \|\{x \in 𝒫 (A \cup \{z\}) \| \|x\| = K\}\| = \|\{x \in 𝒫 (A \cup \{z\}) \| (\neg z \in x \land \|x\| = K)\} \cup \{x \in 𝒫 (A \cup \{z\}) \| (z \in x \land \|x\| = K)\}\|$
190		ssrab2	$⊢ \{x \in 𝒫 (A \cup \{z\}) \| (\neg z \in x \land \|x\| = K)\} \subseteq 𝒫 (A \cup \{z\})$
191		ssfi	$⊢ (𝒫 (A \cup \{z\}) \in Fin \land \{x \in 𝒫 (A \cup \{z\}) \| (\neg z \in x \land \|x\| = K)\} \subseteq 𝒫 (A \cup \{z\})) \to \{x \in 𝒫 (A \cup \{z\}) \| (\neg z \in x \land \|x\| = K)\} \in Fin$
192	55 190 191	sylancl	$⊢ φ \to \{x \in 𝒫 (A \cup \{z\}) \| (\neg z \in x \land \|x\| = K)\} \in Fin$
193		inrab	$⊢ \{x \in 𝒫 (A \cup \{z\}) \| (\neg z \in x \land \|x\| = K)\} \cap \{x \in 𝒫 (A \cup \{z\}) \| (z \in x \land \|x\| = K)\} = \{x \in 𝒫 (A \cup \{z\}) \| ((\neg z \in x \land \|x\| = K) \land (z \in x \land \|x\| = K))\}$
194		simprl	$⊢ ((\neg z \in x \land \|x\| = K) \land (z \in x \land \|x\| = K)) \to z \in x$
195		simpll	$⊢ ((\neg z \in x \land \|x\| = K) \land (z \in x \land \|x\| = K)) \to \neg z \in x$
196	194 195	pm2.65i	$⊢ \neg ((\neg z \in x \land \|x\| = K) \land (z \in x \land \|x\| = K))$
197	196	rgenw	$⊢ \forall x \in 𝒫 (A \cup \{z\}) \neg ((\neg z \in x \land \|x\| = K) \land (z \in x \land \|x\| = K))$
198		rabeq0	$⊢ \{x \in 𝒫 (A \cup \{z\}) \| ((\neg z \in x \land \|x\| = K) \land (z \in x \land \|x\| = K))\} = \emptyset \leftrightarrow \forall x \in 𝒫 (A \cup \{z\}) \neg ((\neg z \in x \land \|x\| = K) \land (z \in x \land \|x\| = K))$
199	197 198	mpbir	$⊢ \{x \in 𝒫 (A \cup \{z\}) \| ((\neg z \in x \land \|x\| = K) \land (z \in x \land \|x\| = K))\} = \emptyset$
200	193 199	eqtri	$⊢ \{x \in 𝒫 (A \cup \{z\}) \| (\neg z \in x \land \|x\| = K)\} \cap \{x \in 𝒫 (A \cup \{z\}) \| (z \in x \land \|x\| = K)\} = \emptyset$
201	200	a1i	$⊢ φ \to \{x \in 𝒫 (A \cup \{z\}) \| (\neg z \in x \land \|x\| = K)\} \cap \{x \in 𝒫 (A \cup \{z\}) \| (z \in x \land \|x\| = K)\} = \emptyset$
202		hashun	$⊢ (\{x \in 𝒫 (A \cup \{z\}) \| (\neg z \in x \land \|x\| = K)\} \in Fin \land \{x \in 𝒫 (A \cup \{z\}) \| (z \in x \land \|x\| = K)\} \in Fin \land \{x \in 𝒫 (A \cup \{z\}) \| (\neg z \in x \land \|x\| = K)\} \cap \{x \in 𝒫 (A \cup \{z\}) \| (z \in x \land \|x\| = K)\} = \emptyset) \to \|\{x \in 𝒫 (A \cup \{z\}) \| (\neg z \in x \land \|x\| = K)\} \cup \{x \in 𝒫 (A \cup \{z\}) \| (z \in x \land \|x\| = K)\}\| = \|\{x \in 𝒫 (A \cup \{z\}) \| (\neg z \in x \land \|x\| = K)\}\| + \|\{x \in 𝒫 (A \cup \{z\}) \| (z \in x \land \|x\| = K)\}\|$
203	192 58 201 202	syl3anc	$⊢ φ \to \|\{x \in 𝒫 (A \cup \{z\}) \| (\neg z \in x \land \|x\| = K)\} \cup \{x \in 𝒫 (A \cup \{z\}) \| (z \in x \land \|x\| = K)\}\| = \|\{x \in 𝒫 (A \cup \{z\}) \| (\neg z \in x \land \|x\| = K)\}\| + \|\{x \in 𝒫 (A \cup \{z\}) \| (z \in x \land \|x\| = K)\}\|$
204	189 203	eqtrid	$⊢ φ \to \|\{x \in 𝒫 (A \cup \{z\}) \| \|x\| = K\}\| = \|\{x \in 𝒫 (A \cup \{z\}) \| (\neg z \in x \land \|x\| = K)\}\| + \|\{x \in 𝒫 (A \cup \{z\}) \| (z \in x \land \|x\| = K)\}\|$
205	168 181 204	3eqtr4d	$⊢ φ \to (\binom{\|A \cup \{z\}\|}{K}) = \|\{x \in 𝒫 (A \cup \{z\}) \| \|x\| = K\}\|$

Metamath Proof Explorer

Theorem hashbclem

Proof