ramub1lem2 - Metamath Proof Explorer

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

Theorem ramub1lem2 15731

Description: Lemma for ramub1 15732. (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)) ↦ (𝐾‘(𝑢 ∪ {𝑋})))

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

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

Proof of Theorem ramub1lem2 Dummy variables 𝑑 𝑣 𝑤 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ramub1.3	. . 3 ⊢ 𝐶 = (𝑎 ∈ V, 𝑖 ∈ ℕ₀ ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (#‘𝑏) = 𝑖})
2		ramub1.m	. . . 4 ⊢ (𝜑 → 𝑀 ∈ ℕ)
3		nnm1nn0 11334	. . . 4 ⊢ (𝑀 ∈ ℕ → (𝑀 − 1) ∈ ℕ₀)
4	2, 3	syl 17	. . 3 ⊢ (𝜑 → (𝑀 − 1) ∈ ℕ₀)
5		ramub1.r	. . 3 ⊢ (𝜑 → 𝑅 ∈ Fin)
6		ramub1.1	. . 3 ⊢ (𝜑 → 𝐺:𝑅⟶ℕ₀)
7		ramub1.2	. . 3 ⊢ (𝜑 → ((𝑀 − 1) Ramsey 𝐺) ∈ ℕ₀)
8		ramub1.4	. . . 4 ⊢ (𝜑 → 𝑆 ∈ Fin)
9		diffi 8192	. . . 4 ⊢ (𝑆 ∈ Fin → (𝑆 ∖ {𝑋}) ∈ Fin)
10	8, 9	syl 17	. . 3 ⊢ (𝜑 → (𝑆 ∖ {𝑋}) ∈ Fin)
11	7	nn0red 11352	. . . . 5 ⊢ (𝜑 → ((𝑀 − 1) Ramsey 𝐺) ∈ ℝ)
12	11	leidd 10594	. . . 4 ⊢ (𝜑 → ((𝑀 − 1) Ramsey 𝐺) ≤ ((𝑀 − 1) Ramsey 𝐺))
13		hashcl 13147	. . . . . . 7 ⊢ ((𝑆 ∖ {𝑋}) ∈ Fin → (#‘(𝑆 ∖ {𝑋})) ∈ ℕ₀)
14	10, 13	syl 17	. . . . . 6 ⊢ (𝜑 → (#‘(𝑆 ∖ {𝑋})) ∈ ℕ₀)
15	14	nn0cnd 11353	. . . . 5 ⊢ (𝜑 → (#‘(𝑆 ∖ {𝑋})) ∈ ℂ)
16	7	nn0cnd 11353	. . . . 5 ⊢ (𝜑 → ((𝑀 − 1) Ramsey 𝐺) ∈ ℂ)
17		1cnd 10056	. . . . 5 ⊢ (𝜑 → 1 ∈ ℂ)
18		undif1 4043	. . . . . . . 8 ⊢ ((𝑆 ∖ {𝑋}) ∪ {𝑋}) = (𝑆 ∪ {𝑋})
19		ramub1.x	. . . . . . . . . 10 ⊢ (𝜑 → 𝑋 ∈ 𝑆)
20	19	snssd 4340	. . . . . . . . 9 ⊢ (𝜑 → {𝑋} ⊆ 𝑆)
21		ssequn2 3786	. . . . . . . . 9 ⊢ ({𝑋} ⊆ 𝑆 ↔ (𝑆 ∪ {𝑋}) = 𝑆)
22	20, 21	sylib 208	. . . . . . . 8 ⊢ (𝜑 → (𝑆 ∪ {𝑋}) = 𝑆)
23	18, 22	syl5eq 2668	. . . . . . 7 ⊢ (𝜑 → ((𝑆 ∖ {𝑋}) ∪ {𝑋}) = 𝑆)
24	23	fveq2d 6195	. . . . . 6 ⊢ (𝜑 → (#‘((𝑆 ∖ {𝑋}) ∪ {𝑋})) = (#‘𝑆))
25		neldifsnd 4322	. . . . . . 7 ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑆 ∖ {𝑋}))
26		hashunsng 13181	. . . . . . . 8 ⊢ (𝑋 ∈ 𝑆 → (((𝑆 ∖ {𝑋}) ∈ Fin ∧ ¬ 𝑋 ∈ (𝑆 ∖ {𝑋})) → (#‘((𝑆 ∖ {𝑋}) ∪ {𝑋})) = ((#‘(𝑆 ∖ {𝑋})) + 1)))
27	19, 26	syl 17	. . . . . . 7 ⊢ (𝜑 → (((𝑆 ∖ {𝑋}) ∈ Fin ∧ ¬ 𝑋 ∈ (𝑆 ∖ {𝑋})) → (#‘((𝑆 ∖ {𝑋}) ∪ {𝑋})) = ((#‘(𝑆 ∖ {𝑋})) + 1)))
28	10, 25, 27	mp2and 715	. . . . . 6 ⊢ (𝜑 → (#‘((𝑆 ∖ {𝑋}) ∪ {𝑋})) = ((#‘(𝑆 ∖ {𝑋})) + 1))
29		ramub1.5	. . . . . 6 ⊢ (𝜑 → (#‘𝑆) = (((𝑀 − 1) Ramsey 𝐺) + 1))
30	24, 28, 29	3eqtr3d 2664	. . . . 5 ⊢ (𝜑 → ((#‘(𝑆 ∖ {𝑋})) + 1) = (((𝑀 − 1) Ramsey 𝐺) + 1))
31	15, 16, 17, 30	addcan2ad 10242	. . . 4 ⊢ (𝜑 → (#‘(𝑆 ∖ {𝑋})) = ((𝑀 − 1) Ramsey 𝐺))
32	12, 31	breqtrrd 4681	. . 3 ⊢ (𝜑 → ((𝑀 − 1) Ramsey 𝐺) ≤ (#‘(𝑆 ∖ {𝑋})))
33		ramub1.6	. . . . . 6 ⊢ (𝜑 → 𝐾:(𝑆𝐶𝑀)⟶𝑅)
34	33	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ 𝑢 ∈ ((𝑆 ∖ {𝑋})𝐶(𝑀 − 1))) → 𝐾:(𝑆𝐶𝑀)⟶𝑅)
35	1	hashbcval 15706	. . . . . . . . . . . . . . 15 ⊢ (((𝑆 ∖ {𝑋}) ∈ Fin ∧ (𝑀 − 1) ∈ ℕ₀) → ((𝑆 ∖ {𝑋})𝐶(𝑀 − 1)) = {𝑥 ∈ 𝒫 (𝑆 ∖ {𝑋}) ∣ (#‘𝑥) = (𝑀 − 1)})
36	10, 4, 35	syl2anc 693	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑆 ∖ {𝑋})𝐶(𝑀 − 1)) = {𝑥 ∈ 𝒫 (𝑆 ∖ {𝑋}) ∣ (#‘𝑥) = (𝑀 − 1)})
37	36	eleq2d 2687	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑢 ∈ ((𝑆 ∖ {𝑋})𝐶(𝑀 − 1)) ↔ 𝑢 ∈ {𝑥 ∈ 𝒫 (𝑆 ∖ {𝑋}) ∣ (#‘𝑥) = (𝑀 − 1)}))
38		fveq2 6191	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑢 → (#‘𝑥) = (#‘𝑢))
39	38	eqeq1d 2624	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑢 → ((#‘𝑥) = (𝑀 − 1) ↔ (#‘𝑢) = (𝑀 − 1)))
40	39	elrab 3363	. . . . . . . . . . . . 13 ⊢ (𝑢 ∈ {𝑥 ∈ 𝒫 (𝑆 ∖ {𝑋}) ∣ (#‘𝑥) = (𝑀 − 1)} ↔ (𝑢 ∈ 𝒫 (𝑆 ∖ {𝑋}) ∧ (#‘𝑢) = (𝑀 − 1)))
41	37, 40	syl6bb 276	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑢 ∈ ((𝑆 ∖ {𝑋})𝐶(𝑀 − 1)) ↔ (𝑢 ∈ 𝒫 (𝑆 ∖ {𝑋}) ∧ (#‘𝑢) = (𝑀 − 1))))
42	41	simprbda 653	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑢 ∈ ((𝑆 ∖ {𝑋})𝐶(𝑀 − 1))) → 𝑢 ∈ 𝒫 (𝑆 ∖ {𝑋}))
43	42	elpwid 4170	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ ((𝑆 ∖ {𝑋})𝐶(𝑀 − 1))) → 𝑢 ⊆ (𝑆 ∖ {𝑋}))
44	43	difss2d 3740	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑢 ∈ ((𝑆 ∖ {𝑋})𝐶(𝑀 − 1))) → 𝑢 ⊆ 𝑆)
45	20	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑢 ∈ ((𝑆 ∖ {𝑋})𝐶(𝑀 − 1))) → {𝑋} ⊆ 𝑆)
46	44, 45	unssd 3789	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑢 ∈ ((𝑆 ∖ {𝑋})𝐶(𝑀 − 1))) → (𝑢 ∪ {𝑋}) ⊆ 𝑆)
47		vex 3203	. . . . . . . . . 10 ⊢ 𝑢 ∈ V
48		snex 4908	. . . . . . . . . 10 ⊢ {𝑋} ∈ V
49	47, 48	unex 6956	. . . . . . . . 9 ⊢ (𝑢 ∪ {𝑋}) ∈ V
50	49	elpw 4164	. . . . . . . 8 ⊢ ((𝑢 ∪ {𝑋}) ∈ 𝒫 𝑆 ↔ (𝑢 ∪ {𝑋}) ⊆ 𝑆)
51	46, 50	sylibr 224	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑢 ∈ ((𝑆 ∖ {𝑋})𝐶(𝑀 − 1))) → (𝑢 ∪ {𝑋}) ∈ 𝒫 𝑆)
52	10	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ ((𝑆 ∖ {𝑋})𝐶(𝑀 − 1))) → (𝑆 ∖ {𝑋}) ∈ Fin)
53		ssfi 8180	. . . . . . . . . 10 ⊢ (((𝑆 ∖ {𝑋}) ∈ Fin ∧ 𝑢 ⊆ (𝑆 ∖ {𝑋})) → 𝑢 ∈ Fin)
54	52, 43, 53	syl2anc 693	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑢 ∈ ((𝑆 ∖ {𝑋})𝐶(𝑀 − 1))) → 𝑢 ∈ Fin)
55		neldifsnd 4322	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ ((𝑆 ∖ {𝑋})𝐶(𝑀 − 1))) → ¬ 𝑋 ∈ (𝑆 ∖ {𝑋}))
56	43, 55	ssneldd 3606	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑢 ∈ ((𝑆 ∖ {𝑋})𝐶(𝑀 − 1))) → ¬ 𝑋 ∈ 𝑢)
57	19	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ ((𝑆 ∖ {𝑋})𝐶(𝑀 − 1))) → 𝑋 ∈ 𝑆)
58		hashunsng 13181	. . . . . . . . . 10 ⊢ (𝑋 ∈ 𝑆 → ((𝑢 ∈ Fin ∧ ¬ 𝑋 ∈ 𝑢) → (#‘(𝑢 ∪ {𝑋})) = ((#‘𝑢) + 1)))
59	57, 58	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑢 ∈ ((𝑆 ∖ {𝑋})𝐶(𝑀 − 1))) → ((𝑢 ∈ Fin ∧ ¬ 𝑋 ∈ 𝑢) → (#‘(𝑢 ∪ {𝑋})) = ((#‘𝑢) + 1)))
60	54, 56, 59	mp2and 715	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑢 ∈ ((𝑆 ∖ {𝑋})𝐶(𝑀 − 1))) → (#‘(𝑢 ∪ {𝑋})) = ((#‘𝑢) + 1))
61	41	simplbda 654	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑢 ∈ ((𝑆 ∖ {𝑋})𝐶(𝑀 − 1))) → (#‘𝑢) = (𝑀 − 1))
62	61	oveq1d 6665	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑢 ∈ ((𝑆 ∖ {𝑋})𝐶(𝑀 − 1))) → ((#‘𝑢) + 1) = ((𝑀 − 1) + 1))
63	2	nncnd 11036	. . . . . . . . . 10 ⊢ (𝜑 → 𝑀 ∈ ℂ)
64		ax-1cn 9994	. . . . . . . . . 10 ⊢ 1 ∈ ℂ
65		npcan 10290	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑀 − 1) + 1) = 𝑀)
66	63, 64, 65	sylancl 694	. . . . . . . . 9 ⊢ (𝜑 → ((𝑀 − 1) + 1) = 𝑀)
67	66	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑢 ∈ ((𝑆 ∖ {𝑋})𝐶(𝑀 − 1))) → ((𝑀 − 1) + 1) = 𝑀)
68	60, 62, 67	3eqtrd 2660	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑢 ∈ ((𝑆 ∖ {𝑋})𝐶(𝑀 − 1))) → (#‘(𝑢 ∪ {𝑋})) = 𝑀)
69		fveq2 6191	. . . . . . . . 9 ⊢ (𝑥 = (𝑢 ∪ {𝑋}) → (#‘𝑥) = (#‘(𝑢 ∪ {𝑋})))
70	69	eqeq1d 2624	. . . . . . . 8 ⊢ (𝑥 = (𝑢 ∪ {𝑋}) → ((#‘𝑥) = 𝑀 ↔ (#‘(𝑢 ∪ {𝑋})) = 𝑀))
71	70	elrab 3363	. . . . . . 7 ⊢ ((𝑢 ∪ {𝑋}) ∈ {𝑥 ∈ 𝒫 𝑆 ∣ (#‘𝑥) = 𝑀} ↔ ((𝑢 ∪ {𝑋}) ∈ 𝒫 𝑆 ∧ (#‘(𝑢 ∪ {𝑋})) = 𝑀))
72	51, 68, 71	sylanbrc 698	. . . . . 6 ⊢ ((𝜑 ∧ 𝑢 ∈ ((𝑆 ∖ {𝑋})𝐶(𝑀 − 1))) → (𝑢 ∪ {𝑋}) ∈ {𝑥 ∈ 𝒫 𝑆 ∣ (#‘𝑥) = 𝑀})
73	2	nnnn0d 11351	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∈ ℕ₀)
74	1	hashbcval 15706	. . . . . . . 8 ⊢ ((𝑆 ∈ Fin ∧ 𝑀 ∈ ℕ₀) → (𝑆𝐶𝑀) = {𝑥 ∈ 𝒫 𝑆 ∣ (#‘𝑥) = 𝑀})
75	8, 73, 74	syl2anc 693	. . . . . . 7 ⊢ (𝜑 → (𝑆𝐶𝑀) = {𝑥 ∈ 𝒫 𝑆 ∣ (#‘𝑥) = 𝑀})
76	75	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑢 ∈ ((𝑆 ∖ {𝑋})𝐶(𝑀 − 1))) → (𝑆𝐶𝑀) = {𝑥 ∈ 𝒫 𝑆 ∣ (#‘𝑥) = 𝑀})
77	72, 76	eleqtrrd 2704	. . . . 5 ⊢ ((𝜑 ∧ 𝑢 ∈ ((𝑆 ∖ {𝑋})𝐶(𝑀 − 1))) → (𝑢 ∪ {𝑋}) ∈ (𝑆𝐶𝑀))
78	34, 77	ffvelrnd 6360	. . . 4 ⊢ ((𝜑 ∧ 𝑢 ∈ ((𝑆 ∖ {𝑋})𝐶(𝑀 − 1))) → (𝐾‘(𝑢 ∪ {𝑋})) ∈ 𝑅)
79		ramub1.h	. . . 4 ⊢ 𝐻 = (𝑢 ∈ ((𝑆 ∖ {𝑋})𝐶(𝑀 − 1)) ↦ (𝐾‘(𝑢 ∪ {𝑋})))
80	78, 79	fmptd 6385	. . 3 ⊢ (𝜑 → 𝐻:((𝑆 ∖ {𝑋})𝐶(𝑀 − 1))⟶𝑅)
81	1, 4, 5, 6, 7, 10, 32, 80	rami 15719	. 2 ⊢ (𝜑 → ∃𝑑 ∈ 𝑅 ∃𝑤 ∈ 𝒫 (𝑆 ∖ {𝑋})((𝐺‘𝑑) ≤ (#‘𝑤) ∧ (𝑤𝐶(𝑀 − 1)) ⊆ (^◡𝐻 “ {𝑑})))
82	73	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑑 ∈ 𝑅 ∧ 𝑤 ∈ 𝒫 (𝑆 ∖ {𝑋})) ∧ ((𝐺‘𝑑) ≤ (#‘𝑤) ∧ (𝑤𝐶(𝑀 − 1)) ⊆ (^◡𝐻 “ {𝑑})))) → 𝑀 ∈ ℕ₀)
83	5	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑑 ∈ 𝑅 ∧ 𝑤 ∈ 𝒫 (𝑆 ∖ {𝑋})) ∧ ((𝐺‘𝑑) ≤ (#‘𝑤) ∧ (𝑤𝐶(𝑀 − 1)) ⊆ (^◡𝐻 “ {𝑑})))) → 𝑅 ∈ Fin)
84		ramub1.f	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐹:𝑅⟶ℕ)
85	84	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑑 ∈ 𝑅 ∧ 𝑤 ∈ 𝒫 (𝑆 ∖ {𝑋})) ∧ ((𝐺‘𝑑) ≤ (#‘𝑤) ∧ (𝑤𝐶(𝑀 − 1)) ⊆ (^◡𝐻 “ {𝑑})))) → 𝐹:𝑅⟶ℕ)
86		simprll 802	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑑 ∈ 𝑅 ∧ 𝑤 ∈ 𝒫 (𝑆 ∖ {𝑋})) ∧ ((𝐺‘𝑑) ≤ (#‘𝑤) ∧ (𝑤𝐶(𝑀 − 1)) ⊆ (^◡𝐻 “ {𝑑})))) → 𝑑 ∈ 𝑅)
87	85, 86	ffvelrnd 6360	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑑 ∈ 𝑅 ∧ 𝑤 ∈ 𝒫 (𝑆 ∖ {𝑋})) ∧ ((𝐺‘𝑑) ≤ (#‘𝑤) ∧ (𝑤𝐶(𝑀 − 1)) ⊆ (^◡𝐻 “ {𝑑})))) → (𝐹‘𝑑) ∈ ℕ)
88		nnm1nn0 11334	. . . . . . . . . 10 ⊢ ((𝐹‘𝑑) ∈ ℕ → ((𝐹‘𝑑) − 1) ∈ ℕ₀)
89	87, 88	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑑 ∈ 𝑅 ∧ 𝑤 ∈ 𝒫 (𝑆 ∖ {𝑋})) ∧ ((𝐺‘𝑑) ≤ (#‘𝑤) ∧ (𝑤𝐶(𝑀 − 1)) ⊆ (^◡𝐻 “ {𝑑})))) → ((𝐹‘𝑑) − 1) ∈ ℕ₀)
90	89	adantr 481	. . . . . . . 8 ⊢ (((𝜑 ∧ ((𝑑 ∈ 𝑅 ∧ 𝑤 ∈ 𝒫 (𝑆 ∖ {𝑋})) ∧ ((𝐺‘𝑑) ≤ (#‘𝑤) ∧ (𝑤𝐶(𝑀 − 1)) ⊆ (^◡𝐻 “ {𝑑})))) ∧ 𝑦 ∈ 𝑅) → ((𝐹‘𝑑) − 1) ∈ ℕ₀)
91	85	ffvelrnda 6359	. . . . . . . . 9 ⊢ (((𝜑 ∧ ((𝑑 ∈ 𝑅 ∧ 𝑤 ∈ 𝒫 (𝑆 ∖ {𝑋})) ∧ ((𝐺‘𝑑) ≤ (#‘𝑤) ∧ (𝑤𝐶(𝑀 − 1)) ⊆ (^◡𝐻 “ {𝑑})))) ∧ 𝑦 ∈ 𝑅) → (𝐹‘𝑦) ∈ ℕ)
92	91	nnnn0d 11351	. . . . . . . 8 ⊢ (((𝜑 ∧ ((𝑑 ∈ 𝑅 ∧ 𝑤 ∈ 𝒫 (𝑆 ∖ {𝑋})) ∧ ((𝐺‘𝑑) ≤ (#‘𝑤) ∧ (𝑤𝐶(𝑀 − 1)) ⊆ (^◡𝐻 “ {𝑑})))) ∧ 𝑦 ∈ 𝑅) → (𝐹‘𝑦) ∈ ℕ₀)
93	90, 92	ifcld 4131	. . . . . . 7 ⊢ (((𝜑 ∧ ((𝑑 ∈ 𝑅 ∧ 𝑤 ∈ 𝒫 (𝑆 ∖ {𝑋})) ∧ ((𝐺‘𝑑) ≤ (#‘𝑤) ∧ (𝑤𝐶(𝑀 − 1)) ⊆ (^◡𝐻 “ {𝑑})))) ∧ 𝑦 ∈ 𝑅) → if(𝑦 = 𝑑, ((𝐹‘𝑑) − 1), (𝐹‘𝑦)) ∈ ℕ₀)
94		eqid 2622	. . . . . . 7 ⊢ (𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑑, ((𝐹‘𝑑) − 1), (𝐹‘𝑦))) = (𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑑, ((𝐹‘𝑑) − 1), (𝐹‘𝑦)))
95	93, 94	fmptd 6385	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑑 ∈ 𝑅 ∧ 𝑤 ∈ 𝒫 (𝑆 ∖ {𝑋})) ∧ ((𝐺‘𝑑) ≤ (#‘𝑤) ∧ (𝑤𝐶(𝑀 − 1)) ⊆ (^◡𝐻 “ {𝑑})))) → (𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑑, ((𝐹‘𝑑) − 1), (𝐹‘𝑦))):𝑅⟶ℕ₀)
96		equequ2 1953	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑑 → (𝑦 = 𝑥 ↔ 𝑦 = 𝑑))
97		fveq2 6191	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑑 → (𝐹‘𝑥) = (𝐹‘𝑑))
98	97	oveq1d 6665	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑑 → ((𝐹‘𝑥) − 1) = ((𝐹‘𝑑) − 1))
99	96, 98	ifbieq1d 4109	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑑 → if(𝑦 = 𝑥, ((𝐹‘𝑥) − 1), (𝐹‘𝑦)) = if(𝑦 = 𝑑, ((𝐹‘𝑑) − 1), (𝐹‘𝑦)))
100	99	mpteq2dv 4745	. . . . . . . . . 10 ⊢ (𝑥 = 𝑑 → (𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑥, ((𝐹‘𝑥) − 1), (𝐹‘𝑦))) = (𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑑, ((𝐹‘𝑑) − 1), (𝐹‘𝑦))))
101	100	oveq2d 6666	. . . . . . . . 9 ⊢ (𝑥 = 𝑑 → (𝑀 Ramsey (𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑥, ((𝐹‘𝑥) − 1), (𝐹‘𝑦)))) = (𝑀 Ramsey (𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑑, ((𝐹‘𝑑) − 1), (𝐹‘𝑦)))))
102		ramub1.g	. . . . . . . . 9 ⊢ 𝐺 = (𝑥 ∈ 𝑅 ↦ (𝑀 Ramsey (𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑥, ((𝐹‘𝑥) − 1), (𝐹‘𝑦)))))
103		ovex 6678	. . . . . . . . 9 ⊢ (𝑀 Ramsey (𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑑, ((𝐹‘𝑑) − 1), (𝐹‘𝑦)))) ∈ V
104	101, 102, 103	fvmpt 6282	. . . . . . . 8 ⊢ (𝑑 ∈ 𝑅 → (𝐺‘𝑑) = (𝑀 Ramsey (𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑑, ((𝐹‘𝑑) − 1), (𝐹‘𝑦)))))
105	86, 104	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑑 ∈ 𝑅 ∧ 𝑤 ∈ 𝒫 (𝑆 ∖ {𝑋})) ∧ ((𝐺‘𝑑) ≤ (#‘𝑤) ∧ (𝑤𝐶(𝑀 − 1)) ⊆ (^◡𝐻 “ {𝑑})))) → (𝐺‘𝑑) = (𝑀 Ramsey (𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑑, ((𝐹‘𝑑) − 1), (𝐹‘𝑦)))))
106	6	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑑 ∈ 𝑅 ∧ 𝑤 ∈ 𝒫 (𝑆 ∖ {𝑋})) ∧ ((𝐺‘𝑑) ≤ (#‘𝑤) ∧ (𝑤𝐶(𝑀 − 1)) ⊆ (^◡𝐻 “ {𝑑})))) → 𝐺:𝑅⟶ℕ₀)
107	106, 86	ffvelrnd 6360	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑑 ∈ 𝑅 ∧ 𝑤 ∈ 𝒫 (𝑆 ∖ {𝑋})) ∧ ((𝐺‘𝑑) ≤ (#‘𝑤) ∧ (𝑤𝐶(𝑀 − 1)) ⊆ (^◡𝐻 “ {𝑑})))) → (𝐺‘𝑑) ∈ ℕ₀)
108	105, 107	eqeltrrd 2702	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑑 ∈ 𝑅 ∧ 𝑤 ∈ 𝒫 (𝑆 ∖ {𝑋})) ∧ ((𝐺‘𝑑) ≤ (#‘𝑤) ∧ (𝑤𝐶(𝑀 − 1)) ⊆ (^◡𝐻 “ {𝑑})))) → (𝑀 Ramsey (𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑑, ((𝐹‘𝑑) − 1), (𝐹‘𝑦)))) ∈ ℕ₀)
109		simprlr 803	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑑 ∈ 𝑅 ∧ 𝑤 ∈ 𝒫 (𝑆 ∖ {𝑋})) ∧ ((𝐺‘𝑑) ≤ (#‘𝑤) ∧ (𝑤𝐶(𝑀 − 1)) ⊆ (^◡𝐻 “ {𝑑})))) → 𝑤 ∈ 𝒫 (𝑆 ∖ {𝑋}))
110		simprrl 804	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑑 ∈ 𝑅 ∧ 𝑤 ∈ 𝒫 (𝑆 ∖ {𝑋})) ∧ ((𝐺‘𝑑) ≤ (#‘𝑤) ∧ (𝑤𝐶(𝑀 − 1)) ⊆ (^◡𝐻 “ {𝑑})))) → (𝐺‘𝑑) ≤ (#‘𝑤))
111	105, 110	eqbrtrrd 4677	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑑 ∈ 𝑅 ∧ 𝑤 ∈ 𝒫 (𝑆 ∖ {𝑋})) ∧ ((𝐺‘𝑑) ≤ (#‘𝑤) ∧ (𝑤𝐶(𝑀 − 1)) ⊆ (^◡𝐻 “ {𝑑})))) → (𝑀 Ramsey (𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑑, ((𝐹‘𝑑) − 1), (𝐹‘𝑦)))) ≤ (#‘𝑤))
112	33	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑑 ∈ 𝑅 ∧ 𝑤 ∈ 𝒫 (𝑆 ∖ {𝑋})) ∧ ((𝐺‘𝑑) ≤ (#‘𝑤) ∧ (𝑤𝐶(𝑀 − 1)) ⊆ (^◡𝐻 “ {𝑑})))) → 𝐾:(𝑆𝐶𝑀)⟶𝑅)
113	8	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑑 ∈ 𝑅 ∧ 𝑤 ∈ 𝒫 (𝑆 ∖ {𝑋})) ∧ ((𝐺‘𝑑) ≤ (#‘𝑤) ∧ (𝑤𝐶(𝑀 − 1)) ⊆ (^◡𝐻 “ {𝑑})))) → 𝑆 ∈ Fin)
114	109	elpwid 4170	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑑 ∈ 𝑅 ∧ 𝑤 ∈ 𝒫 (𝑆 ∖ {𝑋})) ∧ ((𝐺‘𝑑) ≤ (#‘𝑤) ∧ (𝑤𝐶(𝑀 − 1)) ⊆ (^◡𝐻 “ {𝑑})))) → 𝑤 ⊆ (𝑆 ∖ {𝑋}))
115	114	difss2d 3740	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑑 ∈ 𝑅 ∧ 𝑤 ∈ 𝒫 (𝑆 ∖ {𝑋})) ∧ ((𝐺‘𝑑) ≤ (#‘𝑤) ∧ (𝑤𝐶(𝑀 − 1)) ⊆ (^◡𝐻 “ {𝑑})))) → 𝑤 ⊆ 𝑆)
116	1	hashbcss 15708	. . . . . . . 8 ⊢ ((𝑆 ∈ Fin ∧ 𝑤 ⊆ 𝑆 ∧ 𝑀 ∈ ℕ₀) → (𝑤𝐶𝑀) ⊆ (𝑆𝐶𝑀))
117	113, 115, 82, 116	syl3anc 1326	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑑 ∈ 𝑅 ∧ 𝑤 ∈ 𝒫 (𝑆 ∖ {𝑋})) ∧ ((𝐺‘𝑑) ≤ (#‘𝑤) ∧ (𝑤𝐶(𝑀 − 1)) ⊆ (^◡𝐻 “ {𝑑})))) → (𝑤𝐶𝑀) ⊆ (𝑆𝐶𝑀))
118	112, 117	fssresd 6071	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑑 ∈ 𝑅 ∧ 𝑤 ∈ 𝒫 (𝑆 ∖ {𝑋})) ∧ ((𝐺‘𝑑) ≤ (#‘𝑤) ∧ (𝑤𝐶(𝑀 − 1)) ⊆ (^◡𝐻 “ {𝑑})))) → (𝐾 ↾ (𝑤𝐶𝑀)):(𝑤𝐶𝑀)⟶𝑅)
119	1, 82, 83, 95, 108, 109, 111, 118	rami 15719	. . . . 5 ⊢ ((𝜑 ∧ ((𝑑 ∈ 𝑅 ∧ 𝑤 ∈ 𝒫 (𝑆 ∖ {𝑋})) ∧ ((𝐺‘𝑑) ≤ (#‘𝑤) ∧ (𝑤𝐶(𝑀 − 1)) ⊆ (^◡𝐻 “ {𝑑})))) → ∃𝑐 ∈ 𝑅 ∃𝑣 ∈ 𝒫 𝑤(((𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑑, ((𝐹‘𝑑) − 1), (𝐹‘𝑦)))‘𝑐) ≤ (#‘𝑣) ∧ (𝑣𝐶𝑀) ⊆ (^◡(𝐾 ↾ (𝑤𝐶𝑀)) “ {𝑐})))
120		equequ1 1952	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑐 → (𝑦 = 𝑑 ↔ 𝑐 = 𝑑))
121		fveq2 6191	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑐 → (𝐹‘𝑦) = (𝐹‘𝑐))
122	120, 121	ifbieq2d 4111	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑐 → if(𝑦 = 𝑑, ((𝐹‘𝑑) − 1), (𝐹‘𝑦)) = if(𝑐 = 𝑑, ((𝐹‘𝑑) − 1), (𝐹‘𝑐)))
123		ovex 6678	. . . . . . . . . . . . . 14 ⊢ ((𝐹‘𝑑) − 1) ∈ V
124		fvex 6201	. . . . . . . . . . . . . 14 ⊢ (𝐹‘𝑐) ∈ V
125	123, 124	ifex 4156	. . . . . . . . . . . . 13 ⊢ if(𝑐 = 𝑑, ((𝐹‘𝑑) − 1), (𝐹‘𝑐)) ∈ V
126	122, 94, 125	fvmpt 6282	. . . . . . . . . . . 12 ⊢ (𝑐 ∈ 𝑅 → ((𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑑, ((𝐹‘𝑑) − 1), (𝐹‘𝑦)))‘𝑐) = if(𝑐 = 𝑑, ((𝐹‘𝑑) − 1), (𝐹‘𝑐)))
127	126	ad2antrl 764	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ((𝑑 ∈ 𝑅 ∧ 𝑤 ∈ 𝒫 (𝑆 ∖ {𝑋})) ∧ ((𝐺‘𝑑) ≤ (#‘𝑤) ∧ (𝑤𝐶(𝑀 − 1)) ⊆ (^◡𝐻 “ {𝑑})))) ∧ (𝑐 ∈ 𝑅 ∧ 𝑣 ∈ 𝒫 𝑤)) → ((𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑑, ((𝐹‘𝑑) − 1), (𝐹‘𝑦)))‘𝑐) = if(𝑐 = 𝑑, ((𝐹‘𝑑) − 1), (𝐹‘𝑐)))
128	127	breq1d 4663	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ((𝑑 ∈ 𝑅 ∧ 𝑤 ∈ 𝒫 (𝑆 ∖ {𝑋})) ∧ ((𝐺‘𝑑) ≤ (#‘𝑤) ∧ (𝑤𝐶(𝑀 − 1)) ⊆ (^◡𝐻 “ {𝑑})))) ∧ (𝑐 ∈ 𝑅 ∧ 𝑣 ∈ 𝒫 𝑤)) → (((𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑑, ((𝐹‘𝑑) − 1), (𝐹‘𝑦)))‘𝑐) ≤ (#‘𝑣) ↔ if(𝑐 = 𝑑, ((𝐹‘𝑑) − 1), (𝐹‘𝑐)) ≤ (#‘𝑣)))
129	128	anbi1d 741	. . . . . . . . 9 ⊢ (((𝜑 ∧ ((𝑑 ∈ 𝑅 ∧ 𝑤 ∈ 𝒫 (𝑆 ∖ {𝑋})) ∧ ((𝐺‘𝑑) ≤ (#‘𝑤) ∧ (𝑤𝐶(𝑀 − 1)) ⊆ (^◡𝐻 “ {𝑑})))) ∧ (𝑐 ∈ 𝑅 ∧ 𝑣 ∈ 𝒫 𝑤)) → ((((𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑑, ((𝐹‘𝑑) − 1), (𝐹‘𝑦)))‘𝑐) ≤ (#‘𝑣) ∧ (𝑣𝐶𝑀) ⊆ (^◡(𝐾 ↾ (𝑤𝐶𝑀)) “ {𝑐})) ↔ (if(𝑐 = 𝑑, ((𝐹‘𝑑) − 1), (𝐹‘𝑐)) ≤ (#‘𝑣) ∧ (𝑣𝐶𝑀) ⊆ (^◡(𝐾 ↾ (𝑤𝐶𝑀)) “ {𝑐}))))
130	2	ad2antrr 762	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ((𝑑 ∈ 𝑅 ∧ 𝑤 ∈ 𝒫 (𝑆 ∖ {𝑋})) ∧ ((𝐺‘𝑑) ≤ (#‘𝑤) ∧ (𝑤𝐶(𝑀 − 1)) ⊆ (^◡𝐻 “ {𝑑})))) ∧ ((𝑐 ∈ 𝑅 ∧ 𝑣 ∈ 𝒫 𝑤) ∧ (if(𝑐 = 𝑑, ((𝐹‘𝑑) − 1), (𝐹‘𝑐)) ≤ (#‘𝑣) ∧ (𝑣𝐶𝑀) ⊆ (^◡(𝐾 ↾ (𝑤𝐶𝑀)) “ {𝑐})))) → 𝑀 ∈ ℕ)
131	5	ad2antrr 762	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ((𝑑 ∈ 𝑅 ∧ 𝑤 ∈ 𝒫 (𝑆 ∖ {𝑋})) ∧ ((𝐺‘𝑑) ≤ (#‘𝑤) ∧ (𝑤𝐶(𝑀 − 1)) ⊆ (^◡𝐻 “ {𝑑})))) ∧ ((𝑐 ∈ 𝑅 ∧ 𝑣 ∈ 𝒫 𝑤) ∧ (if(𝑐 = 𝑑, ((𝐹‘𝑑) − 1), (𝐹‘𝑐)) ≤ (#‘𝑣) ∧ (𝑣𝐶𝑀) ⊆ (^◡(𝐾 ↾ (𝑤𝐶𝑀)) “ {𝑐})))) → 𝑅 ∈ Fin)
132	84	ad2antrr 762	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ((𝑑 ∈ 𝑅 ∧ 𝑤 ∈ 𝒫 (𝑆 ∖ {𝑋})) ∧ ((𝐺‘𝑑) ≤ (#‘𝑤) ∧ (𝑤𝐶(𝑀 − 1)) ⊆ (^◡𝐻 “ {𝑑})))) ∧ ((𝑐 ∈ 𝑅 ∧ 𝑣 ∈ 𝒫 𝑤) ∧ (if(𝑐 = 𝑑, ((𝐹‘𝑑) − 1), (𝐹‘𝑐)) ≤ (#‘𝑣) ∧ (𝑣𝐶𝑀) ⊆ (^◡(𝐾 ↾ (𝑤𝐶𝑀)) “ {𝑐})))) → 𝐹:𝑅⟶ℕ)
133	6	ad2antrr 762	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ((𝑑 ∈ 𝑅 ∧ 𝑤 ∈ 𝒫 (𝑆 ∖ {𝑋})) ∧ ((𝐺‘𝑑) ≤ (#‘𝑤) ∧ (𝑤𝐶(𝑀 − 1)) ⊆ (^◡𝐻 “ {𝑑})))) ∧ ((𝑐 ∈ 𝑅 ∧ 𝑣 ∈ 𝒫 𝑤) ∧ (if(𝑐 = 𝑑, ((𝐹‘𝑑) − 1), (𝐹‘𝑐)) ≤ (#‘𝑣) ∧ (𝑣𝐶𝑀) ⊆ (^◡(𝐾 ↾ (𝑤𝐶𝑀)) “ {𝑐})))) → 𝐺:𝑅⟶ℕ₀)
134	7	ad2antrr 762	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ((𝑑 ∈ 𝑅 ∧ 𝑤 ∈ 𝒫 (𝑆 ∖ {𝑋})) ∧ ((𝐺‘𝑑) ≤ (#‘𝑤) ∧ (𝑤𝐶(𝑀 − 1)) ⊆ (^◡𝐻 “ {𝑑})))) ∧ ((𝑐 ∈ 𝑅 ∧ 𝑣 ∈ 𝒫 𝑤) ∧ (if(𝑐 = 𝑑, ((𝐹‘𝑑) − 1), (𝐹‘𝑐)) ≤ (#‘𝑣) ∧ (𝑣𝐶𝑀) ⊆ (^◡(𝐾 ↾ (𝑤𝐶𝑀)) “ {𝑐})))) → ((𝑀 − 1) Ramsey 𝐺) ∈ ℕ₀)
135	8	ad2antrr 762	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ((𝑑 ∈ 𝑅 ∧ 𝑤 ∈ 𝒫 (𝑆 ∖ {𝑋})) ∧ ((𝐺‘𝑑) ≤ (#‘𝑤) ∧ (𝑤𝐶(𝑀 − 1)) ⊆ (^◡𝐻 “ {𝑑})))) ∧ ((𝑐 ∈ 𝑅 ∧ 𝑣 ∈ 𝒫 𝑤) ∧ (if(𝑐 = 𝑑, ((𝐹‘𝑑) − 1), (𝐹‘𝑐)) ≤ (#‘𝑣) ∧ (𝑣𝐶𝑀) ⊆ (^◡(𝐾 ↾ (𝑤𝐶𝑀)) “ {𝑐})))) → 𝑆 ∈ Fin)
136	29	ad2antrr 762	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ((𝑑 ∈ 𝑅 ∧ 𝑤 ∈ 𝒫 (𝑆 ∖ {𝑋})) ∧ ((𝐺‘𝑑) ≤ (#‘𝑤) ∧ (𝑤𝐶(𝑀 − 1)) ⊆ (^◡𝐻 “ {𝑑})))) ∧ ((𝑐 ∈ 𝑅 ∧ 𝑣 ∈ 𝒫 𝑤) ∧ (if(𝑐 = 𝑑, ((𝐹‘𝑑) − 1), (𝐹‘𝑐)) ≤ (#‘𝑣) ∧ (𝑣𝐶𝑀) ⊆ (^◡(𝐾 ↾ (𝑤𝐶𝑀)) “ {𝑐})))) → (#‘𝑆) = (((𝑀 − 1) Ramsey 𝐺) + 1))
137	33	ad2antrr 762	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ((𝑑 ∈ 𝑅 ∧ 𝑤 ∈ 𝒫 (𝑆 ∖ {𝑋})) ∧ ((𝐺‘𝑑) ≤ (#‘𝑤) ∧ (𝑤𝐶(𝑀 − 1)) ⊆ (^◡𝐻 “ {𝑑})))) ∧ ((𝑐 ∈ 𝑅 ∧ 𝑣 ∈ 𝒫 𝑤) ∧ (if(𝑐 = 𝑑, ((𝐹‘𝑑) − 1), (𝐹‘𝑐)) ≤ (#‘𝑣) ∧ (𝑣𝐶𝑀) ⊆ (^◡(𝐾 ↾ (𝑤𝐶𝑀)) “ {𝑐})))) → 𝐾:(𝑆𝐶𝑀)⟶𝑅)
138	19	ad2antrr 762	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ((𝑑 ∈ 𝑅 ∧ 𝑤 ∈ 𝒫 (𝑆 ∖ {𝑋})) ∧ ((𝐺‘𝑑) ≤ (#‘𝑤) ∧ (𝑤𝐶(𝑀 − 1)) ⊆ (^◡𝐻 “ {𝑑})))) ∧ ((𝑐 ∈ 𝑅 ∧ 𝑣 ∈ 𝒫 𝑤) ∧ (if(𝑐 = 𝑑, ((𝐹‘𝑑) − 1), (𝐹‘𝑐)) ≤ (#‘𝑣) ∧ (𝑣𝐶𝑀) ⊆ (^◡(𝐾 ↾ (𝑤𝐶𝑀)) “ {𝑐})))) → 𝑋 ∈ 𝑆)
139	86	adantr 481	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ((𝑑 ∈ 𝑅 ∧ 𝑤 ∈ 𝒫 (𝑆 ∖ {𝑋})) ∧ ((𝐺‘𝑑) ≤ (#‘𝑤) ∧ (𝑤𝐶(𝑀 − 1)) ⊆ (^◡𝐻 “ {𝑑})))) ∧ ((𝑐 ∈ 𝑅 ∧ 𝑣 ∈ 𝒫 𝑤) ∧ (if(𝑐 = 𝑑, ((𝐹‘𝑑) − 1), (𝐹‘𝑐)) ≤ (#‘𝑣) ∧ (𝑣𝐶𝑀) ⊆ (^◡(𝐾 ↾ (𝑤𝐶𝑀)) “ {𝑐})))) → 𝑑 ∈ 𝑅)
140	114	adantr 481	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ((𝑑 ∈ 𝑅 ∧ 𝑤 ∈ 𝒫 (𝑆 ∖ {𝑋})) ∧ ((𝐺‘𝑑) ≤ (#‘𝑤) ∧ (𝑤𝐶(𝑀 − 1)) ⊆ (^◡𝐻 “ {𝑑})))) ∧ ((𝑐 ∈ 𝑅 ∧ 𝑣 ∈ 𝒫 𝑤) ∧ (if(𝑐 = 𝑑, ((𝐹‘𝑑) − 1), (𝐹‘𝑐)) ≤ (#‘𝑣) ∧ (𝑣𝐶𝑀) ⊆ (^◡(𝐾 ↾ (𝑤𝐶𝑀)) “ {𝑐})))) → 𝑤 ⊆ (𝑆 ∖ {𝑋}))
141	110	adantr 481	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ((𝑑 ∈ 𝑅 ∧ 𝑤 ∈ 𝒫 (𝑆 ∖ {𝑋})) ∧ ((𝐺‘𝑑) ≤ (#‘𝑤) ∧ (𝑤𝐶(𝑀 − 1)) ⊆ (^◡𝐻 “ {𝑑})))) ∧ ((𝑐 ∈ 𝑅 ∧ 𝑣 ∈ 𝒫 𝑤) ∧ (if(𝑐 = 𝑑, ((𝐹‘𝑑) − 1), (𝐹‘𝑐)) ≤ (#‘𝑣) ∧ (𝑣𝐶𝑀) ⊆ (^◡(𝐾 ↾ (𝑤𝐶𝑀)) “ {𝑐})))) → (𝐺‘𝑑) ≤ (#‘𝑤))
142		simprrr 805	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑑 ∈ 𝑅 ∧ 𝑤 ∈ 𝒫 (𝑆 ∖ {𝑋})) ∧ ((𝐺‘𝑑) ≤ (#‘𝑤) ∧ (𝑤𝐶(𝑀 − 1)) ⊆ (^◡𝐻 “ {𝑑})))) → (𝑤𝐶(𝑀 − 1)) ⊆ (^◡𝐻 “ {𝑑}))
143	142	adantr 481	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ((𝑑 ∈ 𝑅 ∧ 𝑤 ∈ 𝒫 (𝑆 ∖ {𝑋})) ∧ ((𝐺‘𝑑) ≤ (#‘𝑤) ∧ (𝑤𝐶(𝑀 − 1)) ⊆ (^◡𝐻 “ {𝑑})))) ∧ ((𝑐 ∈ 𝑅 ∧ 𝑣 ∈ 𝒫 𝑤) ∧ (if(𝑐 = 𝑑, ((𝐹‘𝑑) − 1), (𝐹‘𝑐)) ≤ (#‘𝑣) ∧ (𝑣𝐶𝑀) ⊆ (^◡(𝐾 ↾ (𝑤𝐶𝑀)) “ {𝑐})))) → (𝑤𝐶(𝑀 − 1)) ⊆ (^◡𝐻 “ {𝑑}))
144		simprll 802	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ((𝑑 ∈ 𝑅 ∧ 𝑤 ∈ 𝒫 (𝑆 ∖ {𝑋})) ∧ ((𝐺‘𝑑) ≤ (#‘𝑤) ∧ (𝑤𝐶(𝑀 − 1)) ⊆ (^◡𝐻 “ {𝑑})))) ∧ ((𝑐 ∈ 𝑅 ∧ 𝑣 ∈ 𝒫 𝑤) ∧ (if(𝑐 = 𝑑, ((𝐹‘𝑑) − 1), (𝐹‘𝑐)) ≤ (#‘𝑣) ∧ (𝑣𝐶𝑀) ⊆ (^◡(𝐾 ↾ (𝑤𝐶𝑀)) “ {𝑐})))) → 𝑐 ∈ 𝑅)
145		simprlr 803	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ((𝑑 ∈ 𝑅 ∧ 𝑤 ∈ 𝒫 (𝑆 ∖ {𝑋})) ∧ ((𝐺‘𝑑) ≤ (#‘𝑤) ∧ (𝑤𝐶(𝑀 − 1)) ⊆ (^◡𝐻 “ {𝑑})))) ∧ ((𝑐 ∈ 𝑅 ∧ 𝑣 ∈ 𝒫 𝑤) ∧ (if(𝑐 = 𝑑, ((𝐹‘𝑑) − 1), (𝐹‘𝑐)) ≤ (#‘𝑣) ∧ (𝑣𝐶𝑀) ⊆ (^◡(𝐾 ↾ (𝑤𝐶𝑀)) “ {𝑐})))) → 𝑣 ∈ 𝒫 𝑤)
146	145	elpwid 4170	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ((𝑑 ∈ 𝑅 ∧ 𝑤 ∈ 𝒫 (𝑆 ∖ {𝑋})) ∧ ((𝐺‘𝑑) ≤ (#‘𝑤) ∧ (𝑤𝐶(𝑀 − 1)) ⊆ (^◡𝐻 “ {𝑑})))) ∧ ((𝑐 ∈ 𝑅 ∧ 𝑣 ∈ 𝒫 𝑤) ∧ (if(𝑐 = 𝑑, ((𝐹‘𝑑) − 1), (𝐹‘𝑐)) ≤ (#‘𝑣) ∧ (𝑣𝐶𝑀) ⊆ (^◡(𝐾 ↾ (𝑤𝐶𝑀)) “ {𝑐})))) → 𝑣 ⊆ 𝑤)
147		simprrl 804	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ((𝑑 ∈ 𝑅 ∧ 𝑤 ∈ 𝒫 (𝑆 ∖ {𝑋})) ∧ ((𝐺‘𝑑) ≤ (#‘𝑤) ∧ (𝑤𝐶(𝑀 − 1)) ⊆ (^◡𝐻 “ {𝑑})))) ∧ ((𝑐 ∈ 𝑅 ∧ 𝑣 ∈ 𝒫 𝑤) ∧ (if(𝑐 = 𝑑, ((𝐹‘𝑑) − 1), (𝐹‘𝑐)) ≤ (#‘𝑣) ∧ (𝑣𝐶𝑀) ⊆ (^◡(𝐾 ↾ (𝑤𝐶𝑀)) “ {𝑐})))) → if(𝑐 = 𝑑, ((𝐹‘𝑑) − 1), (𝐹‘𝑐)) ≤ (#‘𝑣))
148		simprrr 805	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ((𝑑 ∈ 𝑅 ∧ 𝑤 ∈ 𝒫 (𝑆 ∖ {𝑋})) ∧ ((𝐺‘𝑑) ≤ (#‘𝑤) ∧ (𝑤𝐶(𝑀 − 1)) ⊆ (^◡𝐻 “ {𝑑})))) ∧ ((𝑐 ∈ 𝑅 ∧ 𝑣 ∈ 𝒫 𝑤) ∧ (if(𝑐 = 𝑑, ((𝐹‘𝑑) − 1), (𝐹‘𝑐)) ≤ (#‘𝑣) ∧ (𝑣𝐶𝑀) ⊆ (^◡(𝐾 ↾ (𝑤𝐶𝑀)) “ {𝑐})))) → (𝑣𝐶𝑀) ⊆ (^◡(𝐾 ↾ (𝑤𝐶𝑀)) “ {𝑐}))
149		cnvresima 5623	. . . . . . . . . . . . 13 ⊢ (^◡(𝐾 ↾ (𝑤𝐶𝑀)) “ {𝑐}) = ((^◡𝐾 “ {𝑐}) ∩ (𝑤𝐶𝑀))
150		inss1 3833	. . . . . . . . . . . . 13 ⊢ ((^◡𝐾 “ {𝑐}) ∩ (𝑤𝐶𝑀)) ⊆ (^◡𝐾 “ {𝑐})
151	149, 150	eqsstri 3635	. . . . . . . . . . . 12 ⊢ (^◡(𝐾 ↾ (𝑤𝐶𝑀)) “ {𝑐}) ⊆ (^◡𝐾 “ {𝑐})
152	148, 151	syl6ss 3615	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ((𝑑 ∈ 𝑅 ∧ 𝑤 ∈ 𝒫 (𝑆 ∖ {𝑋})) ∧ ((𝐺‘𝑑) ≤ (#‘𝑤) ∧ (𝑤𝐶(𝑀 − 1)) ⊆ (^◡𝐻 “ {𝑑})))) ∧ ((𝑐 ∈ 𝑅 ∧ 𝑣 ∈ 𝒫 𝑤) ∧ (if(𝑐 = 𝑑, ((𝐹‘𝑑) − 1), (𝐹‘𝑐)) ≤ (#‘𝑣) ∧ (𝑣𝐶𝑀) ⊆ (^◡(𝐾 ↾ (𝑤𝐶𝑀)) “ {𝑐})))) → (𝑣𝐶𝑀) ⊆ (^◡𝐾 “ {𝑐}))
153	130, 131, 132, 102, 133, 134, 1, 135, 136, 137, 138, 79, 139, 140, 141, 143, 144, 146, 147, 152	ramub1lem1 15730	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ((𝑑 ∈ 𝑅 ∧ 𝑤 ∈ 𝒫 (𝑆 ∖ {𝑋})) ∧ ((𝐺‘𝑑) ≤ (#‘𝑤) ∧ (𝑤𝐶(𝑀 − 1)) ⊆ (^◡𝐻 “ {𝑑})))) ∧ ((𝑐 ∈ 𝑅 ∧ 𝑣 ∈ 𝒫 𝑤) ∧ (if(𝑐 = 𝑑, ((𝐹‘𝑑) − 1), (𝐹‘𝑐)) ≤ (#‘𝑣) ∧ (𝑣𝐶𝑀) ⊆ (^◡(𝐾 ↾ (𝑤𝐶𝑀)) “ {𝑐})))) → ∃𝑧 ∈ 𝒫 𝑆((𝐹‘𝑐) ≤ (#‘𝑧) ∧ (𝑧𝐶𝑀) ⊆ (^◡𝐾 “ {𝑐})))
154	153	expr 643	. . . . . . . . 9 ⊢ (((𝜑 ∧ ((𝑑 ∈ 𝑅 ∧ 𝑤 ∈ 𝒫 (𝑆 ∖ {𝑋})) ∧ ((𝐺‘𝑑) ≤ (#‘𝑤) ∧ (𝑤𝐶(𝑀 − 1)) ⊆ (^◡𝐻 “ {𝑑})))) ∧ (𝑐 ∈ 𝑅 ∧ 𝑣 ∈ 𝒫 𝑤)) → ((if(𝑐 = 𝑑, ((𝐹‘𝑑) − 1), (𝐹‘𝑐)) ≤ (#‘𝑣) ∧ (𝑣𝐶𝑀) ⊆ (^◡(𝐾 ↾ (𝑤𝐶𝑀)) “ {𝑐})) → ∃𝑧 ∈ 𝒫 𝑆((𝐹‘𝑐) ≤ (#‘𝑧) ∧ (𝑧𝐶𝑀) ⊆ (^◡𝐾 “ {𝑐}))))
155	129, 154	sylbid 230	. . . . . . . 8 ⊢ (((𝜑 ∧ ((𝑑 ∈ 𝑅 ∧ 𝑤 ∈ 𝒫 (𝑆 ∖ {𝑋})) ∧ ((𝐺‘𝑑) ≤ (#‘𝑤) ∧ (𝑤𝐶(𝑀 − 1)) ⊆ (^◡𝐻 “ {𝑑})))) ∧ (𝑐 ∈ 𝑅 ∧ 𝑣 ∈ 𝒫 𝑤)) → ((((𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑑, ((𝐹‘𝑑) − 1), (𝐹‘𝑦)))‘𝑐) ≤ (#‘𝑣) ∧ (𝑣𝐶𝑀) ⊆ (^◡(𝐾 ↾ (𝑤𝐶𝑀)) “ {𝑐})) → ∃𝑧 ∈ 𝒫 𝑆((𝐹‘𝑐) ≤ (#‘𝑧) ∧ (𝑧𝐶𝑀) ⊆ (^◡𝐾 “ {𝑐}))))
156	155	anassrs 680	. . . . . . 7 ⊢ ((((𝜑 ∧ ((𝑑 ∈ 𝑅 ∧ 𝑤 ∈ 𝒫 (𝑆 ∖ {𝑋})) ∧ ((𝐺‘𝑑) ≤ (#‘𝑤) ∧ (𝑤𝐶(𝑀 − 1)) ⊆ (^◡𝐻 “ {𝑑})))) ∧ 𝑐 ∈ 𝑅) ∧ 𝑣 ∈ 𝒫 𝑤) → ((((𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑑, ((𝐹‘𝑑) − 1), (𝐹‘𝑦)))‘𝑐) ≤ (#‘𝑣) ∧ (𝑣𝐶𝑀) ⊆ (^◡(𝐾 ↾ (𝑤𝐶𝑀)) “ {𝑐})) → ∃𝑧 ∈ 𝒫 𝑆((𝐹‘𝑐) ≤ (#‘𝑧) ∧ (𝑧𝐶𝑀) ⊆ (^◡𝐾 “ {𝑐}))))
157	156	rexlimdva 3031	. . . . . 6 ⊢ (((𝜑 ∧ ((𝑑 ∈ 𝑅 ∧ 𝑤 ∈ 𝒫 (𝑆 ∖ {𝑋})) ∧ ((𝐺‘𝑑) ≤ (#‘𝑤) ∧ (𝑤𝐶(𝑀 − 1)) ⊆ (^◡𝐻 “ {𝑑})))) ∧ 𝑐 ∈ 𝑅) → (∃𝑣 ∈ 𝒫 𝑤(((𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑑, ((𝐹‘𝑑) − 1), (𝐹‘𝑦)))‘𝑐) ≤ (#‘𝑣) ∧ (𝑣𝐶𝑀) ⊆ (^◡(𝐾 ↾ (𝑤𝐶𝑀)) “ {𝑐})) → ∃𝑧 ∈ 𝒫 𝑆((𝐹‘𝑐) ≤ (#‘𝑧) ∧ (𝑧𝐶𝑀) ⊆ (^◡𝐾 “ {𝑐}))))
158	157	reximdva 3017	. . . . 5 ⊢ ((𝜑 ∧ ((𝑑 ∈ 𝑅 ∧ 𝑤 ∈ 𝒫 (𝑆 ∖ {𝑋})) ∧ ((𝐺‘𝑑) ≤ (#‘𝑤) ∧ (𝑤𝐶(𝑀 − 1)) ⊆ (^◡𝐻 “ {𝑑})))) → (∃𝑐 ∈ 𝑅 ∃𝑣 ∈ 𝒫 𝑤(((𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑑, ((𝐹‘𝑑) − 1), (𝐹‘𝑦)))‘𝑐) ≤ (#‘𝑣) ∧ (𝑣𝐶𝑀) ⊆ (^◡(𝐾 ↾ (𝑤𝐶𝑀)) “ {𝑐})) → ∃𝑐 ∈ 𝑅 ∃𝑧 ∈ 𝒫 𝑆((𝐹‘𝑐) ≤ (#‘𝑧) ∧ (𝑧𝐶𝑀) ⊆ (^◡𝐾 “ {𝑐}))))
159	119, 158	mpd 15	. . . 4 ⊢ ((𝜑 ∧ ((𝑑 ∈ 𝑅 ∧ 𝑤 ∈ 𝒫 (𝑆 ∖ {𝑋})) ∧ ((𝐺‘𝑑) ≤ (#‘𝑤) ∧ (𝑤𝐶(𝑀 − 1)) ⊆ (^◡𝐻 “ {𝑑})))) → ∃𝑐 ∈ 𝑅 ∃𝑧 ∈ 𝒫 𝑆((𝐹‘𝑐) ≤ (#‘𝑧) ∧ (𝑧𝐶𝑀) ⊆ (^◡𝐾 “ {𝑐})))
160	159	expr 643	. . 3 ⊢ ((𝜑 ∧ (𝑑 ∈ 𝑅 ∧ 𝑤 ∈ 𝒫 (𝑆 ∖ {𝑋}))) → (((𝐺‘𝑑) ≤ (#‘𝑤) ∧ (𝑤𝐶(𝑀 − 1)) ⊆ (^◡𝐻 “ {𝑑})) → ∃𝑐 ∈ 𝑅 ∃𝑧 ∈ 𝒫 𝑆((𝐹‘𝑐) ≤ (#‘𝑧) ∧ (𝑧𝐶𝑀) ⊆ (^◡𝐾 “ {𝑐}))))
161	160	rexlimdvva 3038	. 2 ⊢ (𝜑 → (∃𝑑 ∈ 𝑅 ∃𝑤 ∈ 𝒫 (𝑆 ∖ {𝑋})((𝐺‘𝑑) ≤ (#‘𝑤) ∧ (𝑤𝐶(𝑀 − 1)) ⊆ (^◡𝐻 “ {𝑑})) → ∃𝑐 ∈ 𝑅 ∃𝑧 ∈ 𝒫 𝑆((𝐹‘𝑐) ≤ (#‘𝑧) ∧ (𝑧𝐶𝑀) ⊆ (^◡𝐾 “ {𝑐}))))
162	81, 161	mpd 15	1 ⊢ (𝜑 → ∃𝑐 ∈ 𝑅 ∃𝑧 ∈ 𝒫 𝑆((𝐹‘𝑐) ≤ (#‘𝑧) ∧ (𝑧𝐶𝑀) ⊆ (^◡𝐾 “ {𝑐})))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 384 = wceq 1483 ∈ wcel 1990 ∃wrex 2913 {crab 2916 Vcvv 3200 ∖ cdif 3571 ∪ cun 3572 ∩ cin 3573 ⊆ wss 3574 ifcif 4086 𝒫 cpw 4158 {csn 4177 class class class wbr 4653 ↦ cmpt 4729 ^◡ccnv 5113 ↾ cres 5116 “ cima 5117 ⟶wf 5884 ‘cfv 5888 (class class class)co 6650 ↦ cmpt2 6652 Fincfn 7955 ℂcc 9934 1c1 9937 + caddc 9939 ≤ cle 10075 − cmin 10266 ℕcn 11020 ℕ₀cn0 11292 #chash 13117 Ramsey cram 15703

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-oadd 7564 df-er 7742 df-map 7859 df-en 7956 df-dom 7957 df-sdom 7958 df-fin 7959 df-sup 8348 df-inf 8349 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-nn 11021 df-n0 11293 df-z 11378 df-uz 11688 df-fz 12327 df-hash 13118 df-ram 15705

This theorem is referenced by: ramub1 15732

W3C validator