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

Metamath Proof Explorer

Theorem hashbclem

Proof