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

Metamath Proof Explorer

Theorem hashbclem

Proof