hashbclem - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > hashbclem		Structured version Visualization version GIF version

Theorem hashbclem 13174

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

**Hypotheses**
Ref	Expression
hashbc.1	⊢ (𝜑 → 𝐴 ∈ Fin)
hashbc.2	⊢ (𝜑 → ¬ 𝑧 ∈ 𝐴)
hashbc.3	⊢ (𝜑 → ∀𝑗 ∈ ℤ ((#‘𝐴)C𝑗) = (#‘{𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = 𝑗}))
hashbc.4	⊢ (𝜑 → 𝐾 ∈ ℤ)

**Assertion**
Ref	Expression
hashbclem	⊢ (𝜑 → ((#‘(𝐴 ∪ {𝑧}))C𝐾) = (#‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (#‘𝑥) = 𝐾}))

Distinct variable groups: 𝑥,𝑗,𝑧,𝐴 𝑗,𝐾,𝑥 𝜑,𝑥 Allowed substitution hints: 𝜑(𝑧,𝑗) 𝐾(𝑧)

Proof of Theorem hashbclem Dummy variables 𝑢 𝑣 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		hashbc.4	. . . . 5 ⊢ (𝜑 → 𝐾 ∈ ℤ)
2		hashbc.3	. . . . 5 ⊢ (𝜑 → ∀𝑗 ∈ ℤ ((#‘𝐴)C𝑗) = (#‘{𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = 𝑗}))
3		oveq2 6612	. . . . . . 7 ⊢ (𝑗 = 𝐾 → ((#‘𝐴)C𝑗) = ((#‘𝐴)C𝐾))
4		eqeq2 2632	. . . . . . . . 9 ⊢ (𝑗 = 𝐾 → ((#‘𝑥) = 𝑗 ↔ (#‘𝑥) = 𝐾))
5	4	rabbidv 3177	. . . . . . . 8 ⊢ (𝑗 = 𝐾 → {𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = 𝑗} = {𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = 𝐾})
6	5	fveq2d 6152	. . . . . . 7 ⊢ (𝑗 = 𝐾 → (#‘{𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = 𝑗}) = (#‘{𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = 𝐾}))
7	3, 6	eqeq12d 2636	. . . . . 6 ⊢ (𝑗 = 𝐾 → (((#‘𝐴)C𝑗) = (#‘{𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = 𝑗}) ↔ ((#‘𝐴)C𝐾) = (#‘{𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = 𝐾})))
8	7	rspcv 3291	. . . . 5 ⊢ (𝐾 ∈ ℤ → (∀𝑗 ∈ ℤ ((#‘𝐴)C𝑗) = (#‘{𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = 𝑗}) → ((#‘𝐴)C𝐾) = (#‘{𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = 𝐾})))
9	1, 2, 8	sylc 65	. . . 4 ⊢ (𝜑 → ((#‘𝐴)C𝐾) = (#‘{𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = 𝐾}))
10		ssun1 3754	. . . . . . . . . . . . 13 ⊢ 𝐴 ⊆ (𝐴 ∪ {𝑧})
11		sspwb 4878	. . . . . . . . . . . . 13 ⊢ (𝐴 ⊆ (𝐴 ∪ {𝑧}) ↔ 𝒫 𝐴 ⊆ 𝒫 (𝐴 ∪ {𝑧}))
12	10, 11	mpbi 220	. . . . . . . . . . . 12 ⊢ 𝒫 𝐴 ⊆ 𝒫 (𝐴 ∪ {𝑧})
13	12	sseli 3579	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝒫 𝐴 → 𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}))
14	13	adantl 482	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝒫 𝐴) → 𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}))
15		hashbc.2	. . . . . . . . . . 11 ⊢ (𝜑 → ¬ 𝑧 ∈ 𝐴)
16		elpwi 4140	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ 𝒫 𝐴 → 𝑥 ⊆ 𝐴)
17	16	ssneld 3585	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝒫 𝐴 → (¬ 𝑧 ∈ 𝐴 → ¬ 𝑧 ∈ 𝑥))
18	15, 17	mpan9 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝒫 𝐴) → ¬ 𝑧 ∈ 𝑥)
19	14, 18	jca 554	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝒫 𝐴) → (𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧 ∈ 𝑥))
20		elpwi 4140	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) → 𝑥 ⊆ (𝐴 ∪ {𝑧}))
21		uncom 3735	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∪ {𝑧}) = ({𝑧} ∪ 𝐴)
22	20, 21	syl6sseq 3630	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) → 𝑥 ⊆ ({𝑧} ∪ 𝐴))
23	22	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧 ∈ 𝑥) → 𝑥 ⊆ ({𝑧} ∪ 𝐴))
24		simpr 477	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧 ∈ 𝑥) → ¬ 𝑧 ∈ 𝑥)
25		disjsn 4216	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∩ {𝑧}) = ∅ ↔ ¬ 𝑧 ∈ 𝑥)
26	24, 25	sylibr 224	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧 ∈ 𝑥) → (𝑥 ∩ {𝑧}) = ∅)
27		disjssun 4008	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∩ {𝑧}) = ∅ → (𝑥 ⊆ ({𝑧} ∪ 𝐴) ↔ 𝑥 ⊆ 𝐴))
28	26, 27	syl 17	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧 ∈ 𝑥) → (𝑥 ⊆ ({𝑧} ∪ 𝐴) ↔ 𝑥 ⊆ 𝐴))
29	23, 28	mpbid 222	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧 ∈ 𝑥) → 𝑥 ⊆ 𝐴)
30		vex 3189	. . . . . . . . . . . 12 ⊢ 𝑥 ∈ V
31	30	elpw 4136	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝒫 𝐴 ↔ 𝑥 ⊆ 𝐴)
32	29, 31	sylibr 224	. . . . . . . . . 10 ⊢ ((𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧 ∈ 𝑥) → 𝑥 ∈ 𝒫 𝐴)
33	32	adantl 482	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧 ∈ 𝑥)) → 𝑥 ∈ 𝒫 𝐴)
34	19, 33	impbida 876	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ 𝒫 𝐴 ↔ (𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧 ∈ 𝑥)))
35	34	anbi1d 740	. . . . . . 7 ⊢ (𝜑 → ((𝑥 ∈ 𝒫 𝐴 ∧ (#‘𝑥) = 𝐾) ↔ ((𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧 ∈ 𝑥) ∧ (#‘𝑥) = 𝐾)))
36		anass 680	. . . . . . 7 ⊢ (((𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧 ∈ 𝑥) ∧ (#‘𝑥) = 𝐾) ↔ (𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (¬ 𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)))
37	35, 36	syl6bb 276	. . . . . 6 ⊢ (𝜑 → ((𝑥 ∈ 𝒫 𝐴 ∧ (#‘𝑥) = 𝐾) ↔ (𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (¬ 𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾))))
38	37	rabbidva2 3174	. . . . 5 ⊢ (𝜑 → {𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = 𝐾} = {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)})
39	38	fveq2d 6152	. . . 4 ⊢ (𝜑 → (#‘{𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = 𝐾}) = (#‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)}))
40	9, 39	eqtrd 2655	. . 3 ⊢ (𝜑 → ((#‘𝐴)C𝐾) = (#‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)}))
41		peano2zm 11364	. . . . . 6 ⊢ (𝐾 ∈ ℤ → (𝐾 − 1) ∈ ℤ)
42	1, 41	syl 17	. . . . 5 ⊢ (𝜑 → (𝐾 − 1) ∈ ℤ)
43		oveq2 6612	. . . . . . 7 ⊢ (𝑗 = (𝐾 − 1) → ((#‘𝐴)C𝑗) = ((#‘𝐴)C(𝐾 − 1)))
44		eqeq2 2632	. . . . . . . . 9 ⊢ (𝑗 = (𝐾 − 1) → ((#‘𝑥) = 𝑗 ↔ (#‘𝑥) = (𝐾 − 1)))
45	44	rabbidv 3177	. . . . . . . 8 ⊢ (𝑗 = (𝐾 − 1) → {𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = 𝑗} = {𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)})
46	45	fveq2d 6152	. . . . . . 7 ⊢ (𝑗 = (𝐾 − 1) → (#‘{𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = 𝑗}) = (#‘{𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)}))
47	43, 46	eqeq12d 2636	. . . . . 6 ⊢ (𝑗 = (𝐾 − 1) → (((#‘𝐴)C𝑗) = (#‘{𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = 𝑗}) ↔ ((#‘𝐴)C(𝐾 − 1)) = (#‘{𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)})))
48	47	rspcv 3291	. . . . 5 ⊢ ((𝐾 − 1) ∈ ℤ → (∀𝑗 ∈ ℤ ((#‘𝐴)C𝑗) = (#‘{𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = 𝑗}) → ((#‘𝐴)C(𝐾 − 1)) = (#‘{𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)})))
49	42, 2, 48	sylc 65	. . . 4 ⊢ (𝜑 → ((#‘𝐴)C(𝐾 − 1)) = (#‘{𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)}))
50		hashbc.1	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ∈ Fin)
51		pwfi 8205	. . . . . . . 8 ⊢ (𝐴 ∈ Fin ↔ 𝒫 𝐴 ∈ Fin)
52	50, 51	sylib 208	. . . . . . 7 ⊢ (𝜑 → 𝒫 𝐴 ∈ Fin)
53		rabexg 4772	. . . . . . 7 ⊢ (𝒫 𝐴 ∈ Fin → {𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)} ∈ V)
54	52, 53	syl 17	. . . . . 6 ⊢ (𝜑 → {𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)} ∈ V)
55		snfi 7982	. . . . . . . . . 10 ⊢ {𝑧} ∈ Fin
56		unfi 8171	. . . . . . . . . 10 ⊢ ((𝐴 ∈ Fin ∧ {𝑧} ∈ Fin) → (𝐴 ∪ {𝑧}) ∈ Fin)
57	50, 55, 56	sylancl 693	. . . . . . . . 9 ⊢ (𝜑 → (𝐴 ∪ {𝑧}) ∈ Fin)
58		pwfi 8205	. . . . . . . . 9 ⊢ ((𝐴 ∪ {𝑧}) ∈ Fin ↔ 𝒫 (𝐴 ∪ {𝑧}) ∈ Fin)
59	57, 58	sylib 208	. . . . . . . 8 ⊢ (𝜑 → 𝒫 (𝐴 ∪ {𝑧}) ∈ Fin)
60		ssrab2 3666	. . . . . . . 8 ⊢ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)} ⊆ 𝒫 (𝐴 ∪ {𝑧})
61		ssfi 8124	. . . . . . . 8 ⊢ ((𝒫 (𝐴 ∪ {𝑧}) ∈ Fin ∧ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)} ⊆ 𝒫 (𝐴 ∪ {𝑧})) → {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)} ∈ Fin)
62	59, 60, 61	sylancl 693	. . . . . . 7 ⊢ (𝜑 → {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)} ∈ Fin)
63		elex 3198	. . . . . . 7 ⊢ ({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)} ∈ Fin → {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)} ∈ V)
64	62, 63	syl 17	. . . . . 6 ⊢ (𝜑 → {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)} ∈ V)
65		fveq2 6148	. . . . . . . . 9 ⊢ (𝑥 = 𝑢 → (#‘𝑥) = (#‘𝑢))
66	65	eqeq1d 2623	. . . . . . . 8 ⊢ (𝑥 = 𝑢 → ((#‘𝑥) = (𝐾 − 1) ↔ (#‘𝑢) = (𝐾 − 1)))
67	66	elrab 3346	. . . . . . 7 ⊢ (𝑢 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)} ↔ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1)))
68		elpwi 4140	. . . . . . . . . . . 12 ⊢ (𝑢 ∈ 𝒫 𝐴 → 𝑢 ⊆ 𝐴)
69	68	ad2antrl 763	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1))) → 𝑢 ⊆ 𝐴)
70		unss1 3760	. . . . . . . . . . 11 ⊢ (𝑢 ⊆ 𝐴 → (𝑢 ∪ {𝑧}) ⊆ (𝐴 ∪ {𝑧}))
71	69, 70	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1))) → (𝑢 ∪ {𝑧}) ⊆ (𝐴 ∪ {𝑧}))
72		vex 3189	. . . . . . . . . . . 12 ⊢ 𝑢 ∈ V
73		snex 4869	. . . . . . . . . . . 12 ⊢ {𝑧} ∈ V
74	72, 73	unex 6909	. . . . . . . . . . 11 ⊢ (𝑢 ∪ {𝑧}) ∈ V
75	74	elpw 4136	. . . . . . . . . 10 ⊢ ((𝑢 ∪ {𝑧}) ∈ 𝒫 (𝐴 ∪ {𝑧}) ↔ (𝑢 ∪ {𝑧}) ⊆ (𝐴 ∪ {𝑧}))
76	71, 75	sylibr 224	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1))) → (𝑢 ∪ {𝑧}) ∈ 𝒫 (𝐴 ∪ {𝑧}))
77	50	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1))) → 𝐴 ∈ Fin)
78		ssfi 8124	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ Fin ∧ 𝑢 ⊆ 𝐴) → 𝑢 ∈ Fin)
79	77, 69, 78	syl2anc 692	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1))) → 𝑢 ∈ Fin)
80	55	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1))) → {𝑧} ∈ Fin)
81	15	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1))) → ¬ 𝑧 ∈ 𝐴)
82	69, 81	ssneldd 3586	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1))) → ¬ 𝑧 ∈ 𝑢)
83		disjsn 4216	. . . . . . . . . . . . 13 ⊢ ((𝑢 ∩ {𝑧}) = ∅ ↔ ¬ 𝑧 ∈ 𝑢)
84	82, 83	sylibr 224	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1))) → (𝑢 ∩ {𝑧}) = ∅)
85		hashun 13111	. . . . . . . . . . . 12 ⊢ ((𝑢 ∈ Fin ∧ {𝑧} ∈ Fin ∧ (𝑢 ∩ {𝑧}) = ∅) → (#‘(𝑢 ∪ {𝑧})) = ((#‘𝑢) + (#‘{𝑧})))
86	79, 80, 84, 85	syl3anc 1323	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1))) → (#‘(𝑢 ∪ {𝑧})) = ((#‘𝑢) + (#‘{𝑧})))
87		simprr 795	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1))) → (#‘𝑢) = (𝐾 − 1))
88		vex 3189	. . . . . . . . . . . . . 14 ⊢ 𝑧 ∈ V
89		hashsng 13099	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ V → (#‘{𝑧}) = 1)
90	88, 89	ax-mp 5	. . . . . . . . . . . . 13 ⊢ (#‘{𝑧}) = 1
91	90	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1))) → (#‘{𝑧}) = 1)
92	87, 91	oveq12d 6622	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1))) → ((#‘𝑢) + (#‘{𝑧})) = ((𝐾 − 1) + 1))
93	1	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1))) → 𝐾 ∈ ℤ)
94	93	zcnd 11427	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1))) → 𝐾 ∈ ℂ)
95		ax-1cn 9938	. . . . . . . . . . . 12 ⊢ 1 ∈ ℂ
96		npcan 10234	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝐾 − 1) + 1) = 𝐾)
97	94, 95, 96	sylancl 693	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1))) → ((𝐾 − 1) + 1) = 𝐾)
98	86, 92, 97	3eqtrd 2659	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1))) → (#‘(𝑢 ∪ {𝑧})) = 𝐾)
99		ssun2 3755	. . . . . . . . . . 11 ⊢ {𝑧} ⊆ (𝑢 ∪ {𝑧})
100	88	snss 4286	. . . . . . . . . . 11 ⊢ (𝑧 ∈ (𝑢 ∪ {𝑧}) ↔ {𝑧} ⊆ (𝑢 ∪ {𝑧}))
101	99, 100	mpbir 221	. . . . . . . . . 10 ⊢ 𝑧 ∈ (𝑢 ∪ {𝑧})
102	98, 101	jctil 559	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1))) → (𝑧 ∈ (𝑢 ∪ {𝑧}) ∧ (#‘(𝑢 ∪ {𝑧})) = 𝐾))
103		eleq2 2687	. . . . . . . . . . 11 ⊢ (𝑥 = (𝑢 ∪ {𝑧}) → (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ (𝑢 ∪ {𝑧})))
104		fveq2 6148	. . . . . . . . . . . 12 ⊢ (𝑥 = (𝑢 ∪ {𝑧}) → (#‘𝑥) = (#‘(𝑢 ∪ {𝑧})))
105	104	eqeq1d 2623	. . . . . . . . . . 11 ⊢ (𝑥 = (𝑢 ∪ {𝑧}) → ((#‘𝑥) = 𝐾 ↔ (#‘(𝑢 ∪ {𝑧})) = 𝐾))
106	103, 105	anbi12d 746	. . . . . . . . . 10 ⊢ (𝑥 = (𝑢 ∪ {𝑧}) → ((𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾) ↔ (𝑧 ∈ (𝑢 ∪ {𝑧}) ∧ (#‘(𝑢 ∪ {𝑧})) = 𝐾)))
107	106	elrab 3346	. . . . . . . . 9 ⊢ ((𝑢 ∪ {𝑧}) ∈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)} ↔ ((𝑢 ∪ {𝑧}) ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ (𝑢 ∪ {𝑧}) ∧ (#‘(𝑢 ∪ {𝑧})) = 𝐾)))
108	76, 102, 107	sylanbrc 697	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1))) → (𝑢 ∪ {𝑧}) ∈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)})
109	108	ex 450	. . . . . . 7 ⊢ (𝜑 → ((𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1)) → (𝑢 ∪ {𝑧}) ∈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)}))
110	67, 109	syl5bi 232	. . . . . 6 ⊢ (𝜑 → (𝑢 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)} → (𝑢 ∪ {𝑧}) ∈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)}))
111		eleq2 2687	. . . . . . . . 9 ⊢ (𝑥 = 𝑣 → (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑣))
112		fveq2 6148	. . . . . . . . . 10 ⊢ (𝑥 = 𝑣 → (#‘𝑥) = (#‘𝑣))
113	112	eqeq1d 2623	. . . . . . . . 9 ⊢ (𝑥 = 𝑣 → ((#‘𝑥) = 𝐾 ↔ (#‘𝑣) = 𝐾))
114	111, 113	anbi12d 746	. . . . . . . 8 ⊢ (𝑥 = 𝑣 → ((𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾) ↔ (𝑧 ∈ 𝑣 ∧ (#‘𝑣) = 𝐾)))
115	114	elrab 3346	. . . . . . 7 ⊢ (𝑣 ∈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)} ↔ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (#‘𝑣) = 𝐾)))
116		elpwi 4140	. . . . . . . . . . . . 13 ⊢ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) → 𝑣 ⊆ (𝐴 ∪ {𝑧}))
117	116	ad2antrl 763	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (#‘𝑣) = 𝐾))) → 𝑣 ⊆ (𝐴 ∪ {𝑧}))
118	117, 21	syl6sseq 3630	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (#‘𝑣) = 𝐾))) → 𝑣 ⊆ ({𝑧} ∪ 𝐴))
119		ssundif 4024	. . . . . . . . . . 11 ⊢ (𝑣 ⊆ ({𝑧} ∪ 𝐴) ↔ (𝑣 ∖ {𝑧}) ⊆ 𝐴)
120	118, 119	sylib 208	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (#‘𝑣) = 𝐾))) → (𝑣 ∖ {𝑧}) ⊆ 𝐴)
121		vex 3189	. . . . . . . . . . . 12 ⊢ 𝑣 ∈ V
122		difexg 4768	. . . . . . . . . . . 12 ⊢ (𝑣 ∈ V → (𝑣 ∖ {𝑧}) ∈ V)
123	121, 122	ax-mp 5	. . . . . . . . . . 11 ⊢ (𝑣 ∖ {𝑧}) ∈ V
124	123	elpw 4136	. . . . . . . . . 10 ⊢ ((𝑣 ∖ {𝑧}) ∈ 𝒫 𝐴 ↔ (𝑣 ∖ {𝑧}) ⊆ 𝐴)
125	120, 124	sylibr 224	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (#‘𝑣) = 𝐾))) → (𝑣 ∖ {𝑧}) ∈ 𝒫 𝐴)
126	50	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (#‘𝑣) = 𝐾))) → 𝐴 ∈ Fin)
127		ssfi 8124	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ Fin ∧ (𝑣 ∖ {𝑧}) ⊆ 𝐴) → (𝑣 ∖ {𝑧}) ∈ Fin)
128	126, 120, 127	syl2anc 692	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (#‘𝑣) = 𝐾))) → (𝑣 ∖ {𝑧}) ∈ Fin)
129		hashcl 13087	. . . . . . . . . . . . 13 ⊢ ((𝑣 ∖ {𝑧}) ∈ Fin → (#‘(𝑣 ∖ {𝑧})) ∈ ℕ₀)
130	128, 129	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (#‘𝑣) = 𝐾))) → (#‘(𝑣 ∖ {𝑧})) ∈ ℕ₀)
131	130	nn0cnd 11297	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (#‘𝑣) = 𝐾))) → (#‘(𝑣 ∖ {𝑧})) ∈ ℂ)
132		pncan 10231	. . . . . . . . . . 11 ⊢ (((#‘(𝑣 ∖ {𝑧})) ∈ ℂ ∧ 1 ∈ ℂ) → (((#‘(𝑣 ∖ {𝑧})) + 1) − 1) = (#‘(𝑣 ∖ {𝑧})))
133	131, 95, 132	sylancl 693	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (#‘𝑣) = 𝐾))) → (((#‘(𝑣 ∖ {𝑧})) + 1) − 1) = (#‘(𝑣 ∖ {𝑧})))
134		undif1 4015	. . . . . . . . . . . . . 14 ⊢ ((𝑣 ∖ {𝑧}) ∪ {𝑧}) = (𝑣 ∪ {𝑧})
135		simprrl 803	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (#‘𝑣) = 𝐾))) → 𝑧 ∈ 𝑣)
136	135	snssd 4309	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (#‘𝑣) = 𝐾))) → {𝑧} ⊆ 𝑣)
137		ssequn2 3764	. . . . . . . . . . . . . . 15 ⊢ ({𝑧} ⊆ 𝑣 ↔ (𝑣 ∪ {𝑧}) = 𝑣)
138	136, 137	sylib 208	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (#‘𝑣) = 𝐾))) → (𝑣 ∪ {𝑧}) = 𝑣)
139	134, 138	syl5eq 2667	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (#‘𝑣) = 𝐾))) → ((𝑣 ∖ {𝑧}) ∪ {𝑧}) = 𝑣)
140	139	fveq2d 6152	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (#‘𝑣) = 𝐾))) → (#‘((𝑣 ∖ {𝑧}) ∪ {𝑧})) = (#‘𝑣))
141	55	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (#‘𝑣) = 𝐾))) → {𝑧} ∈ Fin)
142		incom 3783	. . . . . . . . . . . . . . . 16 ⊢ ((𝑣 ∖ {𝑧}) ∩ {𝑧}) = ({𝑧} ∩ (𝑣 ∖ {𝑧}))
143		disjdif 4012	. . . . . . . . . . . . . . . 16 ⊢ ({𝑧} ∩ (𝑣 ∖ {𝑧})) = ∅
144	142, 143	eqtri 2643	. . . . . . . . . . . . . . 15 ⊢ ((𝑣 ∖ {𝑧}) ∩ {𝑧}) = ∅
145	144	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (#‘𝑣) = 𝐾))) → ((𝑣 ∖ {𝑧}) ∩ {𝑧}) = ∅)
146		hashun 13111	. . . . . . . . . . . . . 14 ⊢ (((𝑣 ∖ {𝑧}) ∈ Fin ∧ {𝑧} ∈ Fin ∧ ((𝑣 ∖ {𝑧}) ∩ {𝑧}) = ∅) → (#‘((𝑣 ∖ {𝑧}) ∪ {𝑧})) = ((#‘(𝑣 ∖ {𝑧})) + (#‘{𝑧})))
147	128, 141, 145, 146	syl3anc 1323	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (#‘𝑣) = 𝐾))) → (#‘((𝑣 ∖ {𝑧}) ∪ {𝑧})) = ((#‘(𝑣 ∖ {𝑧})) + (#‘{𝑧})))
148	90	oveq2i 6615	. . . . . . . . . . . . 13 ⊢ ((#‘(𝑣 ∖ {𝑧})) + (#‘{𝑧})) = ((#‘(𝑣 ∖ {𝑧})) + 1)
149	147, 148	syl6eq 2671	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (#‘𝑣) = 𝐾))) → (#‘((𝑣 ∖ {𝑧}) ∪ {𝑧})) = ((#‘(𝑣 ∖ {𝑧})) + 1))
150		simprrr 804	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (#‘𝑣) = 𝐾))) → (#‘𝑣) = 𝐾)
151	140, 149, 150	3eqtr3d 2663	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (#‘𝑣) = 𝐾))) → ((#‘(𝑣 ∖ {𝑧})) + 1) = 𝐾)
152	151	oveq1d 6619	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (#‘𝑣) = 𝐾))) → (((#‘(𝑣 ∖ {𝑧})) + 1) − 1) = (𝐾 − 1))
153	133, 152	eqtr3d 2657	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (#‘𝑣) = 𝐾))) → (#‘(𝑣 ∖ {𝑧})) = (𝐾 − 1))
154		fveq2 6148	. . . . . . . . . . 11 ⊢ (𝑥 = (𝑣 ∖ {𝑧}) → (#‘𝑥) = (#‘(𝑣 ∖ {𝑧})))
155	154	eqeq1d 2623	. . . . . . . . . 10 ⊢ (𝑥 = (𝑣 ∖ {𝑧}) → ((#‘𝑥) = (𝐾 − 1) ↔ (#‘(𝑣 ∖ {𝑧})) = (𝐾 − 1)))
156	155	elrab 3346	. . . . . . . . 9 ⊢ ((𝑣 ∖ {𝑧}) ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)} ↔ ((𝑣 ∖ {𝑧}) ∈ 𝒫 𝐴 ∧ (#‘(𝑣 ∖ {𝑧})) = (𝐾 − 1)))
157	125, 153, 156	sylanbrc 697	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (#‘𝑣) = 𝐾))) → (𝑣 ∖ {𝑧}) ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)})
158	157	ex 450	. . . . . . 7 ⊢ (𝜑 → ((𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (#‘𝑣) = 𝐾)) → (𝑣 ∖ {𝑧}) ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)}))
159	115, 158	syl5bi 232	. . . . . 6 ⊢ (𝜑 → (𝑣 ∈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)} → (𝑣 ∖ {𝑧}) ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)}))
160	67, 115	anbi12i 732	. . . . . . 7 ⊢ ((𝑢 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)} ∧ 𝑣 ∈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)}) ↔ ((𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1)) ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (#‘𝑣) = 𝐾))))
161		simp3rl 1132	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1)) ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (#‘𝑣) = 𝐾))) → 𝑧 ∈ 𝑣)
162	161	snssd 4309	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1)) ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (#‘𝑣) = 𝐾))) → {𝑧} ⊆ 𝑣)
163		incom 3783	. . . . . . . . . . . 12 ⊢ ({𝑧} ∩ 𝑢) = (𝑢 ∩ {𝑧})
164	84	3adant3 1079	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1)) ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (#‘𝑣) = 𝐾))) → (𝑢 ∩ {𝑧}) = ∅)
165	163, 164	syl5eq 2667	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1)) ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (#‘𝑣) = 𝐾))) → ({𝑧} ∩ 𝑢) = ∅)
166		uneqdifeq 4029	. . . . . . . . . . 11 ⊢ (({𝑧} ⊆ 𝑣 ∧ ({𝑧} ∩ 𝑢) = ∅) → (({𝑧} ∪ 𝑢) = 𝑣 ↔ (𝑣 ∖ {𝑧}) = 𝑢))
167	162, 165, 166	syl2anc 692	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1)) ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (#‘𝑣) = 𝐾))) → (({𝑧} ∪ 𝑢) = 𝑣 ↔ (𝑣 ∖ {𝑧}) = 𝑢))
168	167	bicomd 213	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1)) ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (#‘𝑣) = 𝐾))) → ((𝑣 ∖ {𝑧}) = 𝑢 ↔ ({𝑧} ∪ 𝑢) = 𝑣))
169		eqcom 2628	. . . . . . . . 9 ⊢ (𝑢 = (𝑣 ∖ {𝑧}) ↔ (𝑣 ∖ {𝑧}) = 𝑢)
170		eqcom 2628	. . . . . . . . . 10 ⊢ (𝑣 = (𝑢 ∪ {𝑧}) ↔ (𝑢 ∪ {𝑧}) = 𝑣)
171		uncom 3735	. . . . . . . . . . 11 ⊢ (𝑢 ∪ {𝑧}) = ({𝑧} ∪ 𝑢)
172	171	eqeq1i 2626	. . . . . . . . . 10 ⊢ ((𝑢 ∪ {𝑧}) = 𝑣 ↔ ({𝑧} ∪ 𝑢) = 𝑣)
173	170, 172	bitri 264	. . . . . . . . 9 ⊢ (𝑣 = (𝑢 ∪ {𝑧}) ↔ ({𝑧} ∪ 𝑢) = 𝑣)
174	168, 169, 173	3bitr4g 303	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1)) ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (#‘𝑣) = 𝐾))) → (𝑢 = (𝑣 ∖ {𝑧}) ↔ 𝑣 = (𝑢 ∪ {𝑧})))
175	174	3expib 1265	. . . . . . 7 ⊢ (𝜑 → (((𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1)) ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (#‘𝑣) = 𝐾))) → (𝑢 = (𝑣 ∖ {𝑧}) ↔ 𝑣 = (𝑢 ∪ {𝑧}))))
176	160, 175	syl5bi 232	. . . . . 6 ⊢ (𝜑 → ((𝑢 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)} ∧ 𝑣 ∈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)}) → (𝑢 = (𝑣 ∖ {𝑧}) ↔ 𝑣 = (𝑢 ∪ {𝑧}))))
177	54, 64, 110, 159, 176	en3d 7936	. . . . 5 ⊢ (𝜑 → {𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)} ≈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)})
178		ssrab2 3666	. . . . . . 7 ⊢ {𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)} ⊆ 𝒫 𝐴
179		ssfi 8124	. . . . . . 7 ⊢ ((𝒫 𝐴 ∈ Fin ∧ {𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)} ⊆ 𝒫 𝐴) → {𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)} ∈ Fin)
180	52, 178, 179	sylancl 693	. . . . . 6 ⊢ (𝜑 → {𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)} ∈ Fin)
181		hashen 13075	. . . . . 6 ⊢ (({𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)} ∈ Fin ∧ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)} ∈ Fin) → ((#‘{𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)}) = (#‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)}) ↔ {𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)} ≈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)}))
182	180, 62, 181	syl2anc 692	. . . . 5 ⊢ (𝜑 → ((#‘{𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)}) = (#‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)}) ↔ {𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)} ≈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)}))
183	177, 182	mpbird 247	. . . 4 ⊢ (𝜑 → (#‘{𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)}) = (#‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)}))
184	49, 183	eqtrd 2655	. . 3 ⊢ (𝜑 → ((#‘𝐴)C(𝐾 − 1)) = (#‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)}))
185	40, 184	oveq12d 6622	. 2 ⊢ (𝜑 → (((#‘𝐴)C𝐾) + ((#‘𝐴)C(𝐾 − 1))) = ((#‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)}) + (#‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)})))
186	55	a1i 11	. . . . . 6 ⊢ (𝜑 → {𝑧} ∈ Fin)
187		disjsn 4216	. . . . . . 7 ⊢ ((𝐴 ∩ {𝑧}) = ∅ ↔ ¬ 𝑧 ∈ 𝐴)
188	15, 187	sylibr 224	. . . . . 6 ⊢ (𝜑 → (𝐴 ∩ {𝑧}) = ∅)
189		hashun 13111	. . . . . 6 ⊢ ((𝐴 ∈ Fin ∧ {𝑧} ∈ Fin ∧ (𝐴 ∩ {𝑧}) = ∅) → (#‘(𝐴 ∪ {𝑧})) = ((#‘𝐴) + (#‘{𝑧})))
190	50, 186, 188, 189	syl3anc 1323	. . . . 5 ⊢ (𝜑 → (#‘(𝐴 ∪ {𝑧})) = ((#‘𝐴) + (#‘{𝑧})))
191	90	oveq2i 6615	. . . . 5 ⊢ ((#‘𝐴) + (#‘{𝑧})) = ((#‘𝐴) + 1)
192	190, 191	syl6eq 2671	. . . 4 ⊢ (𝜑 → (#‘(𝐴 ∪ {𝑧})) = ((#‘𝐴) + 1))
193	192	oveq1d 6619	. . 3 ⊢ (𝜑 → ((#‘(𝐴 ∪ {𝑧}))C𝐾) = (((#‘𝐴) + 1)C𝐾))
194		hashcl 13087	. . . . 5 ⊢ (𝐴 ∈ Fin → (#‘𝐴) ∈ ℕ₀)
195	50, 194	syl 17	. . . 4 ⊢ (𝜑 → (#‘𝐴) ∈ ℕ₀)
196		bcpasc 13048	. . . 4 ⊢ (((#‘𝐴) ∈ ℕ₀ ∧ 𝐾 ∈ ℤ) → (((#‘𝐴)C𝐾) + ((#‘𝐴)C(𝐾 − 1))) = (((#‘𝐴) + 1)C𝐾))
197	195, 1, 196	syl2anc 692	. . 3 ⊢ (𝜑 → (((#‘𝐴)C𝐾) + ((#‘𝐴)C(𝐾 − 1))) = (((#‘𝐴) + 1)C𝐾))
198	193, 197	eqtr4d 2658	. 2 ⊢ (𝜑 → ((#‘(𝐴 ∪ {𝑧}))C𝐾) = (((#‘𝐴)C𝐾) + ((#‘𝐴)C(𝐾 − 1))))
199		pm2.1 433	. . . . . . . . 9 ⊢ (¬ 𝑧 ∈ 𝑥 ∨ 𝑧 ∈ 𝑥)
200	199	biantrur 527	. . . . . . . 8 ⊢ ((#‘𝑥) = 𝐾 ↔ ((¬ 𝑧 ∈ 𝑥 ∨ 𝑧 ∈ 𝑥) ∧ (#‘𝑥) = 𝐾))
201		andir 911	. . . . . . . 8 ⊢ (((¬ 𝑧 ∈ 𝑥 ∨ 𝑧 ∈ 𝑥) ∧ (#‘𝑥) = 𝐾) ↔ ((¬ 𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾) ∨ (𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)))
202	200, 201	bitri 264	. . . . . . 7 ⊢ ((#‘𝑥) = 𝐾 ↔ ((¬ 𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾) ∨ (𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)))
203	202	a1i 11	. . . . . 6 ⊢ (𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) → ((#‘𝑥) = 𝐾 ↔ ((¬ 𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾) ∨ (𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾))))
204	203	rabbiia 3173	. . . . 5 ⊢ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (#‘𝑥) = 𝐾} = {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ ((¬ 𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾) ∨ (𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾))}
205		unrab 3874	. . . . 5 ⊢ ({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)} ∪ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)}) = {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ ((¬ 𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾) ∨ (𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾))}
206	204, 205	eqtr4i 2646	. . . 4 ⊢ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (#‘𝑥) = 𝐾} = ({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)} ∪ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)})
207	206	fveq2i 6151	. . 3 ⊢ (#‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (#‘𝑥) = 𝐾}) = (#‘({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)} ∪ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)}))
208		ssrab2 3666	. . . . 5 ⊢ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)} ⊆ 𝒫 (𝐴 ∪ {𝑧})
209		ssfi 8124	. . . . 5 ⊢ ((𝒫 (𝐴 ∪ {𝑧}) ∈ Fin ∧ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)} ⊆ 𝒫 (𝐴 ∪ {𝑧})) → {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)} ∈ Fin)
210	59, 208, 209	sylancl 693	. . . 4 ⊢ (𝜑 → {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)} ∈ Fin)
211		inrab 3875	. . . . . 6 ⊢ ({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)} ∩ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)}) = {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ ((¬ 𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾) ∧ (𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾))}
212		simprl 793	. . . . . . . . 9 ⊢ (((¬ 𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾) ∧ (𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)) → 𝑧 ∈ 𝑥)
213		simpll 789	. . . . . . . . 9 ⊢ (((¬ 𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾) ∧ (𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)) → ¬ 𝑧 ∈ 𝑥)
214	212, 213	pm2.65i 185	. . . . . . . 8 ⊢ ¬ ((¬ 𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾) ∧ (𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾))
215	214	rgenw 2919	. . . . . . 7 ⊢ ∀𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ¬ ((¬ 𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾) ∧ (𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾))
216		rabeq0 3931	. . . . . . 7 ⊢ ({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ ((¬ 𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾) ∧ (𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾))} = ∅ ↔ ∀𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ¬ ((¬ 𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾) ∧ (𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)))
217	215, 216	mpbir 221	. . . . . 6 ⊢ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ ((¬ 𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾) ∧ (𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾))} = ∅
218	211, 217	eqtri 2643	. . . . 5 ⊢ ({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)} ∩ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)}) = ∅
219	218	a1i 11	. . . 4 ⊢ (𝜑 → ({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)} ∩ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)}) = ∅)
220		hashun 13111	. . . 4 ⊢ (({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)} ∈ Fin ∧ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)} ∈ Fin ∧ ({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)} ∩ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)}) = ∅) → (#‘({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)} ∪ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)})) = ((#‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)}) + (#‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)})))
221	210, 62, 219, 220	syl3anc 1323	. . 3 ⊢ (𝜑 → (#‘({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)} ∪ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)})) = ((#‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)}) + (#‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)})))
222	207, 221	syl5eq 2667	. 2 ⊢ (𝜑 → (#‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (#‘𝑥) = 𝐾}) = ((#‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)}) + (#‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)})))
223	185, 198, 222	3eqtr4d 2665	1 ⊢ (𝜑 → ((#‘(𝐴 ∪ {𝑧}))C𝐾) = (#‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (#‘𝑥) = 𝐾}))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 196 ∨ wo 383 ∧ wa 384 ∧ w3a 1036 = wceq 1480 ∈ wcel 1987 ∀wral 2907 {crab 2911 Vcvv 3186 ∖ cdif 3552 ∪ cun 3553 ∩ cin 3554 ⊆ wss 3555 ∅c0 3891 𝒫 cpw 4130 {csn 4148 class class class wbr 4613 ‘cfv 5847 (class class class)co 6604 ≈ cen 7896 Fincfn 7899 ℂcc 9878 1c1 9881 + caddc 9883 − cmin 10210 ℕ₀cn0 11236 ℤcz 11321 Ccbc 13029 #chash 13057

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1719 ax-4 1734 ax-5 1836 ax-6 1885 ax-7 1932 ax-8 1989 ax-9 1996 ax-10 2016 ax-11 2031 ax-12 2044 ax-13 2245 ax-ext 2601 ax-rep 4731 ax-sep 4741 ax-nul 4749 ax-pow 4803 ax-pr 4867 ax-un 6902 ax-cnex 9936 ax-resscn 9937 ax-1cn 9938 ax-icn 9939 ax-addcl 9940 ax-addrcl 9941 ax-mulcl 9942 ax-mulrcl 9943 ax-mulcom 9944 ax-addass 9945 ax-mulass 9946 ax-distr 9947 ax-i2m1 9948 ax-1ne0 9949 ax-1rid 9950 ax-rnegex 9951 ax-rrecex 9952 ax-cnre 9953 ax-pre-lttri 9954 ax-pre-lttrn 9955 ax-pre-ltadd 9956 ax-pre-mulgt0 9957

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1037 df-3an 1038 df-tru 1483 df-ex 1702 df-nf 1707 df-sb 1878 df-eu 2473 df-mo 2474 df-clab 2608 df-cleq 2614 df-clel 2617 df-nfc 2750 df-ne 2791 df-nel 2894 df-ral 2912 df-rex 2913 df-reu 2914 df-rmo 2915 df-rab 2916 df-v 3188 df-sbc 3418 df-csb 3515 df-dif 3558 df-un 3560 df-in 3562 df-ss 3569 df-pss 3571 df-nul 3892 df-if 4059 df-pw 4132 df-sn 4149 df-pr 4151 df-tp 4153 df-op 4155 df-uni 4403 df-int 4441 df-iun 4487 df-br 4614 df-opab 4674 df-mpt 4675 df-tr 4713 df-eprel 4985 df-id 4989 df-po 4995 df-so 4996 df-fr 5033 df-we 5035 df-xp 5080 df-rel 5081 df-cnv 5082 df-co 5083 df-dm 5084 df-rn 5085 df-res 5086 df-ima 5087 df-pred 5639 df-ord 5685 df-on 5686 df-lim 5687 df-suc 5688 df-iota 5810 df-fun 5849 df-fn 5850 df-f 5851 df-f1 5852 df-fo 5853 df-f1o 5854 df-fv 5855 df-riota 6565 df-ov 6607 df-oprab 6608 df-mpt2 6609 df-om 7013 df-1st 7113 df-2nd 7114 df-wrecs 7352 df-recs 7413 df-rdg 7451 df-1o 7505 df-2o 7506 df-oadd 7509 df-er 7687 df-map 7804 df-en 7900 df-dom 7901 df-sdom 7902 df-fin 7903 df-card 8709 df-cda 8934 df-pnf 10020 df-mnf 10021 df-xr 10022 df-ltxr 10023 df-le 10024 df-sub 10212 df-neg 10213 df-div 10629 df-nn 10965 df-n0 11237 df-z 11322 df-uz 11632 df-rp 11777 df-fz 12269 df-seq 12742 df-fac 13001 df-bc 13030 df-hash 13058

This theorem is referenced by: hashbc 13175

W3C validator