ramub1lem1 - Metamath Proof Explorer

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

Theorem ramub1lem1 15568

Description: Lemma for ramub1 15570. (Contributed by Mario Carneiro, 23-Apr-2015.)

**Hypotheses**
Ref	Expression
ramub1.m	⊢ (𝜑 → 𝑀 ∈ ℕ)
ramub1.r	⊢ (𝜑 → 𝑅 ∈ Fin)
ramub1.f	⊢ (𝜑 → 𝐹:𝑅⟶ℕ)
ramub1.g	⊢ 𝐺 = (𝑥 ∈ 𝑅 ↦ (𝑀 Ramsey (𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑥, ((𝐹‘𝑥) − 1), (𝐹‘𝑦)))))
ramub1.1	⊢ (𝜑 → 𝐺:𝑅⟶ℕ₀)
ramub1.2	⊢ (𝜑 → ((𝑀 − 1) Ramsey 𝐺) ∈ ℕ₀)
ramub1.3	⊢ 𝐶 = (𝑎 ∈ V, 𝑖 ∈ ℕ₀ ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (#‘𝑏) = 𝑖})
ramub1.4	⊢ (𝜑 → 𝑆 ∈ Fin)
ramub1.5	⊢ (𝜑 → (#‘𝑆) = (((𝑀 − 1) Ramsey 𝐺) + 1))
ramub1.6	⊢ (𝜑 → 𝐾:(𝑆𝐶𝑀)⟶𝑅)
ramub1.x	⊢ (𝜑 → 𝑋 ∈ 𝑆)
ramub1.h	⊢ 𝐻 = (𝑢 ∈ ((𝑆 ∖ {𝑋})𝐶(𝑀 − 1)) ↦ (𝐾‘(𝑢 ∪ {𝑋})))
ramub1.d	⊢ (𝜑 → 𝐷 ∈ 𝑅)
ramub1.w	⊢ (𝜑 → 𝑊 ⊆ (𝑆 ∖ {𝑋}))
ramub1.7	⊢ (𝜑 → (𝐺‘𝐷) ≤ (#‘𝑊))
ramub1.8	⊢ (𝜑 → (𝑊𝐶(𝑀 − 1)) ⊆ (^◡𝐻 “ {𝐷}))
ramub1.e	⊢ (𝜑 → 𝐸 ∈ 𝑅)
ramub1.v	⊢ (𝜑 → 𝑉 ⊆ 𝑊)
ramub1.9	⊢ (𝜑 → if(𝐸 = 𝐷, ((𝐹‘𝐷) − 1), (𝐹‘𝐸)) ≤ (#‘𝑉))
ramub1.s	⊢ (𝜑 → (𝑉𝐶𝑀) ⊆ (^◡𝐾 “ {𝐸}))

**Assertion**
Ref	Expression
ramub1lem1	⊢ (𝜑 → ∃𝑧 ∈ 𝒫 𝑆((𝐹‘𝐸) ≤ (#‘𝑧) ∧ (𝑧𝐶𝑀) ⊆ (^◡𝐾 “ {𝐸})))

Distinct variable groups: 𝑥,𝑢,𝐷 𝑦,𝑢,𝑧,𝐹,𝑥 𝑎,𝑏,𝑖,𝑢,𝑥,𝑦,𝑧,𝑀 𝐺,𝑎,𝑖,𝑢,𝑥,𝑦,𝑧 𝑢,𝑅,𝑥,𝑦,𝑧 𝑊,𝑎,𝑖,𝑢 𝜑,𝑢,𝑥,𝑦,𝑧 𝑆,𝑎,𝑖,𝑢,𝑥,𝑦,𝑧 𝑉,𝑎,𝑖,𝑥,𝑧 𝑢,𝐶,𝑥,𝑦,𝑧 𝑢,𝐻,𝑥,𝑦,𝑧 𝑢,𝐾,𝑥,𝑦,𝑧 𝑥,𝐸,𝑧 𝑋,𝑎,𝑖,𝑢,𝑥,𝑦,𝑧 Allowed substitution hints: 𝜑(𝑖,𝑎,𝑏) 𝐶(𝑖,𝑎,𝑏) 𝐷(𝑦,𝑧,𝑖,𝑎,𝑏) 𝑅(𝑖,𝑎,𝑏) 𝑆(𝑏) 𝐸(𝑦,𝑢,𝑖,𝑎,𝑏) 𝐹(𝑖,𝑎,𝑏) 𝐺(𝑏) 𝐻(𝑖,𝑎,𝑏) 𝐾(𝑖,𝑎,𝑏) 𝑉(𝑦,𝑢,𝑏) 𝑊(𝑥,𝑦,𝑧,𝑏) 𝑋(𝑏)

**Proof of Theorem ramub1lem1**
Step	Hyp	Ref	Expression
1		ramub1.v	. . . . . . . 8 ⊢ (𝜑 → 𝑉 ⊆ 𝑊)
2		ramub1.w	. . . . . . . 8 ⊢ (𝜑 → 𝑊 ⊆ (𝑆 ∖ {𝑋}))
3	1, 2	sstrd 3578	. . . . . . 7 ⊢ (𝜑 → 𝑉 ⊆ (𝑆 ∖ {𝑋}))
4	3	difss2d 3702	. . . . . 6 ⊢ (𝜑 → 𝑉 ⊆ 𝑆)
5		ramub1.x	. . . . . . 7 ⊢ (𝜑 → 𝑋 ∈ 𝑆)
6	5	snssd 4281	. . . . . 6 ⊢ (𝜑 → {𝑋} ⊆ 𝑆)
7	4, 6	unssd 3751	. . . . 5 ⊢ (𝜑 → (𝑉 ∪ {𝑋}) ⊆ 𝑆)
8		ramub1.4	. . . . . 6 ⊢ (𝜑 → 𝑆 ∈ Fin)
9		elpw2g 4754	. . . . . 6 ⊢ (𝑆 ∈ Fin → ((𝑉 ∪ {𝑋}) ∈ 𝒫 𝑆 ↔ (𝑉 ∪ {𝑋}) ⊆ 𝑆))
10	8, 9	syl 17	. . . . 5 ⊢ (𝜑 → ((𝑉 ∪ {𝑋}) ∈ 𝒫 𝑆 ↔ (𝑉 ∪ {𝑋}) ⊆ 𝑆))
11	7, 10	mpbird 246	. . . 4 ⊢ (𝜑 → (𝑉 ∪ {𝑋}) ∈ 𝒫 𝑆)
12	11	adantr 480	. . 3 ⊢ ((𝜑 ∧ 𝐸 = 𝐷) → (𝑉 ∪ {𝑋}) ∈ 𝒫 𝑆)
13		iftrue 4042	. . . . . . 7 ⊢ (𝐸 = 𝐷 → if(𝐸 = 𝐷, ((𝐹‘𝐷) − 1), (𝐹‘𝐸)) = ((𝐹‘𝐷) − 1))
14	13	adantl 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝐸 = 𝐷) → if(𝐸 = 𝐷, ((𝐹‘𝐷) − 1), (𝐹‘𝐸)) = ((𝐹‘𝐷) − 1))
15		ramub1.9	. . . . . . 7 ⊢ (𝜑 → if(𝐸 = 𝐷, ((𝐹‘𝐷) − 1), (𝐹‘𝐸)) ≤ (#‘𝑉))
16	15	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝐸 = 𝐷) → if(𝐸 = 𝐷, ((𝐹‘𝐷) − 1), (𝐹‘𝐸)) ≤ (#‘𝑉))
17	14, 16	eqbrtrrd 4607	. . . . 5 ⊢ ((𝜑 ∧ 𝐸 = 𝐷) → ((𝐹‘𝐷) − 1) ≤ (#‘𝑉))
18		ramub1.f	. . . . . . . . 9 ⊢ (𝜑 → 𝐹:𝑅⟶ℕ)
19		ramub1.d	. . . . . . . . 9 ⊢ (𝜑 → 𝐷 ∈ 𝑅)
20	18, 19	ffvelrnd 6268	. . . . . . . 8 ⊢ (𝜑 → (𝐹‘𝐷) ∈ ℕ)
21	20	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐸 = 𝐷) → (𝐹‘𝐷) ∈ ℕ)
22	21	nnred 10912	. . . . . 6 ⊢ ((𝜑 ∧ 𝐸 = 𝐷) → (𝐹‘𝐷) ∈ ℝ)
23		1red 9934	. . . . . 6 ⊢ ((𝜑 ∧ 𝐸 = 𝐷) → 1 ∈ ℝ)
24		ssfi 8065	. . . . . . . . 9 ⊢ ((𝑆 ∈ Fin ∧ 𝑉 ⊆ 𝑆) → 𝑉 ∈ Fin)
25	8, 4, 24	syl2anc 691	. . . . . . . 8 ⊢ (𝜑 → 𝑉 ∈ Fin)
26		hashcl 13009	. . . . . . . 8 ⊢ (𝑉 ∈ Fin → (#‘𝑉) ∈ ℕ₀)
27		nn0re 11178	. . . . . . . 8 ⊢ ((#‘𝑉) ∈ ℕ₀ → (#‘𝑉) ∈ ℝ)
28	25, 26, 27	3syl 18	. . . . . . 7 ⊢ (𝜑 → (#‘𝑉) ∈ ℝ)
29	28	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝐸 = 𝐷) → (#‘𝑉) ∈ ℝ)
30	22, 23, 29	lesubaddd 10503	. . . . 5 ⊢ ((𝜑 ∧ 𝐸 = 𝐷) → (((𝐹‘𝐷) − 1) ≤ (#‘𝑉) ↔ (𝐹‘𝐷) ≤ ((#‘𝑉) + 1)))
31	17, 30	mpbid 221	. . . 4 ⊢ ((𝜑 ∧ 𝐸 = 𝐷) → (𝐹‘𝐷) ≤ ((#‘𝑉) + 1))
32		fveq2 6103	. . . . 5 ⊢ (𝐸 = 𝐷 → (𝐹‘𝐸) = (𝐹‘𝐷))
33		snidg 4153	. . . . . . . 8 ⊢ (𝑋 ∈ 𝑆 → 𝑋 ∈ {𝑋})
34	5, 33	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝑋 ∈ {𝑋})
35	3	sseld 3567	. . . . . . . 8 ⊢ (𝜑 → (𝑋 ∈ 𝑉 → 𝑋 ∈ (𝑆 ∖ {𝑋})))
36		eldifn 3695	. . . . . . . 8 ⊢ (𝑋 ∈ (𝑆 ∖ {𝑋}) → ¬ 𝑋 ∈ {𝑋})
37	35, 36	syl6 34	. . . . . . 7 ⊢ (𝜑 → (𝑋 ∈ 𝑉 → ¬ 𝑋 ∈ {𝑋}))
38	34, 37	mt2d 130	. . . . . 6 ⊢ (𝜑 → ¬ 𝑋 ∈ 𝑉)
39		hashunsng 13042	. . . . . . 7 ⊢ (𝑋 ∈ 𝑆 → ((𝑉 ∈ Fin ∧ ¬ 𝑋 ∈ 𝑉) → (#‘(𝑉 ∪ {𝑋})) = ((#‘𝑉) + 1)))
40	5, 39	syl 17	. . . . . 6 ⊢ (𝜑 → ((𝑉 ∈ Fin ∧ ¬ 𝑋 ∈ 𝑉) → (#‘(𝑉 ∪ {𝑋})) = ((#‘𝑉) + 1)))
41	25, 38, 40	mp2and 711	. . . . 5 ⊢ (𝜑 → (#‘(𝑉 ∪ {𝑋})) = ((#‘𝑉) + 1))
42	32, 41	breqan12rd 4600	. . . 4 ⊢ ((𝜑 ∧ 𝐸 = 𝐷) → ((𝐹‘𝐸) ≤ (#‘(𝑉 ∪ {𝑋})) ↔ (𝐹‘𝐷) ≤ ((#‘𝑉) + 1)))
43	31, 42	mpbird 246	. . 3 ⊢ ((𝜑 ∧ 𝐸 = 𝐷) → (𝐹‘𝐸) ≤ (#‘(𝑉 ∪ {𝑋})))
44		snfi 7923	. . . . . . 7 ⊢ {𝑋} ∈ Fin
45		unfi 8112	. . . . . . 7 ⊢ ((𝑉 ∈ Fin ∧ {𝑋} ∈ Fin) → (𝑉 ∪ {𝑋}) ∈ Fin)
46	25, 44, 45	sylancl 693	. . . . . 6 ⊢ (𝜑 → (𝑉 ∪ {𝑋}) ∈ Fin)
47		ramub1.m	. . . . . . 7 ⊢ (𝜑 → 𝑀 ∈ ℕ)
48	47	nnnn0d 11228	. . . . . 6 ⊢ (𝜑 → 𝑀 ∈ ℕ₀)
49		ramub1.3	. . . . . . 7 ⊢ 𝐶 = (𝑎 ∈ V, 𝑖 ∈ ℕ₀ ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (#‘𝑏) = 𝑖})
50	49	hashbcval 15544	. . . . . 6 ⊢ (((𝑉 ∪ {𝑋}) ∈ Fin ∧ 𝑀 ∈ ℕ₀) → ((𝑉 ∪ {𝑋})𝐶𝑀) = {𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∣ (#‘𝑥) = 𝑀})
51	46, 48, 50	syl2anc 691	. . . . 5 ⊢ (𝜑 → ((𝑉 ∪ {𝑋})𝐶𝑀) = {𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∣ (#‘𝑥) = 𝑀})
52	51	adantr 480	. . . 4 ⊢ ((𝜑 ∧ 𝐸 = 𝐷) → ((𝑉 ∪ {𝑋})𝐶𝑀) = {𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∣ (#‘𝑥) = 𝑀})
53		simpl1l 1105	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (#‘𝑥) = 𝑀) ∧ 𝑥 ∈ 𝒫 𝑉) → 𝜑)
54	49	hashbcval 15544	. . . . . . . . . 10 ⊢ ((𝑉 ∈ Fin ∧ 𝑀 ∈ ℕ₀) → (𝑉𝐶𝑀) = {𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 𝑀})
55	25, 48, 54	syl2anc 691	. . . . . . . . 9 ⊢ (𝜑 → (𝑉𝐶𝑀) = {𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 𝑀})
56		ramub1.s	. . . . . . . . 9 ⊢ (𝜑 → (𝑉𝐶𝑀) ⊆ (^◡𝐾 “ {𝐸}))
57	55, 56	eqsstr3d 3603	. . . . . . . 8 ⊢ (𝜑 → {𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 𝑀} ⊆ (^◡𝐾 “ {𝐸}))
58	53, 57	syl 17	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (#‘𝑥) = 𝑀) ∧ 𝑥 ∈ 𝒫 𝑉) → {𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 𝑀} ⊆ (^◡𝐾 “ {𝐸}))
59		simpr 476	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (#‘𝑥) = 𝑀) ∧ 𝑥 ∈ 𝒫 𝑉) → 𝑥 ∈ 𝒫 𝑉)
60		simpl3 1059	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (#‘𝑥) = 𝑀) ∧ 𝑥 ∈ 𝒫 𝑉) → (#‘𝑥) = 𝑀)
61		rabid 3095	. . . . . . . 8 ⊢ (𝑥 ∈ {𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 𝑀} ↔ (𝑥 ∈ 𝒫 𝑉 ∧ (#‘𝑥) = 𝑀))
62	59, 60, 61	sylanbrc 695	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (#‘𝑥) = 𝑀) ∧ 𝑥 ∈ 𝒫 𝑉) → 𝑥 ∈ {𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 𝑀})
63	58, 62	sseldd 3569	. . . . . 6 ⊢ ((((𝜑 ∧ 𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (#‘𝑥) = 𝑀) ∧ 𝑥 ∈ 𝒫 𝑉) → 𝑥 ∈ (^◡𝐾 “ {𝐸}))
64		simpl2 1058	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (#‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}))
65	64	elpwid 4118	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (#‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → 𝑥 ⊆ (𝑉 ∪ {𝑋}))
66		simpl1l 1105	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (#‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → 𝜑)
67	66, 7	syl 17	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (#‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → (𝑉 ∪ {𝑋}) ⊆ 𝑆)
68	65, 67	sstrd 3578	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (#‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → 𝑥 ⊆ 𝑆)
69		vex 3176	. . . . . . . . . . 11 ⊢ 𝑥 ∈ V
70	69	elpw 4114	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝒫 𝑆 ↔ 𝑥 ⊆ 𝑆)
71	68, 70	sylibr 223	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (#‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → 𝑥 ∈ 𝒫 𝑆)
72		simpl3 1059	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (#‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → (#‘𝑥) = 𝑀)
73		rabid 3095	. . . . . . . . 9 ⊢ (𝑥 ∈ {𝑥 ∈ 𝒫 𝑆 ∣ (#‘𝑥) = 𝑀} ↔ (𝑥 ∈ 𝒫 𝑆 ∧ (#‘𝑥) = 𝑀))
74	71, 72, 73	sylanbrc 695	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (#‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → 𝑥 ∈ {𝑥 ∈ 𝒫 𝑆 ∣ (#‘𝑥) = 𝑀})
75	49	hashbcval 15544	. . . . . . . . . 10 ⊢ ((𝑆 ∈ Fin ∧ 𝑀 ∈ ℕ₀) → (𝑆𝐶𝑀) = {𝑥 ∈ 𝒫 𝑆 ∣ (#‘𝑥) = 𝑀})
76	8, 48, 75	syl2anc 691	. . . . . . . . 9 ⊢ (𝜑 → (𝑆𝐶𝑀) = {𝑥 ∈ 𝒫 𝑆 ∣ (#‘𝑥) = 𝑀})
77	66, 76	syl 17	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (#‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → (𝑆𝐶𝑀) = {𝑥 ∈ 𝒫 𝑆 ∣ (#‘𝑥) = 𝑀})
78	74, 77	eleqtrrd 2691	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (#‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → 𝑥 ∈ (𝑆𝐶𝑀))
79	2	difss2d 3702	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑊 ⊆ 𝑆)
80		ssfi 8065	. . . . . . . . . . . . . . 15 ⊢ ((𝑆 ∈ Fin ∧ 𝑊 ⊆ 𝑆) → 𝑊 ∈ Fin)
81	8, 79, 80	syl2anc 691	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑊 ∈ Fin)
82		nnm1nn0 11211	. . . . . . . . . . . . . . 15 ⊢ (𝑀 ∈ ℕ → (𝑀 − 1) ∈ ℕ₀)
83	47, 82	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑀 − 1) ∈ ℕ₀)
84	49	hashbcval 15544	. . . . . . . . . . . . . 14 ⊢ ((𝑊 ∈ Fin ∧ (𝑀 − 1) ∈ ℕ₀) → (𝑊𝐶(𝑀 − 1)) = {𝑢 ∈ 𝒫 𝑊 ∣ (#‘𝑢) = (𝑀 − 1)})
85	81, 83, 84	syl2anc 691	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑊𝐶(𝑀 − 1)) = {𝑢 ∈ 𝒫 𝑊 ∣ (#‘𝑢) = (𝑀 − 1)})
86		ramub1.8	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑊𝐶(𝑀 − 1)) ⊆ (^◡𝐻 “ {𝐷}))
87	85, 86	eqsstr3d 3603	. . . . . . . . . . . 12 ⊢ (𝜑 → {𝑢 ∈ 𝒫 𝑊 ∣ (#‘𝑢) = (𝑀 − 1)} ⊆ (^◡𝐻 “ {𝐷}))
88	66, 87	syl 17	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (#‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → {𝑢 ∈ 𝒫 𝑊 ∣ (#‘𝑢) = (𝑀 − 1)} ⊆ (^◡𝐻 “ {𝐷}))
89		uncom 3719	. . . . . . . . . . . . . . . 16 ⊢ (𝑉 ∪ {𝑋}) = ({𝑋} ∪ 𝑉)
90	65, 89	syl6sseq 3614	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (#‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → 𝑥 ⊆ ({𝑋} ∪ 𝑉))
91		ssundif 4004	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ⊆ ({𝑋} ∪ 𝑉) ↔ (𝑥 ∖ {𝑋}) ⊆ 𝑉)
92	90, 91	sylib 207	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (#‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → (𝑥 ∖ {𝑋}) ⊆ 𝑉)
93	66, 1	syl 17	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (#‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → 𝑉 ⊆ 𝑊)
94	92, 93	sstrd 3578	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (#‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → (𝑥 ∖ {𝑋}) ⊆ 𝑊)
95		difexg 4735	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ V → (𝑥 ∖ {𝑋}) ∈ V)
96	69, 95	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∖ {𝑋}) ∈ V
97	96	elpw 4114	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∖ {𝑋}) ∈ 𝒫 𝑊 ↔ (𝑥 ∖ {𝑋}) ⊆ 𝑊)
98	94, 97	sylibr 223	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (#‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → (𝑥 ∖ {𝑋}) ∈ 𝒫 𝑊)
99	66, 8	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (#‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → 𝑆 ∈ Fin)
100		ssfi 8065	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑆 ∈ Fin ∧ 𝑥 ⊆ 𝑆) → 𝑥 ∈ Fin)
101	99, 68, 100	syl2anc 691	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (#‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → 𝑥 ∈ Fin)
102		diffi 8077	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ Fin → (𝑥 ∖ {𝑋}) ∈ Fin)
103	101, 102	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (#‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → (𝑥 ∖ {𝑋}) ∈ Fin)
104		hashcl 13009	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∖ {𝑋}) ∈ Fin → (#‘(𝑥 ∖ {𝑋})) ∈ ℕ₀)
105		nn0cn 11179	. . . . . . . . . . . . . . 15 ⊢ ((#‘(𝑥 ∖ {𝑋})) ∈ ℕ₀ → (#‘(𝑥 ∖ {𝑋})) ∈ ℂ)
106	103, 104, 105	3syl 18	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (#‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → (#‘(𝑥 ∖ {𝑋})) ∈ ℂ)
107		ax-1cn 9873	. . . . . . . . . . . . . 14 ⊢ 1 ∈ ℂ
108		pncan 10166	. . . . . . . . . . . . . 14 ⊢ (((#‘(𝑥 ∖ {𝑋})) ∈ ℂ ∧ 1 ∈ ℂ) → (((#‘(𝑥 ∖ {𝑋})) + 1) − 1) = (#‘(𝑥 ∖ {𝑋})))
109	106, 107, 108	sylancl 693	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (#‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → (((#‘(𝑥 ∖ {𝑋})) + 1) − 1) = (#‘(𝑥 ∖ {𝑋})))
110		neldifsnd 4263	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (#‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → ¬ 𝑋 ∈ (𝑥 ∖ {𝑋}))
111		hashunsng 13042	. . . . . . . . . . . . . . . . 17 ⊢ (𝑋 ∈ 𝑆 → (((𝑥 ∖ {𝑋}) ∈ Fin ∧ ¬ 𝑋 ∈ (𝑥 ∖ {𝑋})) → (#‘((𝑥 ∖ {𝑋}) ∪ {𝑋})) = ((#‘(𝑥 ∖ {𝑋})) + 1)))
112	66, 5, 111	3syl 18	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (#‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → (((𝑥 ∖ {𝑋}) ∈ Fin ∧ ¬ 𝑋 ∈ (𝑥 ∖ {𝑋})) → (#‘((𝑥 ∖ {𝑋}) ∪ {𝑋})) = ((#‘(𝑥 ∖ {𝑋})) + 1)))
113	103, 110, 112	mp2and 711	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (#‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → (#‘((𝑥 ∖ {𝑋}) ∪ {𝑋})) = ((#‘(𝑥 ∖ {𝑋})) + 1))
114		undif1 3995	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∖ {𝑋}) ∪ {𝑋}) = (𝑥 ∪ {𝑋})
115		simpr 476	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (#‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → ¬ 𝑥 ∈ 𝒫 𝑉)
116	64, 115	eldifd 3551	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (#‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → 𝑥 ∈ (𝒫 (𝑉 ∪ {𝑋}) ∖ 𝒫 𝑉))
117		elpwunsn 4171	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ (𝒫 (𝑉 ∪ {𝑋}) ∖ 𝒫 𝑉) → 𝑋 ∈ 𝑥)
118	116, 117	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (#‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → 𝑋 ∈ 𝑥)
119	118	snssd 4281	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (#‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → {𝑋} ⊆ 𝑥)
120		ssequn2 3748	. . . . . . . . . . . . . . . . . . 19 ⊢ ({𝑋} ⊆ 𝑥 ↔ (𝑥 ∪ {𝑋}) = 𝑥)
121	119, 120	sylib 207	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (#‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → (𝑥 ∪ {𝑋}) = 𝑥)
122	114, 121	syl5req 2657	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (#‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → 𝑥 = ((𝑥 ∖ {𝑋}) ∪ {𝑋}))
123	122	fveq2d 6107	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (#‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → (#‘𝑥) = (#‘((𝑥 ∖ {𝑋}) ∪ {𝑋})))
124	123, 72	eqtr3d 2646	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (#‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → (#‘((𝑥 ∖ {𝑋}) ∪ {𝑋})) = 𝑀)
125	113, 124	eqtr3d 2646	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (#‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → ((#‘(𝑥 ∖ {𝑋})) + 1) = 𝑀)
126	125	oveq1d 6564	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (#‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → (((#‘(𝑥 ∖ {𝑋})) + 1) − 1) = (𝑀 − 1))
127	109, 126	eqtr3d 2646	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (#‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → (#‘(𝑥 ∖ {𝑋})) = (𝑀 − 1))
128		fveq2 6103	. . . . . . . . . . . . . 14 ⊢ (𝑢 = (𝑥 ∖ {𝑋}) → (#‘𝑢) = (#‘(𝑥 ∖ {𝑋})))
129	128	eqeq1d 2612	. . . . . . . . . . . . 13 ⊢ (𝑢 = (𝑥 ∖ {𝑋}) → ((#‘𝑢) = (𝑀 − 1) ↔ (#‘(𝑥 ∖ {𝑋})) = (𝑀 − 1)))
130	129	elrab 3331	. . . . . . . . . . . 12 ⊢ ((𝑥 ∖ {𝑋}) ∈ {𝑢 ∈ 𝒫 𝑊 ∣ (#‘𝑢) = (𝑀 − 1)} ↔ ((𝑥 ∖ {𝑋}) ∈ 𝒫 𝑊 ∧ (#‘(𝑥 ∖ {𝑋})) = (𝑀 − 1)))
131	98, 127, 130	sylanbrc 695	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (#‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → (𝑥 ∖ {𝑋}) ∈ {𝑢 ∈ 𝒫 𝑊 ∣ (#‘𝑢) = (𝑀 − 1)})
132	88, 131	sseldd 3569	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (#‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → (𝑥 ∖ {𝑋}) ∈ (^◡𝐻 “ {𝐷}))
133		ramub1.h	. . . . . . . . . . . 12 ⊢ 𝐻 = (𝑢 ∈ ((𝑆 ∖ {𝑋})𝐶(𝑀 − 1)) ↦ (𝐾‘(𝑢 ∪ {𝑋})))
134	133	mptiniseg 5546	. . . . . . . . . . 11 ⊢ (𝐷 ∈ 𝑅 → (^◡𝐻 “ {𝐷}) = {𝑢 ∈ ((𝑆 ∖ {𝑋})𝐶(𝑀 − 1)) ∣ (𝐾‘(𝑢 ∪ {𝑋})) = 𝐷})
135	66, 19, 134	3syl 18	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (#‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → (^◡𝐻 “ {𝐷}) = {𝑢 ∈ ((𝑆 ∖ {𝑋})𝐶(𝑀 − 1)) ∣ (𝐾‘(𝑢 ∪ {𝑋})) = 𝐷})
136	132, 135	eleqtrd 2690	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (#‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → (𝑥 ∖ {𝑋}) ∈ {𝑢 ∈ ((𝑆 ∖ {𝑋})𝐶(𝑀 − 1)) ∣ (𝐾‘(𝑢 ∪ {𝑋})) = 𝐷})
137		uneq1 3722	. . . . . . . . . . . . 13 ⊢ (𝑢 = (𝑥 ∖ {𝑋}) → (𝑢 ∪ {𝑋}) = ((𝑥 ∖ {𝑋}) ∪ {𝑋}))
138	137	fveq2d 6107	. . . . . . . . . . . 12 ⊢ (𝑢 = (𝑥 ∖ {𝑋}) → (𝐾‘(𝑢 ∪ {𝑋})) = (𝐾‘((𝑥 ∖ {𝑋}) ∪ {𝑋})))
139	138	eqeq1d 2612	. . . . . . . . . . 11 ⊢ (𝑢 = (𝑥 ∖ {𝑋}) → ((𝐾‘(𝑢 ∪ {𝑋})) = 𝐷 ↔ (𝐾‘((𝑥 ∖ {𝑋}) ∪ {𝑋})) = 𝐷))
140	139	elrab 3331	. . . . . . . . . 10 ⊢ ((𝑥 ∖ {𝑋}) ∈ {𝑢 ∈ ((𝑆 ∖ {𝑋})𝐶(𝑀 − 1)) ∣ (𝐾‘(𝑢 ∪ {𝑋})) = 𝐷} ↔ ((𝑥 ∖ {𝑋}) ∈ ((𝑆 ∖ {𝑋})𝐶(𝑀 − 1)) ∧ (𝐾‘((𝑥 ∖ {𝑋}) ∪ {𝑋})) = 𝐷))
141	140	simprbi 479	. . . . . . . . 9 ⊢ ((𝑥 ∖ {𝑋}) ∈ {𝑢 ∈ ((𝑆 ∖ {𝑋})𝐶(𝑀 − 1)) ∣ (𝐾‘(𝑢 ∪ {𝑋})) = 𝐷} → (𝐾‘((𝑥 ∖ {𝑋}) ∪ {𝑋})) = 𝐷)
142	136, 141	syl 17	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (#‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → (𝐾‘((𝑥 ∖ {𝑋}) ∪ {𝑋})) = 𝐷)
143	122	fveq2d 6107	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (#‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → (𝐾‘𝑥) = (𝐾‘((𝑥 ∖ {𝑋}) ∪ {𝑋})))
144		simpl1r 1106	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (#‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → 𝐸 = 𝐷)
145	142, 143, 144	3eqtr4d 2654	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (#‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → (𝐾‘𝑥) = 𝐸)
146		ramub1.6	. . . . . . . . 9 ⊢ (𝜑 → 𝐾:(𝑆𝐶𝑀)⟶𝑅)
147		ffn 5958	. . . . . . . . 9 ⊢ (𝐾:(𝑆𝐶𝑀)⟶𝑅 → 𝐾 Fn (𝑆𝐶𝑀))
148	146, 147	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝐾 Fn (𝑆𝐶𝑀))
149		fniniseg 6246	. . . . . . . 8 ⊢ (𝐾 Fn (𝑆𝐶𝑀) → (𝑥 ∈ (^◡𝐾 “ {𝐸}) ↔ (𝑥 ∈ (𝑆𝐶𝑀) ∧ (𝐾‘𝑥) = 𝐸)))
150	66, 148, 149	3syl 18	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (#‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → (𝑥 ∈ (^◡𝐾 “ {𝐸}) ↔ (𝑥 ∈ (𝑆𝐶𝑀) ∧ (𝐾‘𝑥) = 𝐸)))
151	78, 145, 150	mpbir2and 959	. . . . . 6 ⊢ ((((𝜑 ∧ 𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (#‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → 𝑥 ∈ (^◡𝐾 “ {𝐸}))
152	63, 151	pm2.61dan 828	. . . . 5 ⊢ (((𝜑 ∧ 𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (#‘𝑥) = 𝑀) → 𝑥 ∈ (^◡𝐾 “ {𝐸}))
153	152	rabssdv 3645	. . . 4 ⊢ ((𝜑 ∧ 𝐸 = 𝐷) → {𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∣ (#‘𝑥) = 𝑀} ⊆ (^◡𝐾 “ {𝐸}))
154	52, 153	eqsstrd 3602	. . 3 ⊢ ((𝜑 ∧ 𝐸 = 𝐷) → ((𝑉 ∪ {𝑋})𝐶𝑀) ⊆ (^◡𝐾 “ {𝐸}))
155		fveq2 6103	. . . . . 6 ⊢ (𝑧 = (𝑉 ∪ {𝑋}) → (#‘𝑧) = (#‘(𝑉 ∪ {𝑋})))
156	155	breq2d 4595	. . . . 5 ⊢ (𝑧 = (𝑉 ∪ {𝑋}) → ((𝐹‘𝐸) ≤ (#‘𝑧) ↔ (𝐹‘𝐸) ≤ (#‘(𝑉 ∪ {𝑋}))))
157		oveq1 6556	. . . . . 6 ⊢ (𝑧 = (𝑉 ∪ {𝑋}) → (𝑧𝐶𝑀) = ((𝑉 ∪ {𝑋})𝐶𝑀))
158	157	sseq1d 3595	. . . . 5 ⊢ (𝑧 = (𝑉 ∪ {𝑋}) → ((𝑧𝐶𝑀) ⊆ (^◡𝐾 “ {𝐸}) ↔ ((𝑉 ∪ {𝑋})𝐶𝑀) ⊆ (^◡𝐾 “ {𝐸})))
159	156, 158	anbi12d 743	. . . 4 ⊢ (𝑧 = (𝑉 ∪ {𝑋}) → (((𝐹‘𝐸) ≤ (#‘𝑧) ∧ (𝑧𝐶𝑀) ⊆ (^◡𝐾 “ {𝐸})) ↔ ((𝐹‘𝐸) ≤ (#‘(𝑉 ∪ {𝑋})) ∧ ((𝑉 ∪ {𝑋})𝐶𝑀) ⊆ (^◡𝐾 “ {𝐸}))))
160	159	rspcev 3282	. . 3 ⊢ (((𝑉 ∪ {𝑋}) ∈ 𝒫 𝑆 ∧ ((𝐹‘𝐸) ≤ (#‘(𝑉 ∪ {𝑋})) ∧ ((𝑉 ∪ {𝑋})𝐶𝑀) ⊆ (^◡𝐾 “ {𝐸}))) → ∃𝑧 ∈ 𝒫 𝑆((𝐹‘𝐸) ≤ (#‘𝑧) ∧ (𝑧𝐶𝑀) ⊆ (^◡𝐾 “ {𝐸})))
161	12, 43, 154, 160	syl12anc 1316	. 2 ⊢ ((𝜑 ∧ 𝐸 = 𝐷) → ∃𝑧 ∈ 𝒫 𝑆((𝐹‘𝐸) ≤ (#‘𝑧) ∧ (𝑧𝐶𝑀) ⊆ (^◡𝐾 “ {𝐸})))
162		elpw2g 4754	. . . . . 6 ⊢ (𝑆 ∈ Fin → (𝑉 ∈ 𝒫 𝑆 ↔ 𝑉 ⊆ 𝑆))
163	8, 162	syl 17	. . . . 5 ⊢ (𝜑 → (𝑉 ∈ 𝒫 𝑆 ↔ 𝑉 ⊆ 𝑆))
164	4, 163	mpbird 246	. . . 4 ⊢ (𝜑 → 𝑉 ∈ 𝒫 𝑆)
165	164	adantr 480	. . 3 ⊢ ((𝜑 ∧ 𝐸 ≠ 𝐷) → 𝑉 ∈ 𝒫 𝑆)
166		ifnefalse 4048	. . . . 5 ⊢ (𝐸 ≠ 𝐷 → if(𝐸 = 𝐷, ((𝐹‘𝐷) − 1), (𝐹‘𝐸)) = (𝐹‘𝐸))
167	166	adantl 481	. . . 4 ⊢ ((𝜑 ∧ 𝐸 ≠ 𝐷) → if(𝐸 = 𝐷, ((𝐹‘𝐷) − 1), (𝐹‘𝐸)) = (𝐹‘𝐸))
168	15	adantr 480	. . . 4 ⊢ ((𝜑 ∧ 𝐸 ≠ 𝐷) → if(𝐸 = 𝐷, ((𝐹‘𝐷) − 1), (𝐹‘𝐸)) ≤ (#‘𝑉))
169	167, 168	eqbrtrrd 4607	. . 3 ⊢ ((𝜑 ∧ 𝐸 ≠ 𝐷) → (𝐹‘𝐸) ≤ (#‘𝑉))
170	56	adantr 480	. . 3 ⊢ ((𝜑 ∧ 𝐸 ≠ 𝐷) → (𝑉𝐶𝑀) ⊆ (^◡𝐾 “ {𝐸}))
171		fveq2 6103	. . . . . 6 ⊢ (𝑧 = 𝑉 → (#‘𝑧) = (#‘𝑉))
172	171	breq2d 4595	. . . . 5 ⊢ (𝑧 = 𝑉 → ((𝐹‘𝐸) ≤ (#‘𝑧) ↔ (𝐹‘𝐸) ≤ (#‘𝑉)))
173		oveq1 6556	. . . . . 6 ⊢ (𝑧 = 𝑉 → (𝑧𝐶𝑀) = (𝑉𝐶𝑀))
174	173	sseq1d 3595	. . . . 5 ⊢ (𝑧 = 𝑉 → ((𝑧𝐶𝑀) ⊆ (^◡𝐾 “ {𝐸}) ↔ (𝑉𝐶𝑀) ⊆ (^◡𝐾 “ {𝐸})))
175	172, 174	anbi12d 743	. . . 4 ⊢ (𝑧 = 𝑉 → (((𝐹‘𝐸) ≤ (#‘𝑧) ∧ (𝑧𝐶𝑀) ⊆ (^◡𝐾 “ {𝐸})) ↔ ((𝐹‘𝐸) ≤ (#‘𝑉) ∧ (𝑉𝐶𝑀) ⊆ (^◡𝐾 “ {𝐸}))))
176	175	rspcev 3282	. . 3 ⊢ ((𝑉 ∈ 𝒫 𝑆 ∧ ((𝐹‘𝐸) ≤ (#‘𝑉) ∧ (𝑉𝐶𝑀) ⊆ (^◡𝐾 “ {𝐸}))) → ∃𝑧 ∈ 𝒫 𝑆((𝐹‘𝐸) ≤ (#‘𝑧) ∧ (𝑧𝐶𝑀) ⊆ (^◡𝐾 “ {𝐸})))
177	165, 169, 170, 176	syl12anc 1316	. 2 ⊢ ((𝜑 ∧ 𝐸 ≠ 𝐷) → ∃𝑧 ∈ 𝒫 𝑆((𝐹‘𝐸) ≤ (#‘𝑧) ∧ (𝑧𝐶𝑀) ⊆ (^◡𝐾 “ {𝐸})))
178	161, 177	pm2.61dane 2869	1 ⊢ (𝜑 → ∃𝑧 ∈ 𝒫 𝑆((𝐹‘𝐸) ≤ (#‘𝑧) ∧ (𝑧𝐶𝑀) ⊆ (^◡𝐾 “ {𝐸})))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 195 ∧ wa 383 ∧ w3a 1031 = wceq 1475 ∈ wcel 1977 ≠ wne 2780 ∃wrex 2897 {crab 2900 Vcvv 3173 ∖ cdif 3537 ∪ cun 3538 ⊆ wss 3540 ifcif 4036 𝒫 cpw 4108 {csn 4125 class class class wbr 4583 ↦ cmpt 4643 ^◡ccnv 5037 “ cima 5041 Fn wfn 5799 ⟶wf 5800 ‘cfv 5804 (class class class)co 6549 ↦ cmpt2 6551 Fincfn 7841 ℂcc 9813 ℝcr 9814 1c1 9816 + caddc 9818 ≤ cle 9954 − cmin 10145 ℕcn 10897 ℕ₀cn0 11169 #chash 12979 Ramsey cram 15541

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-8 1979 ax-9 1986 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-rep 4699 ax-sep 4709 ax-nul 4717 ax-pow 4769 ax-pr 4833 ax-un 6847 ax-cnex 9871 ax-resscn 9872 ax-1cn 9873 ax-icn 9874 ax-addcl 9875 ax-addrcl 9876 ax-mulcl 9877 ax-mulrcl 9878 ax-mulcom 9879 ax-addass 9880 ax-mulass 9881 ax-distr 9882 ax-i2m1 9883 ax-1ne0 9884 ax-1rid 9885 ax-rnegex 9886 ax-rrecex 9887 ax-cnre 9888 ax-pre-lttri 9889 ax-pre-lttrn 9890 ax-pre-ltadd 9891 ax-pre-mulgt0 9892

This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3or 1032 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-eu 2462 df-mo 2463 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ne 2782 df-nel 2783 df-ral 2901 df-rex 2902 df-reu 2903 df-rmo 2904 df-rab 2905 df-v 3175 df-sbc 3403 df-csb 3500 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-pss 3556 df-nul 3875 df-if 4037 df-pw 4110 df-sn 4126 df-pr 4128 df-tp 4130 df-op 4132 df-uni 4373 df-int 4411 df-iun 4457 df-br 4584 df-opab 4644 df-mpt 4645 df-tr 4681 df-eprel 4949 df-id 4953 df-po 4959 df-so 4960 df-fr 4997 df-we 4999 df-xp 5044 df-rel 5045 df-cnv 5046 df-co 5047 df-dm 5048 df-rn 5049 df-res 5050 df-ima 5051 df-pred 5597 df-ord 5643 df-on 5644 df-lim 5645 df-suc 5646 df-iota 5768 df-fun 5806 df-fn 5807 df-f 5808 df-f1 5809 df-fo 5810 df-f1o 5811 df-fv 5812 df-riota 6511 df-ov 6552 df-oprab 6553 df-mpt2 6554 df-om 6958 df-1st 7059 df-2nd 7060 df-wrecs 7294 df-recs 7355 df-rdg 7393 df-1o 7447 df-oadd 7451 df-er 7629 df-en 7842 df-dom 7843 df-sdom 7844 df-fin 7845 df-card 8648 df-cda 8873 df-pnf 9955 df-mnf 9956 df-xr 9957 df-ltxr 9958 df-le 9959 df-sub 10147 df-neg 10148 df-nn 10898 df-n0 11170 df-z 11255 df-uz 11564 df-fz 12198 df-hash 12980

This theorem is referenced by: ramub1lem2 15569

W3C validator