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 13236

Description: Lemma for hashbc 13237: 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 6658	. . . . . . 7 ⊢ (𝑗 = 𝐾 → ((#‘𝐴)C𝑗) = ((#‘𝐴)C𝐾))
4		eqeq2 2633	. . . . . . . . 9 ⊢ (𝑗 = 𝐾 → ((#‘𝑥) = 𝑗 ↔ (#‘𝑥) = 𝐾))
5	4	rabbidv 3189	. . . . . . . 8 ⊢ (𝑗 = 𝐾 → {𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = 𝑗} = {𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = 𝐾})
6	5	fveq2d 6195	. . . . . . 7 ⊢ (𝑗 = 𝐾 → (#‘{𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = 𝑗}) = (#‘{𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = 𝐾}))
7	3, 6	eqeq12d 2637	. . . . . 6 ⊢ (𝑗 = 𝐾 → (((#‘𝐴)C𝑗) = (#‘{𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = 𝑗}) ↔ ((#‘𝐴)C𝐾) = (#‘{𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = 𝐾})))
8	7	rspcv 3305	. . . . 5 ⊢ (𝐾 ∈ ℤ → (∀𝑗 ∈ ℤ ((#‘𝐴)C𝑗) = (#‘{𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = 𝑗}) → ((#‘𝐴)C𝐾) = (#‘{𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = 𝐾})))
9	1, 2, 8	sylc 65	. . . 4 ⊢ (𝜑 → ((#‘𝐴)C𝐾) = (#‘{𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = 𝐾}))
10		ssun1 3776	. . . . . . . . . . . . 13 ⊢ 𝐴 ⊆ (𝐴 ∪ {𝑧})
11		sspwb 4917	. . . . . . . . . . . . 13 ⊢ (𝐴 ⊆ (𝐴 ∪ {𝑧}) ↔ 𝒫 𝐴 ⊆ 𝒫 (𝐴 ∪ {𝑧}))
12	10, 11	mpbi 220	. . . . . . . . . . . 12 ⊢ 𝒫 𝐴 ⊆ 𝒫 (𝐴 ∪ {𝑧})
13	12	sseli 3599	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝒫 𝐴 → 𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}))
14	13	adantl 482	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝒫 𝐴) → 𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}))
15		hashbc.2	. . . . . . . . . . 11 ⊢ (𝜑 → ¬ 𝑧 ∈ 𝐴)
16		elpwi 4168	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ 𝒫 𝐴 → 𝑥 ⊆ 𝐴)
17	16	ssneld 3605	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝒫 𝐴 → (¬ 𝑧 ∈ 𝐴 → ¬ 𝑧 ∈ 𝑥))
18	15, 17	mpan9 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝒫 𝐴) → ¬ 𝑧 ∈ 𝑥)
19	14, 18	jca 554	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝒫 𝐴) → (𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧 ∈ 𝑥))
20		elpwi 4168	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) → 𝑥 ⊆ (𝐴 ∪ {𝑧}))
21		uncom 3757	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∪ {𝑧}) = ({𝑧} ∪ 𝐴)
22	20, 21	syl6sseq 3651	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) → 𝑥 ⊆ ({𝑧} ∪ 𝐴))
23	22	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧 ∈ 𝑥) → 𝑥 ⊆ ({𝑧} ∪ 𝐴))
24		simpr 477	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧 ∈ 𝑥) → ¬ 𝑧 ∈ 𝑥)
25		disjsn 4246	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∩ {𝑧}) = ∅ ↔ ¬ 𝑧 ∈ 𝑥)
26	24, 25	sylibr 224	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧 ∈ 𝑥) → (𝑥 ∩ {𝑧}) = ∅)
27		disjssun 4036	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∩ {𝑧}) = ∅ → (𝑥 ⊆ ({𝑧} ∪ 𝐴) ↔ 𝑥 ⊆ 𝐴))
28	26, 27	syl 17	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧 ∈ 𝑥) → (𝑥 ⊆ ({𝑧} ∪ 𝐴) ↔ 𝑥 ⊆ 𝐴))
29	23, 28	mpbid 222	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧 ∈ 𝑥) → 𝑥 ⊆ 𝐴)
30		vex 3203	. . . . . . . . . . . 12 ⊢ 𝑥 ∈ V
31	30	elpw 4164	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝒫 𝐴 ↔ 𝑥 ⊆ 𝐴)
32	29, 31	sylibr 224	. . . . . . . . . 10 ⊢ ((𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧 ∈ 𝑥) → 𝑥 ∈ 𝒫 𝐴)
33	32	adantl 482	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧 ∈ 𝑥)) → 𝑥 ∈ 𝒫 𝐴)
34	19, 33	impbida 877	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ 𝒫 𝐴 ↔ (𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧 ∈ 𝑥)))
35	34	anbi1d 741	. . . . . . 7 ⊢ (𝜑 → ((𝑥 ∈ 𝒫 𝐴 ∧ (#‘𝑥) = 𝐾) ↔ ((𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧 ∈ 𝑥) ∧ (#‘𝑥) = 𝐾)))
36		anass 681	. . . . . . 7 ⊢ (((𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧 ∈ 𝑥) ∧ (#‘𝑥) = 𝐾) ↔ (𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (¬ 𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)))
37	35, 36	syl6bb 276	. . . . . 6 ⊢ (𝜑 → ((𝑥 ∈ 𝒫 𝐴 ∧ (#‘𝑥) = 𝐾) ↔ (𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (¬ 𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾))))
38	37	rabbidva2 3186	. . . . 5 ⊢ (𝜑 → {𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = 𝐾} = {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)})
39	38	fveq2d 6195	. . . 4 ⊢ (𝜑 → (#‘{𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = 𝐾}) = (#‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)}))
40	9, 39	eqtrd 2656	. . 3 ⊢ (𝜑 → ((#‘𝐴)C𝐾) = (#‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)}))
41		peano2zm 11420	. . . . . 6 ⊢ (𝐾 ∈ ℤ → (𝐾 − 1) ∈ ℤ)
42	1, 41	syl 17	. . . . 5 ⊢ (𝜑 → (𝐾 − 1) ∈ ℤ)
43		oveq2 6658	. . . . . . 7 ⊢ (𝑗 = (𝐾 − 1) → ((#‘𝐴)C𝑗) = ((#‘𝐴)C(𝐾 − 1)))
44		eqeq2 2633	. . . . . . . . 9 ⊢ (𝑗 = (𝐾 − 1) → ((#‘𝑥) = 𝑗 ↔ (#‘𝑥) = (𝐾 − 1)))
45	44	rabbidv 3189	. . . . . . . 8 ⊢ (𝑗 = (𝐾 − 1) → {𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = 𝑗} = {𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)})
46	45	fveq2d 6195	. . . . . . 7 ⊢ (𝑗 = (𝐾 − 1) → (#‘{𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = 𝑗}) = (#‘{𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)}))
47	43, 46	eqeq12d 2637	. . . . . 6 ⊢ (𝑗 = (𝐾 − 1) → (((#‘𝐴)C𝑗) = (#‘{𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = 𝑗}) ↔ ((#‘𝐴)C(𝐾 − 1)) = (#‘{𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)})))
48	47	rspcv 3305	. . . . 5 ⊢ ((𝐾 − 1) ∈ ℤ → (∀𝑗 ∈ ℤ ((#‘𝐴)C𝑗) = (#‘{𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = 𝑗}) → ((#‘𝐴)C(𝐾 − 1)) = (#‘{𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)})))
49	42, 2, 48	sylc 65	. . . 4 ⊢ (𝜑 → ((#‘𝐴)C(𝐾 − 1)) = (#‘{𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)}))
50		hashbc.1	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ∈ Fin)
51		pwfi 8261	. . . . . . . 8 ⊢ (𝐴 ∈ Fin ↔ 𝒫 𝐴 ∈ Fin)
52	50, 51	sylib 208	. . . . . . 7 ⊢ (𝜑 → 𝒫 𝐴 ∈ Fin)
53		rabexg 4812	. . . . . . 7 ⊢ (𝒫 𝐴 ∈ Fin → {𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)} ∈ V)
54	52, 53	syl 17	. . . . . 6 ⊢ (𝜑 → {𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)} ∈ V)
55		snfi 8038	. . . . . . . . . 10 ⊢ {𝑧} ∈ Fin
56		unfi 8227	. . . . . . . . . 10 ⊢ ((𝐴 ∈ Fin ∧ {𝑧} ∈ Fin) → (𝐴 ∪ {𝑧}) ∈ Fin)
57	50, 55, 56	sylancl 694	. . . . . . . . 9 ⊢ (𝜑 → (𝐴 ∪ {𝑧}) ∈ Fin)
58		pwfi 8261	. . . . . . . . 9 ⊢ ((𝐴 ∪ {𝑧}) ∈ Fin ↔ 𝒫 (𝐴 ∪ {𝑧}) ∈ Fin)
59	57, 58	sylib 208	. . . . . . . 8 ⊢ (𝜑 → 𝒫 (𝐴 ∪ {𝑧}) ∈ Fin)
60		ssrab2 3687	. . . . . . . 8 ⊢ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)} ⊆ 𝒫 (𝐴 ∪ {𝑧})
61		ssfi 8180	. . . . . . . 8 ⊢ ((𝒫 (𝐴 ∪ {𝑧}) ∈ Fin ∧ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)} ⊆ 𝒫 (𝐴 ∪ {𝑧})) → {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)} ∈ Fin)
62	59, 60, 61	sylancl 694	. . . . . . 7 ⊢ (𝜑 → {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)} ∈ Fin)
63		elex 3212	. . . . . . 7 ⊢ ({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)} ∈ Fin → {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)} ∈ V)
64	62, 63	syl 17	. . . . . 6 ⊢ (𝜑 → {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)} ∈ V)
65		fveq2 6191	. . . . . . . . 9 ⊢ (𝑥 = 𝑢 → (#‘𝑥) = (#‘𝑢))
66	65	eqeq1d 2624	. . . . . . . 8 ⊢ (𝑥 = 𝑢 → ((#‘𝑥) = (𝐾 − 1) ↔ (#‘𝑢) = (𝐾 − 1)))
67	66	elrab 3363	. . . . . . 7 ⊢ (𝑢 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)} ↔ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1)))
68		elpwi 4168	. . . . . . . . . . . 12 ⊢ (𝑢 ∈ 𝒫 𝐴 → 𝑢 ⊆ 𝐴)
69	68	ad2antrl 764	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1))) → 𝑢 ⊆ 𝐴)
70		unss1 3782	. . . . . . . . . . 11 ⊢ (𝑢 ⊆ 𝐴 → (𝑢 ∪ {𝑧}) ⊆ (𝐴 ∪ {𝑧}))
71	69, 70	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1))) → (𝑢 ∪ {𝑧}) ⊆ (𝐴 ∪ {𝑧}))
72		vex 3203	. . . . . . . . . . . 12 ⊢ 𝑢 ∈ V
73		snex 4908	. . . . . . . . . . . 12 ⊢ {𝑧} ∈ V
74	72, 73	unex 6956	. . . . . . . . . . 11 ⊢ (𝑢 ∪ {𝑧}) ∈ V
75	74	elpw 4164	. . . . . . . . . 10 ⊢ ((𝑢 ∪ {𝑧}) ∈ 𝒫 (𝐴 ∪ {𝑧}) ↔ (𝑢 ∪ {𝑧}) ⊆ (𝐴 ∪ {𝑧}))
76	71, 75	sylibr 224	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1))) → (𝑢 ∪ {𝑧}) ∈ 𝒫 (𝐴 ∪ {𝑧}))
77	50	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1))) → 𝐴 ∈ Fin)
78		ssfi 8180	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ Fin ∧ 𝑢 ⊆ 𝐴) → 𝑢 ∈ Fin)
79	77, 69, 78	syl2anc 693	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1))) → 𝑢 ∈ Fin)
80	55	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1))) → {𝑧} ∈ Fin)
81	15	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1))) → ¬ 𝑧 ∈ 𝐴)
82	69, 81	ssneldd 3606	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1))) → ¬ 𝑧 ∈ 𝑢)
83		disjsn 4246	. . . . . . . . . . . . 13 ⊢ ((𝑢 ∩ {𝑧}) = ∅ ↔ ¬ 𝑧 ∈ 𝑢)
84	82, 83	sylibr 224	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1))) → (𝑢 ∩ {𝑧}) = ∅)
85		hashun 13171	. . . . . . . . . . . 12 ⊢ ((𝑢 ∈ Fin ∧ {𝑧} ∈ Fin ∧ (𝑢 ∩ {𝑧}) = ∅) → (#‘(𝑢 ∪ {𝑧})) = ((#‘𝑢) + (#‘{𝑧})))
86	79, 80, 84, 85	syl3anc 1326	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1))) → (#‘(𝑢 ∪ {𝑧})) = ((#‘𝑢) + (#‘{𝑧})))
87		simprr 796	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1))) → (#‘𝑢) = (𝐾 − 1))
88		vex 3203	. . . . . . . . . . . . . 14 ⊢ 𝑧 ∈ V
89		hashsng 13159	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ V → (#‘{𝑧}) = 1)
90	88, 89	ax-mp 5	. . . . . . . . . . . . 13 ⊢ (#‘{𝑧}) = 1
91	90	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1))) → (#‘{𝑧}) = 1)
92	87, 91	oveq12d 6668	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1))) → ((#‘𝑢) + (#‘{𝑧})) = ((𝐾 − 1) + 1))
93	1	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1))) → 𝐾 ∈ ℤ)
94	93	zcnd 11483	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1))) → 𝐾 ∈ ℂ)
95		ax-1cn 9994	. . . . . . . . . . . 12 ⊢ 1 ∈ ℂ
96		npcan 10290	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝐾 − 1) + 1) = 𝐾)
97	94, 95, 96	sylancl 694	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1))) → ((𝐾 − 1) + 1) = 𝐾)
98	86, 92, 97	3eqtrd 2660	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1))) → (#‘(𝑢 ∪ {𝑧})) = 𝐾)
99		ssun2 3777	. . . . . . . . . . 11 ⊢ {𝑧} ⊆ (𝑢 ∪ {𝑧})
100	88	snss 4316	. . . . . . . . . . 11 ⊢ (𝑧 ∈ (𝑢 ∪ {𝑧}) ↔ {𝑧} ⊆ (𝑢 ∪ {𝑧}))
101	99, 100	mpbir 221	. . . . . . . . . 10 ⊢ 𝑧 ∈ (𝑢 ∪ {𝑧})
102	98, 101	jctil 560	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1))) → (𝑧 ∈ (𝑢 ∪ {𝑧}) ∧ (#‘(𝑢 ∪ {𝑧})) = 𝐾))
103		eleq2 2690	. . . . . . . . . . 11 ⊢ (𝑥 = (𝑢 ∪ {𝑧}) → (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ (𝑢 ∪ {𝑧})))
104		fveq2 6191	. . . . . . . . . . . 12 ⊢ (𝑥 = (𝑢 ∪ {𝑧}) → (#‘𝑥) = (#‘(𝑢 ∪ {𝑧})))
105	104	eqeq1d 2624	. . . . . . . . . . 11 ⊢ (𝑥 = (𝑢 ∪ {𝑧}) → ((#‘𝑥) = 𝐾 ↔ (#‘(𝑢 ∪ {𝑧})) = 𝐾))
106	103, 105	anbi12d 747	. . . . . . . . . 10 ⊢ (𝑥 = (𝑢 ∪ {𝑧}) → ((𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾) ↔ (𝑧 ∈ (𝑢 ∪ {𝑧}) ∧ (#‘(𝑢 ∪ {𝑧})) = 𝐾)))
107	106	elrab 3363	. . . . . . . . 9 ⊢ ((𝑢 ∪ {𝑧}) ∈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)} ↔ ((𝑢 ∪ {𝑧}) ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ (𝑢 ∪ {𝑧}) ∧ (#‘(𝑢 ∪ {𝑧})) = 𝐾)))
108	76, 102, 107	sylanbrc 698	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1))) → (𝑢 ∪ {𝑧}) ∈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)})
109	108	ex 450	. . . . . . 7 ⊢ (𝜑 → ((𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1)) → (𝑢 ∪ {𝑧}) ∈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)}))
110	67, 109	syl5bi 232	. . . . . 6 ⊢ (𝜑 → (𝑢 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)} → (𝑢 ∪ {𝑧}) ∈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)}))
111		eleq2 2690	. . . . . . . . 9 ⊢ (𝑥 = 𝑣 → (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑣))
112		fveq2 6191	. . . . . . . . . 10 ⊢ (𝑥 = 𝑣 → (#‘𝑥) = (#‘𝑣))
113	112	eqeq1d 2624	. . . . . . . . 9 ⊢ (𝑥 = 𝑣 → ((#‘𝑥) = 𝐾 ↔ (#‘𝑣) = 𝐾))
114	111, 113	anbi12d 747	. . . . . . . 8 ⊢ (𝑥 = 𝑣 → ((𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾) ↔ (𝑧 ∈ 𝑣 ∧ (#‘𝑣) = 𝐾)))
115	114	elrab 3363	. . . . . . 7 ⊢ (𝑣 ∈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)} ↔ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (#‘𝑣) = 𝐾)))
116		elpwi 4168	. . . . . . . . . . . . 13 ⊢ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) → 𝑣 ⊆ (𝐴 ∪ {𝑧}))
117	116	ad2antrl 764	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (#‘𝑣) = 𝐾))) → 𝑣 ⊆ (𝐴 ∪ {𝑧}))
118	117, 21	syl6sseq 3651	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (#‘𝑣) = 𝐾))) → 𝑣 ⊆ ({𝑧} ∪ 𝐴))
119		ssundif 4052	. . . . . . . . . . 11 ⊢ (𝑣 ⊆ ({𝑧} ∪ 𝐴) ↔ (𝑣 ∖ {𝑧}) ⊆ 𝐴)
120	118, 119	sylib 208	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (#‘𝑣) = 𝐾))) → (𝑣 ∖ {𝑧}) ⊆ 𝐴)
121		vex 3203	. . . . . . . . . . . 12 ⊢ 𝑣 ∈ V
122		difexg 4808	. . . . . . . . . . . 12 ⊢ (𝑣 ∈ V → (𝑣 ∖ {𝑧}) ∈ V)
123	121, 122	ax-mp 5	. . . . . . . . . . 11 ⊢ (𝑣 ∖ {𝑧}) ∈ V
124	123	elpw 4164	. . . . . . . . . 10 ⊢ ((𝑣 ∖ {𝑧}) ∈ 𝒫 𝐴 ↔ (𝑣 ∖ {𝑧}) ⊆ 𝐴)
125	120, 124	sylibr 224	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (#‘𝑣) = 𝐾))) → (𝑣 ∖ {𝑧}) ∈ 𝒫 𝐴)
126	50	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (#‘𝑣) = 𝐾))) → 𝐴 ∈ Fin)
127		ssfi 8180	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ Fin ∧ (𝑣 ∖ {𝑧}) ⊆ 𝐴) → (𝑣 ∖ {𝑧}) ∈ Fin)
128	126, 120, 127	syl2anc 693	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (#‘𝑣) = 𝐾))) → (𝑣 ∖ {𝑧}) ∈ Fin)
129		hashcl 13147	. . . . . . . . . . . . 13 ⊢ ((𝑣 ∖ {𝑧}) ∈ Fin → (#‘(𝑣 ∖ {𝑧})) ∈ ℕ₀)
130	128, 129	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (#‘𝑣) = 𝐾))) → (#‘(𝑣 ∖ {𝑧})) ∈ ℕ₀)
131	130	nn0cnd 11353	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (#‘𝑣) = 𝐾))) → (#‘(𝑣 ∖ {𝑧})) ∈ ℂ)
132		pncan 10287	. . . . . . . . . . 11 ⊢ (((#‘(𝑣 ∖ {𝑧})) ∈ ℂ ∧ 1 ∈ ℂ) → (((#‘(𝑣 ∖ {𝑧})) + 1) − 1) = (#‘(𝑣 ∖ {𝑧})))
133	131, 95, 132	sylancl 694	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (#‘𝑣) = 𝐾))) → (((#‘(𝑣 ∖ {𝑧})) + 1) − 1) = (#‘(𝑣 ∖ {𝑧})))
134		undif1 4043	. . . . . . . . . . . . . 14 ⊢ ((𝑣 ∖ {𝑧}) ∪ {𝑧}) = (𝑣 ∪ {𝑧})
135		simprrl 804	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (#‘𝑣) = 𝐾))) → 𝑧 ∈ 𝑣)
136	135	snssd 4340	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (#‘𝑣) = 𝐾))) → {𝑧} ⊆ 𝑣)
137		ssequn2 3786	. . . . . . . . . . . . . . 15 ⊢ ({𝑧} ⊆ 𝑣 ↔ (𝑣 ∪ {𝑧}) = 𝑣)
138	136, 137	sylib 208	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (#‘𝑣) = 𝐾))) → (𝑣 ∪ {𝑧}) = 𝑣)
139	134, 138	syl5eq 2668	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (#‘𝑣) = 𝐾))) → ((𝑣 ∖ {𝑧}) ∪ {𝑧}) = 𝑣)
140	139	fveq2d 6195	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (#‘𝑣) = 𝐾))) → (#‘((𝑣 ∖ {𝑧}) ∪ {𝑧})) = (#‘𝑣))
141	55	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (#‘𝑣) = 𝐾))) → {𝑧} ∈ Fin)
142		incom 3805	. . . . . . . . . . . . . . . 16 ⊢ ((𝑣 ∖ {𝑧}) ∩ {𝑧}) = ({𝑧} ∩ (𝑣 ∖ {𝑧}))
143		disjdif 4040	. . . . . . . . . . . . . . . 16 ⊢ ({𝑧} ∩ (𝑣 ∖ {𝑧})) = ∅
144	142, 143	eqtri 2644	. . . . . . . . . . . . . . 15 ⊢ ((𝑣 ∖ {𝑧}) ∩ {𝑧}) = ∅
145	144	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (#‘𝑣) = 𝐾))) → ((𝑣 ∖ {𝑧}) ∩ {𝑧}) = ∅)
146		hashun 13171	. . . . . . . . . . . . . 14 ⊢ (((𝑣 ∖ {𝑧}) ∈ Fin ∧ {𝑧} ∈ Fin ∧ ((𝑣 ∖ {𝑧}) ∩ {𝑧}) = ∅) → (#‘((𝑣 ∖ {𝑧}) ∪ {𝑧})) = ((#‘(𝑣 ∖ {𝑧})) + (#‘{𝑧})))
147	128, 141, 145, 146	syl3anc 1326	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (#‘𝑣) = 𝐾))) → (#‘((𝑣 ∖ {𝑧}) ∪ {𝑧})) = ((#‘(𝑣 ∖ {𝑧})) + (#‘{𝑧})))
148	90	oveq2i 6661	. . . . . . . . . . . . 13 ⊢ ((#‘(𝑣 ∖ {𝑧})) + (#‘{𝑧})) = ((#‘(𝑣 ∖ {𝑧})) + 1)
149	147, 148	syl6eq 2672	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (#‘𝑣) = 𝐾))) → (#‘((𝑣 ∖ {𝑧}) ∪ {𝑧})) = ((#‘(𝑣 ∖ {𝑧})) + 1))
150		simprrr 805	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (#‘𝑣) = 𝐾))) → (#‘𝑣) = 𝐾)
151	140, 149, 150	3eqtr3d 2664	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (#‘𝑣) = 𝐾))) → ((#‘(𝑣 ∖ {𝑧})) + 1) = 𝐾)
152	151	oveq1d 6665	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (#‘𝑣) = 𝐾))) → (((#‘(𝑣 ∖ {𝑧})) + 1) − 1) = (𝐾 − 1))
153	133, 152	eqtr3d 2658	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (#‘𝑣) = 𝐾))) → (#‘(𝑣 ∖ {𝑧})) = (𝐾 − 1))
154		fveq2 6191	. . . . . . . . . . 11 ⊢ (𝑥 = (𝑣 ∖ {𝑧}) → (#‘𝑥) = (#‘(𝑣 ∖ {𝑧})))
155	154	eqeq1d 2624	. . . . . . . . . 10 ⊢ (𝑥 = (𝑣 ∖ {𝑧}) → ((#‘𝑥) = (𝐾 − 1) ↔ (#‘(𝑣 ∖ {𝑧})) = (𝐾 − 1)))
156	155	elrab 3363	. . . . . . . . 9 ⊢ ((𝑣 ∖ {𝑧}) ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)} ↔ ((𝑣 ∖ {𝑧}) ∈ 𝒫 𝐴 ∧ (#‘(𝑣 ∖ {𝑧})) = (𝐾 − 1)))
157	125, 153, 156	sylanbrc 698	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (#‘𝑣) = 𝐾))) → (𝑣 ∖ {𝑧}) ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)})
158	157	ex 450	. . . . . . 7 ⊢ (𝜑 → ((𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (#‘𝑣) = 𝐾)) → (𝑣 ∖ {𝑧}) ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)}))
159	115, 158	syl5bi 232	. . . . . 6 ⊢ (𝜑 → (𝑣 ∈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)} → (𝑣 ∖ {𝑧}) ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)}))
160	67, 115	anbi12i 733	. . . . . . 7 ⊢ ((𝑢 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)} ∧ 𝑣 ∈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)}) ↔ ((𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1)) ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (#‘𝑣) = 𝐾))))
161		simp3rl 1134	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1)) ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (#‘𝑣) = 𝐾))) → 𝑧 ∈ 𝑣)
162	161	snssd 4340	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1)) ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (#‘𝑣) = 𝐾))) → {𝑧} ⊆ 𝑣)
163		incom 3805	. . . . . . . . . . . 12 ⊢ ({𝑧} ∩ 𝑢) = (𝑢 ∩ {𝑧})
164	84	3adant3 1081	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1)) ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (#‘𝑣) = 𝐾))) → (𝑢 ∩ {𝑧}) = ∅)
165	163, 164	syl5eq 2668	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1)) ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (#‘𝑣) = 𝐾))) → ({𝑧} ∩ 𝑢) = ∅)
166		uneqdifeq 4057	. . . . . . . . . . 11 ⊢ (({𝑧} ⊆ 𝑣 ∧ ({𝑧} ∩ 𝑢) = ∅) → (({𝑧} ∪ 𝑢) = 𝑣 ↔ (𝑣 ∖ {𝑧}) = 𝑢))
167	162, 165, 166	syl2anc 693	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1)) ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (#‘𝑣) = 𝐾))) → (({𝑧} ∪ 𝑢) = 𝑣 ↔ (𝑣 ∖ {𝑧}) = 𝑢))
168	167	bicomd 213	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1)) ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (#‘𝑣) = 𝐾))) → ((𝑣 ∖ {𝑧}) = 𝑢 ↔ ({𝑧} ∪ 𝑢) = 𝑣))
169		eqcom 2629	. . . . . . . . 9 ⊢ (𝑢 = (𝑣 ∖ {𝑧}) ↔ (𝑣 ∖ {𝑧}) = 𝑢)
170		eqcom 2629	. . . . . . . . . 10 ⊢ (𝑣 = (𝑢 ∪ {𝑧}) ↔ (𝑢 ∪ {𝑧}) = 𝑣)
171		uncom 3757	. . . . . . . . . . 11 ⊢ (𝑢 ∪ {𝑧}) = ({𝑧} ∪ 𝑢)
172	171	eqeq1i 2627	. . . . . . . . . 10 ⊢ ((𝑢 ∪ {𝑧}) = 𝑣 ↔ ({𝑧} ∪ 𝑢) = 𝑣)
173	170, 172	bitri 264	. . . . . . . . 9 ⊢ (𝑣 = (𝑢 ∪ {𝑧}) ↔ ({𝑧} ∪ 𝑢) = 𝑣)
174	168, 169, 173	3bitr4g 303	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1)) ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (#‘𝑣) = 𝐾))) → (𝑢 = (𝑣 ∖ {𝑧}) ↔ 𝑣 = (𝑢 ∪ {𝑧})))
175	174	3expib 1268	. . . . . . 7 ⊢ (𝜑 → (((𝑢 ∈ 𝒫 𝐴 ∧ (#‘𝑢) = (𝐾 − 1)) ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (#‘𝑣) = 𝐾))) → (𝑢 = (𝑣 ∖ {𝑧}) ↔ 𝑣 = (𝑢 ∪ {𝑧}))))
176	160, 175	syl5bi 232	. . . . . 6 ⊢ (𝜑 → ((𝑢 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)} ∧ 𝑣 ∈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)}) → (𝑢 = (𝑣 ∖ {𝑧}) ↔ 𝑣 = (𝑢 ∪ {𝑧}))))
177	54, 64, 110, 159, 176	en3d 7992	. . . . 5 ⊢ (𝜑 → {𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)} ≈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)})
178		ssrab2 3687	. . . . . . 7 ⊢ {𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)} ⊆ 𝒫 𝐴
179		ssfi 8180	. . . . . . 7 ⊢ ((𝒫 𝐴 ∈ Fin ∧ {𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)} ⊆ 𝒫 𝐴) → {𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)} ∈ Fin)
180	52, 178, 179	sylancl 694	. . . . . 6 ⊢ (𝜑 → {𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)} ∈ Fin)
181		hashen 13135	. . . . . 6 ⊢ (({𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)} ∈ Fin ∧ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)} ∈ Fin) → ((#‘{𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)}) = (#‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)}) ↔ {𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)} ≈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)}))
182	180, 62, 181	syl2anc 693	. . . . 5 ⊢ (𝜑 → ((#‘{𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)}) = (#‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)}) ↔ {𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)} ≈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)}))
183	177, 182	mpbird 247	. . . 4 ⊢ (𝜑 → (#‘{𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = (𝐾 − 1)}) = (#‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)}))
184	49, 183	eqtrd 2656	. . 3 ⊢ (𝜑 → ((#‘𝐴)C(𝐾 − 1)) = (#‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)}))
185	40, 184	oveq12d 6668	. 2 ⊢ (𝜑 → (((#‘𝐴)C𝐾) + ((#‘𝐴)C(𝐾 − 1))) = ((#‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)}) + (#‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)})))
186	55	a1i 11	. . . . . 6 ⊢ (𝜑 → {𝑧} ∈ Fin)
187		disjsn 4246	. . . . . . 7 ⊢ ((𝐴 ∩ {𝑧}) = ∅ ↔ ¬ 𝑧 ∈ 𝐴)
188	15, 187	sylibr 224	. . . . . 6 ⊢ (𝜑 → (𝐴 ∩ {𝑧}) = ∅)
189		hashun 13171	. . . . . 6 ⊢ ((𝐴 ∈ Fin ∧ {𝑧} ∈ Fin ∧ (𝐴 ∩ {𝑧}) = ∅) → (#‘(𝐴 ∪ {𝑧})) = ((#‘𝐴) + (#‘{𝑧})))
190	50, 186, 188, 189	syl3anc 1326	. . . . 5 ⊢ (𝜑 → (#‘(𝐴 ∪ {𝑧})) = ((#‘𝐴) + (#‘{𝑧})))
191	90	oveq2i 6661	. . . . 5 ⊢ ((#‘𝐴) + (#‘{𝑧})) = ((#‘𝐴) + 1)
192	190, 191	syl6eq 2672	. . . 4 ⊢ (𝜑 → (#‘(𝐴 ∪ {𝑧})) = ((#‘𝐴) + 1))
193	192	oveq1d 6665	. . 3 ⊢ (𝜑 → ((#‘(𝐴 ∪ {𝑧}))C𝐾) = (((#‘𝐴) + 1)C𝐾))
194		hashcl 13147	. . . . 5 ⊢ (𝐴 ∈ Fin → (#‘𝐴) ∈ ℕ₀)
195	50, 194	syl 17	. . . 4 ⊢ (𝜑 → (#‘𝐴) ∈ ℕ₀)
196		bcpasc 13108	. . . 4 ⊢ (((#‘𝐴) ∈ ℕ₀ ∧ 𝐾 ∈ ℤ) → (((#‘𝐴)C𝐾) + ((#‘𝐴)C(𝐾 − 1))) = (((#‘𝐴) + 1)C𝐾))
197	195, 1, 196	syl2anc 693	. . 3 ⊢ (𝜑 → (((#‘𝐴)C𝐾) + ((#‘𝐴)C(𝐾 − 1))) = (((#‘𝐴) + 1)C𝐾))
198	193, 197	eqtr4d 2659	. 2 ⊢ (𝜑 → ((#‘(𝐴 ∪ {𝑧}))C𝐾) = (((#‘𝐴)C𝐾) + ((#‘𝐴)C(𝐾 − 1))))
199		pm2.1 433	. . . . . . . . 9 ⊢ (¬ 𝑧 ∈ 𝑥 ∨ 𝑧 ∈ 𝑥)
200	199	biantrur 527	. . . . . . . 8 ⊢ ((#‘𝑥) = 𝐾 ↔ ((¬ 𝑧 ∈ 𝑥 ∨ 𝑧 ∈ 𝑥) ∧ (#‘𝑥) = 𝐾))
201		andir 912	. . . . . . . 8 ⊢ (((¬ 𝑧 ∈ 𝑥 ∨ 𝑧 ∈ 𝑥) ∧ (#‘𝑥) = 𝐾) ↔ ((¬ 𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾) ∨ (𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)))
202	200, 201	bitri 264	. . . . . . 7 ⊢ ((#‘𝑥) = 𝐾 ↔ ((¬ 𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾) ∨ (𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)))
203	202	a1i 11	. . . . . 6 ⊢ (𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) → ((#‘𝑥) = 𝐾 ↔ ((¬ 𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾) ∨ (𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾))))
204	203	rabbiia 3185	. . . . 5 ⊢ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (#‘𝑥) = 𝐾} = {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ ((¬ 𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾) ∨ (𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾))}
205		unrab 3898	. . . . 5 ⊢ ({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)} ∪ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)}) = {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ ((¬ 𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾) ∨ (𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾))}
206	204, 205	eqtr4i 2647	. . . 4 ⊢ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (#‘𝑥) = 𝐾} = ({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)} ∪ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)})
207	206	fveq2i 6194	. . 3 ⊢ (#‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (#‘𝑥) = 𝐾}) = (#‘({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)} ∪ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)}))
208		ssrab2 3687	. . . . 5 ⊢ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)} ⊆ 𝒫 (𝐴 ∪ {𝑧})
209		ssfi 8180	. . . . 5 ⊢ ((𝒫 (𝐴 ∪ {𝑧}) ∈ Fin ∧ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)} ⊆ 𝒫 (𝐴 ∪ {𝑧})) → {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)} ∈ Fin)
210	59, 208, 209	sylancl 694	. . . 4 ⊢ (𝜑 → {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)} ∈ Fin)
211		inrab 3899	. . . . . 6 ⊢ ({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)} ∩ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)}) = {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ ((¬ 𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾) ∧ (𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾))}
212		simprl 794	. . . . . . . . 9 ⊢ (((¬ 𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾) ∧ (𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)) → 𝑧 ∈ 𝑥)
213		simpll 790	. . . . . . . . 9 ⊢ (((¬ 𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾) ∧ (𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)) → ¬ 𝑧 ∈ 𝑥)
214	212, 213	pm2.65i 185	. . . . . . . 8 ⊢ ¬ ((¬ 𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾) ∧ (𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾))
215	214	rgenw 2924	. . . . . . 7 ⊢ ∀𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ¬ ((¬ 𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾) ∧ (𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾))
216		rabeq0 3957	. . . . . . 7 ⊢ ({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ ((¬ 𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾) ∧ (𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾))} = ∅ ↔ ∀𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ¬ ((¬ 𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾) ∧ (𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)))
217	215, 216	mpbir 221	. . . . . 6 ⊢ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ ((¬ 𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾) ∧ (𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾))} = ∅
218	211, 217	eqtri 2644	. . . . 5 ⊢ ({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)} ∩ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)}) = ∅
219	218	a1i 11	. . . 4 ⊢ (𝜑 → ({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)} ∩ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)}) = ∅)
220		hashun 13171	. . . 4 ⊢ (({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)} ∈ Fin ∧ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)} ∈ Fin ∧ ({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)} ∩ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)}) = ∅) → (#‘({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)} ∪ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)})) = ((#‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)}) + (#‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)})))
221	210, 62, 219, 220	syl3anc 1326	. . 3 ⊢ (𝜑 → (#‘({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)} ∪ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)})) = ((#‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)}) + (#‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)})))
222	207, 221	syl5eq 2668	. 2 ⊢ (𝜑 → (#‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (#‘𝑥) = 𝐾}) = ((#‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)}) + (#‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (#‘𝑥) = 𝐾)})))
223	185, 198, 222	3eqtr4d 2666	1 ⊢ (𝜑 → ((#‘(𝐴 ∪ {𝑧}))C𝐾) = (#‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (#‘𝑥) = 𝐾}))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 196 ∨ wo 383 ∧ wa 384 ∧ w3a 1037 = wceq 1483 ∈ wcel 1990 ∀wral 2912 {crab 2916 Vcvv 3200 ∖ cdif 3571 ∪ cun 3572 ∩ cin 3573 ⊆ wss 3574 ∅c0 3915 𝒫 cpw 4158 {csn 4177 class class class wbr 4653 ‘cfv 5888 (class class class)co 6650 ≈ cen 7952 Fincfn 7955 ℂcc 9934 1c1 9937 + caddc 9939 − cmin 10266 ℕ₀cn0 11292 ℤcz 11377 Ccbc 13089 #chash 13117

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-rep 4771 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949 ax-cnex 9992 ax-resscn 9993 ax-1cn 9994 ax-icn 9995 ax-addcl 9996 ax-addrcl 9997 ax-mulcl 9998 ax-mulrcl 9999 ax-mulcom 10000 ax-addass 10001 ax-mulass 10002 ax-distr 10003 ax-i2m1 10004 ax-1ne0 10005 ax-1rid 10006 ax-rnegex 10007 ax-rrecex 10008 ax-cnre 10009 ax-pre-lttri 10010 ax-pre-lttrn 10011 ax-pre-ltadd 10012 ax-pre-mulgt0 10013

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-nel 2898 df-ral 2917 df-rex 2918 df-reu 2919 df-rmo 2920 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-uni 4437 df-int 4476 df-iun 4522 df-br 4654 df-opab 4713 df-mpt 4730 df-tr 4753 df-id 5024 df-eprel 5029 df-po 5035 df-so 5036 df-fr 5073 df-we 5075 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-pred 5680 df-ord 5726 df-on 5727 df-lim 5728 df-suc 5729 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-riota 6611 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-om 7066 df-1st 7168 df-2nd 7169 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-1o 7560 df-2o 7561 df-oadd 7564 df-er 7742 df-map 7859 df-en 7956 df-dom 7957 df-sdom 7958 df-fin 7959 df-card 8765 df-cda 8990 df-pnf 10076 df-mnf 10077 df-xr 10078 df-ltxr 10079 df-le 10080 df-sub 10268 df-neg 10269 df-div 10685 df-nn 11021 df-n0 11293 df-z 11378 df-uz 11688 df-rp 11833 df-fz 12327 df-seq 12802 df-fac 13061 df-bc 13090 df-hash 13118

This theorem is referenced by: hashbc 13237

W3C validator