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

Theorem ramub1lem1 15937
 Description: Lemma for ramub1 15939. (Contributed by Mario Carneiro, 23-Apr-2015.)
Hypotheses
Ref Expression
ramub1.m (𝜑𝑀 ∈ ℕ)
ramub1.r (𝜑𝑅 ∈ Fin)
ramub1.f (𝜑𝐹:𝑅⟶ℕ)
ramub1.g 𝐺 = (𝑥𝑅 ↦ (𝑀 Ramsey (𝑦𝑅 ↦ if(𝑦 = 𝑥, ((𝐹𝑥) − 1), (𝐹𝑦)))))
ramub1.1 (𝜑𝐺:𝑅⟶ℕ0)
ramub1.2 (𝜑 → ((𝑀 − 1) Ramsey 𝐺) ∈ ℕ0)
ramub1.3 𝐶 = (𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (♯‘𝑏) = 𝑖})
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
StepHypRef Expression
1 ramub1.v . . . . . . . 8 (𝜑𝑉𝑊)
2 ramub1.w . . . . . . . 8 (𝜑𝑊 ⊆ (𝑆 ∖ {𝑋}))
31, 2sstrd 3762 . . . . . . 7 (𝜑𝑉 ⊆ (𝑆 ∖ {𝑋}))
43difss2d 3891 . . . . . 6 (𝜑𝑉𝑆)
5 ramub1.x . . . . . . 7 (𝜑𝑋𝑆)
65snssd 4475 . . . . . 6 (𝜑 → {𝑋} ⊆ 𝑆)
74, 6unssd 3940 . . . . 5 (𝜑 → (𝑉 ∪ {𝑋}) ⊆ 𝑆)
8 ramub1.4 . . . . . 6 (𝜑𝑆 ∈ Fin)
9 elpw2g 4958 . . . . . 6 (𝑆 ∈ Fin → ((𝑉 ∪ {𝑋}) ∈ 𝒫 𝑆 ↔ (𝑉 ∪ {𝑋}) ⊆ 𝑆))
108, 9syl 17 . . . . 5 (𝜑 → ((𝑉 ∪ {𝑋}) ∈ 𝒫 𝑆 ↔ (𝑉 ∪ {𝑋}) ⊆ 𝑆))
117, 10mpbird 247 . . . 4 (𝜑 → (𝑉 ∪ {𝑋}) ∈ 𝒫 𝑆)
1211adantr 466 . . 3 ((𝜑𝐸 = 𝐷) → (𝑉 ∪ {𝑋}) ∈ 𝒫 𝑆)
13 iftrue 4231 . . . . . . 7 (𝐸 = 𝐷 → if(𝐸 = 𝐷, ((𝐹𝐷) − 1), (𝐹𝐸)) = ((𝐹𝐷) − 1))
1413adantl 467 . . . . . 6 ((𝜑𝐸 = 𝐷) → if(𝐸 = 𝐷, ((𝐹𝐷) − 1), (𝐹𝐸)) = ((𝐹𝐷) − 1))
15 ramub1.9 . . . . . . 7 (𝜑 → if(𝐸 = 𝐷, ((𝐹𝐷) − 1), (𝐹𝐸)) ≤ (♯‘𝑉))
1615adantr 466 . . . . . 6 ((𝜑𝐸 = 𝐷) → if(𝐸 = 𝐷, ((𝐹𝐷) − 1), (𝐹𝐸)) ≤ (♯‘𝑉))
1714, 16eqbrtrrd 4810 . . . . 5 ((𝜑𝐸 = 𝐷) → ((𝐹𝐷) − 1) ≤ (♯‘𝑉))
18 ramub1.f . . . . . . . . 9 (𝜑𝐹:𝑅⟶ℕ)
19 ramub1.d . . . . . . . . 9 (𝜑𝐷𝑅)
2018, 19ffvelrnd 6503 . . . . . . . 8 (𝜑 → (𝐹𝐷) ∈ ℕ)
2120adantr 466 . . . . . . 7 ((𝜑𝐸 = 𝐷) → (𝐹𝐷) ∈ ℕ)
2221nnred 11237 . . . . . 6 ((𝜑𝐸 = 𝐷) → (𝐹𝐷) ∈ ℝ)
23 1red 10257 . . . . . 6 ((𝜑𝐸 = 𝐷) → 1 ∈ ℝ)
24 ssfi 8336 . . . . . . . . 9 ((𝑆 ∈ Fin ∧ 𝑉𝑆) → 𝑉 ∈ Fin)
258, 4, 24syl2anc 573 . . . . . . . 8 (𝜑𝑉 ∈ Fin)
26 hashcl 13349 . . . . . . . 8 (𝑉 ∈ Fin → (♯‘𝑉) ∈ ℕ0)
27 nn0re 11503 . . . . . . . 8 ((♯‘𝑉) ∈ ℕ0 → (♯‘𝑉) ∈ ℝ)
2825, 26, 273syl 18 . . . . . . 7 (𝜑 → (♯‘𝑉) ∈ ℝ)
2928adantr 466 . . . . . 6 ((𝜑𝐸 = 𝐷) → (♯‘𝑉) ∈ ℝ)
3022, 23, 29lesubaddd 10826 . . . . 5 ((𝜑𝐸 = 𝐷) → (((𝐹𝐷) − 1) ≤ (♯‘𝑉) ↔ (𝐹𝐷) ≤ ((♯‘𝑉) + 1)))
3117, 30mpbid 222 . . . 4 ((𝜑𝐸 = 𝐷) → (𝐹𝐷) ≤ ((♯‘𝑉) + 1))
32 fveq2 6332 . . . . 5 (𝐸 = 𝐷 → (𝐹𝐸) = (𝐹𝐷))
33 snidg 4345 . . . . . . . 8 (𝑋𝑆𝑋 ∈ {𝑋})
345, 33syl 17 . . . . . . 7 (𝜑𝑋 ∈ {𝑋})
353sseld 3751 . . . . . . . 8 (𝜑 → (𝑋𝑉𝑋 ∈ (𝑆 ∖ {𝑋})))
36 eldifn 3884 . . . . . . . 8 (𝑋 ∈ (𝑆 ∖ {𝑋}) → ¬ 𝑋 ∈ {𝑋})
3735, 36syl6 35 . . . . . . 7 (𝜑 → (𝑋𝑉 → ¬ 𝑋 ∈ {𝑋}))
3834, 37mt2d 133 . . . . . 6 (𝜑 → ¬ 𝑋𝑉)
39 hashunsng 13383 . . . . . . 7 (𝑋𝑆 → ((𝑉 ∈ Fin ∧ ¬ 𝑋𝑉) → (♯‘(𝑉 ∪ {𝑋})) = ((♯‘𝑉) + 1)))
405, 39syl 17 . . . . . 6 (𝜑 → ((𝑉 ∈ Fin ∧ ¬ 𝑋𝑉) → (♯‘(𝑉 ∪ {𝑋})) = ((♯‘𝑉) + 1)))
4125, 38, 40mp2and 679 . . . . 5 (𝜑 → (♯‘(𝑉 ∪ {𝑋})) = ((♯‘𝑉) + 1))
4232, 41breqan12rd 4803 . . . 4 ((𝜑𝐸 = 𝐷) → ((𝐹𝐸) ≤ (♯‘(𝑉 ∪ {𝑋})) ↔ (𝐹𝐷) ≤ ((♯‘𝑉) + 1)))
4331, 42mpbird 247 . . 3 ((𝜑𝐸 = 𝐷) → (𝐹𝐸) ≤ (♯‘(𝑉 ∪ {𝑋})))
44 snfi 8194 . . . . . . 7 {𝑋} ∈ Fin
45 unfi 8383 . . . . . . 7 ((𝑉 ∈ Fin ∧ {𝑋} ∈ Fin) → (𝑉 ∪ {𝑋}) ∈ Fin)
4625, 44, 45sylancl 574 . . . . . 6 (𝜑 → (𝑉 ∪ {𝑋}) ∈ Fin)
47 ramub1.m . . . . . . 7 (𝜑𝑀 ∈ ℕ)
4847nnnn0d 11553 . . . . . 6 (𝜑𝑀 ∈ ℕ0)
49 ramub1.3 . . . . . . 7 𝐶 = (𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (♯‘𝑏) = 𝑖})
5049hashbcval 15913 . . . . . 6 (((𝑉 ∪ {𝑋}) ∈ Fin ∧ 𝑀 ∈ ℕ0) → ((𝑉 ∪ {𝑋})𝐶𝑀) = {𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∣ (♯‘𝑥) = 𝑀})
5146, 48, 50syl2anc 573 . . . . 5 (𝜑 → ((𝑉 ∪ {𝑋})𝐶𝑀) = {𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∣ (♯‘𝑥) = 𝑀})
5251adantr 466 . . . 4 ((𝜑𝐸 = 𝐷) → ((𝑉 ∪ {𝑋})𝐶𝑀) = {𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∣ (♯‘𝑥) = 𝑀})
53 simpl1l 1278 . . . . . . . 8 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (♯‘𝑥) = 𝑀) ∧ 𝑥 ∈ 𝒫 𝑉) → 𝜑)
5449hashbcval 15913 . . . . . . . . . 10 ((𝑉 ∈ Fin ∧ 𝑀 ∈ ℕ0) → (𝑉𝐶𝑀) = {𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 𝑀})
5525, 48, 54syl2anc 573 . . . . . . . . 9 (𝜑 → (𝑉𝐶𝑀) = {𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 𝑀})
56 ramub1.s . . . . . . . . 9 (𝜑 → (𝑉𝐶𝑀) ⊆ (𝐾 “ {𝐸}))
5755, 56eqsstr3d 3789 . . . . . . . 8 (𝜑 → {𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 𝑀} ⊆ (𝐾 “ {𝐸}))
5853, 57syl 17 . . . . . . 7 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (♯‘𝑥) = 𝑀) ∧ 𝑥 ∈ 𝒫 𝑉) → {𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 𝑀} ⊆ (𝐾 “ {𝐸}))
59 simpr 471 . . . . . . . 8 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (♯‘𝑥) = 𝑀) ∧ 𝑥 ∈ 𝒫 𝑉) → 𝑥 ∈ 𝒫 𝑉)
60 simpl3 1231 . . . . . . . 8 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (♯‘𝑥) = 𝑀) ∧ 𝑥 ∈ 𝒫 𝑉) → (♯‘𝑥) = 𝑀)
61 rabid 3264 . . . . . . . 8 (𝑥 ∈ {𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 𝑀} ↔ (𝑥 ∈ 𝒫 𝑉 ∧ (♯‘𝑥) = 𝑀))
6259, 60, 61sylanbrc 572 . . . . . . 7 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (♯‘𝑥) = 𝑀) ∧ 𝑥 ∈ 𝒫 𝑉) → 𝑥 ∈ {𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 𝑀})
6358, 62sseldd 3753 . . . . . 6 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (♯‘𝑥) = 𝑀) ∧ 𝑥 ∈ 𝒫 𝑉) → 𝑥 ∈ (𝐾 “ {𝐸}))
64 simpl2 1229 . . . . . . . . . . . 12 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (♯‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}))
6564elpwid 4309 . . . . . . . . . . 11 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (♯‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → 𝑥 ⊆ (𝑉 ∪ {𝑋}))
66 simpl1l 1278 . . . . . . . . . . . 12 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (♯‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → 𝜑)
6766, 7syl 17 . . . . . . . . . . 11 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (♯‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → (𝑉 ∪ {𝑋}) ⊆ 𝑆)
6865, 67sstrd 3762 . . . . . . . . . 10 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (♯‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → 𝑥𝑆)
69 vex 3354 . . . . . . . . . . 11 𝑥 ∈ V
7069elpw 4303 . . . . . . . . . 10 (𝑥 ∈ 𝒫 𝑆𝑥𝑆)
7168, 70sylibr 224 . . . . . . . . 9 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (♯‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → 𝑥 ∈ 𝒫 𝑆)
72 simpl3 1231 . . . . . . . . 9 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (♯‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → (♯‘𝑥) = 𝑀)
73 rabid 3264 . . . . . . . . 9 (𝑥 ∈ {𝑥 ∈ 𝒫 𝑆 ∣ (♯‘𝑥) = 𝑀} ↔ (𝑥 ∈ 𝒫 𝑆 ∧ (♯‘𝑥) = 𝑀))
7471, 72, 73sylanbrc 572 . . . . . . . 8 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (♯‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → 𝑥 ∈ {𝑥 ∈ 𝒫 𝑆 ∣ (♯‘𝑥) = 𝑀})
7549hashbcval 15913 . . . . . . . . . 10 ((𝑆 ∈ Fin ∧ 𝑀 ∈ ℕ0) → (𝑆𝐶𝑀) = {𝑥 ∈ 𝒫 𝑆 ∣ (♯‘𝑥) = 𝑀})
768, 48, 75syl2anc 573 . . . . . . . . 9 (𝜑 → (𝑆𝐶𝑀) = {𝑥 ∈ 𝒫 𝑆 ∣ (♯‘𝑥) = 𝑀})
7766, 76syl 17 . . . . . . . 8 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (♯‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → (𝑆𝐶𝑀) = {𝑥 ∈ 𝒫 𝑆 ∣ (♯‘𝑥) = 𝑀})
7874, 77eleqtrrd 2853 . . . . . . 7 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (♯‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → 𝑥 ∈ (𝑆𝐶𝑀))
792difss2d 3891 . . . . . . . . . . . . . . 15 (𝜑𝑊𝑆)
80 ssfi 8336 . . . . . . . . . . . . . . 15 ((𝑆 ∈ Fin ∧ 𝑊𝑆) → 𝑊 ∈ Fin)
818, 79, 80syl2anc 573 . . . . . . . . . . . . . 14 (𝜑𝑊 ∈ Fin)
82 nnm1nn0 11536 . . . . . . . . . . . . . . 15 (𝑀 ∈ ℕ → (𝑀 − 1) ∈ ℕ0)
8347, 82syl 17 . . . . . . . . . . . . . 14 (𝜑 → (𝑀 − 1) ∈ ℕ0)
8449hashbcval 15913 . . . . . . . . . . . . . 14 ((𝑊 ∈ Fin ∧ (𝑀 − 1) ∈ ℕ0) → (𝑊𝐶(𝑀 − 1)) = {𝑢 ∈ 𝒫 𝑊 ∣ (♯‘𝑢) = (𝑀 − 1)})
8581, 83, 84syl2anc 573 . . . . . . . . . . . . 13 (𝜑 → (𝑊𝐶(𝑀 − 1)) = {𝑢 ∈ 𝒫 𝑊 ∣ (♯‘𝑢) = (𝑀 − 1)})
86 ramub1.8 . . . . . . . . . . . . 13 (𝜑 → (𝑊𝐶(𝑀 − 1)) ⊆ (𝐻 “ {𝐷}))
8785, 86eqsstr3d 3789 . . . . . . . . . . . 12 (𝜑 → {𝑢 ∈ 𝒫 𝑊 ∣ (♯‘𝑢) = (𝑀 − 1)} ⊆ (𝐻 “ {𝐷}))
8866, 87syl 17 . . . . . . . . . . 11 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (♯‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → {𝑢 ∈ 𝒫 𝑊 ∣ (♯‘𝑢) = (𝑀 − 1)} ⊆ (𝐻 “ {𝐷}))
89 uncom 3908 . . . . . . . . . . . . . . . 16 (𝑉 ∪ {𝑋}) = ({𝑋} ∪ 𝑉)
9065, 89syl6sseq 3800 . . . . . . . . . . . . . . 15 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (♯‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → 𝑥 ⊆ ({𝑋} ∪ 𝑉))
91 ssundif 4194 . . . . . . . . . . . . . . 15 (𝑥 ⊆ ({𝑋} ∪ 𝑉) ↔ (𝑥 ∖ {𝑋}) ⊆ 𝑉)
9290, 91sylib 208 . . . . . . . . . . . . . 14 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (♯‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → (𝑥 ∖ {𝑋}) ⊆ 𝑉)
9366, 1syl 17 . . . . . . . . . . . . . 14 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (♯‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → 𝑉𝑊)
9492, 93sstrd 3762 . . . . . . . . . . . . 13 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (♯‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → (𝑥 ∖ {𝑋}) ⊆ 𝑊)
95 difexg 4942 . . . . . . . . . . . . . . 15 (𝑥 ∈ V → (𝑥 ∖ {𝑋}) ∈ V)
9669, 95ax-mp 5 . . . . . . . . . . . . . 14 (𝑥 ∖ {𝑋}) ∈ V
9796elpw 4303 . . . . . . . . . . . . 13 ((𝑥 ∖ {𝑋}) ∈ 𝒫 𝑊 ↔ (𝑥 ∖ {𝑋}) ⊆ 𝑊)
9894, 97sylibr 224 . . . . . . . . . . . 12 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (♯‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → (𝑥 ∖ {𝑋}) ∈ 𝒫 𝑊)
9966, 8syl 17 . . . . . . . . . . . . . . . . 17 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (♯‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → 𝑆 ∈ Fin)
100 ssfi 8336 . . . . . . . . . . . . . . . . 17 ((𝑆 ∈ Fin ∧ 𝑥𝑆) → 𝑥 ∈ Fin)
10199, 68, 100syl2anc 573 . . . . . . . . . . . . . . . 16 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (♯‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → 𝑥 ∈ Fin)
102 diffi 8348 . . . . . . . . . . . . . . . 16 (𝑥 ∈ Fin → (𝑥 ∖ {𝑋}) ∈ Fin)
103101, 102syl 17 . . . . . . . . . . . . . . 15 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (♯‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → (𝑥 ∖ {𝑋}) ∈ Fin)
104 hashcl 13349 . . . . . . . . . . . . . . 15 ((𝑥 ∖ {𝑋}) ∈ Fin → (♯‘(𝑥 ∖ {𝑋})) ∈ ℕ0)
105 nn0cn 11504 . . . . . . . . . . . . . . 15 ((♯‘(𝑥 ∖ {𝑋})) ∈ ℕ0 → (♯‘(𝑥 ∖ {𝑋})) ∈ ℂ)
106103, 104, 1053syl 18 . . . . . . . . . . . . . 14 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (♯‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → (♯‘(𝑥 ∖ {𝑋})) ∈ ℂ)
107 ax-1cn 10196 . . . . . . . . . . . . . 14 1 ∈ ℂ
108 pncan 10489 . . . . . . . . . . . . . 14 (((♯‘(𝑥 ∖ {𝑋})) ∈ ℂ ∧ 1 ∈ ℂ) → (((♯‘(𝑥 ∖ {𝑋})) + 1) − 1) = (♯‘(𝑥 ∖ {𝑋})))
109106, 107, 108sylancl 574 . . . . . . . . . . . . 13 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (♯‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → (((♯‘(𝑥 ∖ {𝑋})) + 1) − 1) = (♯‘(𝑥 ∖ {𝑋})))
110 neldifsnd 4459 . . . . . . . . . . . . . . . 16 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (♯‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → ¬ 𝑋 ∈ (𝑥 ∖ {𝑋}))
111 hashunsng 13383 . . . . . . . . . . . . . . . . 17 (𝑋𝑆 → (((𝑥 ∖ {𝑋}) ∈ Fin ∧ ¬ 𝑋 ∈ (𝑥 ∖ {𝑋})) → (♯‘((𝑥 ∖ {𝑋}) ∪ {𝑋})) = ((♯‘(𝑥 ∖ {𝑋})) + 1)))
11266, 5, 1113syl 18 . . . . . . . . . . . . . . . 16 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (♯‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → (((𝑥 ∖ {𝑋}) ∈ Fin ∧ ¬ 𝑋 ∈ (𝑥 ∖ {𝑋})) → (♯‘((𝑥 ∖ {𝑋}) ∪ {𝑋})) = ((♯‘(𝑥 ∖ {𝑋})) + 1)))
113103, 110, 112mp2and 679 . . . . . . . . . . . . . . 15 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (♯‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → (♯‘((𝑥 ∖ {𝑋}) ∪ {𝑋})) = ((♯‘(𝑥 ∖ {𝑋})) + 1))
114 undif1 4185 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∖ {𝑋}) ∪ {𝑋}) = (𝑥 ∪ {𝑋})
115 simpr 471 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (♯‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → ¬ 𝑥 ∈ 𝒫 𝑉)
11664, 115eldifd 3734 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (♯‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → 𝑥 ∈ (𝒫 (𝑉 ∪ {𝑋}) ∖ 𝒫 𝑉))
117 elpwunsn 4362 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ (𝒫 (𝑉 ∪ {𝑋}) ∖ 𝒫 𝑉) → 𝑋𝑥)
118116, 117syl 17 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (♯‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → 𝑋𝑥)
119118snssd 4475 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (♯‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → {𝑋} ⊆ 𝑥)
120 ssequn2 3937 . . . . . . . . . . . . . . . . . . 19 ({𝑋} ⊆ 𝑥 ↔ (𝑥 ∪ {𝑋}) = 𝑥)
121119, 120sylib 208 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (♯‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → (𝑥 ∪ {𝑋}) = 𝑥)
122114, 121syl5req 2818 . . . . . . . . . . . . . . . . 17 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (♯‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → 𝑥 = ((𝑥 ∖ {𝑋}) ∪ {𝑋}))
123122fveq2d 6336 . . . . . . . . . . . . . . . 16 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (♯‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → (♯‘𝑥) = (♯‘((𝑥 ∖ {𝑋}) ∪ {𝑋})))
124123, 72eqtr3d 2807 . . . . . . . . . . . . . . 15 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (♯‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → (♯‘((𝑥 ∖ {𝑋}) ∪ {𝑋})) = 𝑀)
125113, 124eqtr3d 2807 . . . . . . . . . . . . . 14 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (♯‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → ((♯‘(𝑥 ∖ {𝑋})) + 1) = 𝑀)
126125oveq1d 6808 . . . . . . . . . . . . 13 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (♯‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → (((♯‘(𝑥 ∖ {𝑋})) + 1) − 1) = (𝑀 − 1))
127109, 126eqtr3d 2807 . . . . . . . . . . . 12 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (♯‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → (♯‘(𝑥 ∖ {𝑋})) = (𝑀 − 1))
128 fveq2 6332 . . . . . . . . . . . . . 14 (𝑢 = (𝑥 ∖ {𝑋}) → (♯‘𝑢) = (♯‘(𝑥 ∖ {𝑋})))
129128eqeq1d 2773 . . . . . . . . . . . . 13 (𝑢 = (𝑥 ∖ {𝑋}) → ((♯‘𝑢) = (𝑀 − 1) ↔ (♯‘(𝑥 ∖ {𝑋})) = (𝑀 − 1)))
130129elrab 3515 . . . . . . . . . . . 12 ((𝑥 ∖ {𝑋}) ∈ {𝑢 ∈ 𝒫 𝑊 ∣ (♯‘𝑢) = (𝑀 − 1)} ↔ ((𝑥 ∖ {𝑋}) ∈ 𝒫 𝑊 ∧ (♯‘(𝑥 ∖ {𝑋})) = (𝑀 − 1)))
13198, 127, 130sylanbrc 572 . . . . . . . . . . 11 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (♯‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → (𝑥 ∖ {𝑋}) ∈ {𝑢 ∈ 𝒫 𝑊 ∣ (♯‘𝑢) = (𝑀 − 1)})
13288, 131sseldd 3753 . . . . . . . . . 10 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (♯‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → (𝑥 ∖ {𝑋}) ∈ (𝐻 “ {𝐷}))
133 ramub1.h . . . . . . . . . . . 12 𝐻 = (𝑢 ∈ ((𝑆 ∖ {𝑋})𝐶(𝑀 − 1)) ↦ (𝐾‘(𝑢 ∪ {𝑋})))
134133mptiniseg 5773 . . . . . . . . . . 11 (𝐷𝑅 → (𝐻 “ {𝐷}) = {𝑢 ∈ ((𝑆 ∖ {𝑋})𝐶(𝑀 − 1)) ∣ (𝐾‘(𝑢 ∪ {𝑋})) = 𝐷})
13566, 19, 1343syl 18 . . . . . . . . . 10 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (♯‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → (𝐻 “ {𝐷}) = {𝑢 ∈ ((𝑆 ∖ {𝑋})𝐶(𝑀 − 1)) ∣ (𝐾‘(𝑢 ∪ {𝑋})) = 𝐷})
136132, 135eleqtrd 2852 . . . . . . . . 9 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (♯‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → (𝑥 ∖ {𝑋}) ∈ {𝑢 ∈ ((𝑆 ∖ {𝑋})𝐶(𝑀 − 1)) ∣ (𝐾‘(𝑢 ∪ {𝑋})) = 𝐷})
137 uneq1 3911 . . . . . . . . . . . . 13 (𝑢 = (𝑥 ∖ {𝑋}) → (𝑢 ∪ {𝑋}) = ((𝑥 ∖ {𝑋}) ∪ {𝑋}))
138137fveq2d 6336 . . . . . . . . . . . 12 (𝑢 = (𝑥 ∖ {𝑋}) → (𝐾‘(𝑢 ∪ {𝑋})) = (𝐾‘((𝑥 ∖ {𝑋}) ∪ {𝑋})))
139138eqeq1d 2773 . . . . . . . . . . 11 (𝑢 = (𝑥 ∖ {𝑋}) → ((𝐾‘(𝑢 ∪ {𝑋})) = 𝐷 ↔ (𝐾‘((𝑥 ∖ {𝑋}) ∪ {𝑋})) = 𝐷))
140139elrab 3515 . . . . . . . . . 10 ((𝑥 ∖ {𝑋}) ∈ {𝑢 ∈ ((𝑆 ∖ {𝑋})𝐶(𝑀 − 1)) ∣ (𝐾‘(𝑢 ∪ {𝑋})) = 𝐷} ↔ ((𝑥 ∖ {𝑋}) ∈ ((𝑆 ∖ {𝑋})𝐶(𝑀 − 1)) ∧ (𝐾‘((𝑥 ∖ {𝑋}) ∪ {𝑋})) = 𝐷))
141140simprbi 484 . . . . . . . . 9 ((𝑥 ∖ {𝑋}) ∈ {𝑢 ∈ ((𝑆 ∖ {𝑋})𝐶(𝑀 − 1)) ∣ (𝐾‘(𝑢 ∪ {𝑋})) = 𝐷} → (𝐾‘((𝑥 ∖ {𝑋}) ∪ {𝑋})) = 𝐷)
142136, 141syl 17 . . . . . . . 8 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (♯‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → (𝐾‘((𝑥 ∖ {𝑋}) ∪ {𝑋})) = 𝐷)
143122fveq2d 6336 . . . . . . . 8 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (♯‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → (𝐾𝑥) = (𝐾‘((𝑥 ∖ {𝑋}) ∪ {𝑋})))
144 simpl1r 1280 . . . . . . . 8 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (♯‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → 𝐸 = 𝐷)
145142, 143, 1443eqtr4d 2815 . . . . . . 7 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (♯‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → (𝐾𝑥) = 𝐸)
146 ramub1.6 . . . . . . . . 9 (𝜑𝐾:(𝑆𝐶𝑀)⟶𝑅)
147 ffn 6185 . . . . . . . . 9 (𝐾:(𝑆𝐶𝑀)⟶𝑅𝐾 Fn (𝑆𝐶𝑀))
148146, 147syl 17 . . . . . . . 8 (𝜑𝐾 Fn (𝑆𝐶𝑀))
149 fniniseg 6481 . . . . . . . 8 (𝐾 Fn (𝑆𝐶𝑀) → (𝑥 ∈ (𝐾 “ {𝐸}) ↔ (𝑥 ∈ (𝑆𝐶𝑀) ∧ (𝐾𝑥) = 𝐸)))
15066, 148, 1493syl 18 . . . . . . 7 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (♯‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → (𝑥 ∈ (𝐾 “ {𝐸}) ↔ (𝑥 ∈ (𝑆𝐶𝑀) ∧ (𝐾𝑥) = 𝐸)))
15178, 145, 150mpbir2and 692 . . . . . 6 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (♯‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → 𝑥 ∈ (𝐾 “ {𝐸}))
15263, 151pm2.61dan 814 . . . . 5 (((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (♯‘𝑥) = 𝑀) → 𝑥 ∈ (𝐾 “ {𝐸}))
153152rabssdv 3831 . . . 4 ((𝜑𝐸 = 𝐷) → {𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∣ (♯‘𝑥) = 𝑀} ⊆ (𝐾 “ {𝐸}))
15452, 153eqsstrd 3788 . . 3 ((𝜑𝐸 = 𝐷) → ((𝑉 ∪ {𝑋})𝐶𝑀) ⊆ (𝐾 “ {𝐸}))
155 fveq2 6332 . . . . . 6 (𝑧 = (𝑉 ∪ {𝑋}) → (♯‘𝑧) = (♯‘(𝑉 ∪ {𝑋})))
156155breq2d 4798 . . . . 5 (𝑧 = (𝑉 ∪ {𝑋}) → ((𝐹𝐸) ≤ (♯‘𝑧) ↔ (𝐹𝐸) ≤ (♯‘(𝑉 ∪ {𝑋}))))
157 oveq1 6800 . . . . . 6 (𝑧 = (𝑉 ∪ {𝑋}) → (𝑧𝐶𝑀) = ((𝑉 ∪ {𝑋})𝐶𝑀))
158157sseq1d 3781 . . . . 5 (𝑧 = (𝑉 ∪ {𝑋}) → ((𝑧𝐶𝑀) ⊆ (𝐾 “ {𝐸}) ↔ ((𝑉 ∪ {𝑋})𝐶𝑀) ⊆ (𝐾 “ {𝐸})))
159156, 158anbi12d 616 . . . 4 (𝑧 = (𝑉 ∪ {𝑋}) → (((𝐹𝐸) ≤ (♯‘𝑧) ∧ (𝑧𝐶𝑀) ⊆ (𝐾 “ {𝐸})) ↔ ((𝐹𝐸) ≤ (♯‘(𝑉 ∪ {𝑋})) ∧ ((𝑉 ∪ {𝑋})𝐶𝑀) ⊆ (𝐾 “ {𝐸}))))
160159rspcev 3460 . . 3 (((𝑉 ∪ {𝑋}) ∈ 𝒫 𝑆 ∧ ((𝐹𝐸) ≤ (♯‘(𝑉 ∪ {𝑋})) ∧ ((𝑉 ∪ {𝑋})𝐶𝑀) ⊆ (𝐾 “ {𝐸}))) → ∃𝑧 ∈ 𝒫 𝑆((𝐹𝐸) ≤ (♯‘𝑧) ∧ (𝑧𝐶𝑀) ⊆ (𝐾 “ {𝐸})))
16112, 43, 154, 160syl12anc 1474 . 2 ((𝜑𝐸 = 𝐷) → ∃𝑧 ∈ 𝒫 𝑆((𝐹𝐸) ≤ (♯‘𝑧) ∧ (𝑧𝐶𝑀) ⊆ (𝐾 “ {𝐸})))
162 elpw2g 4958 . . . . . 6 (𝑆 ∈ Fin → (𝑉 ∈ 𝒫 𝑆𝑉𝑆))
1638, 162syl 17 . . . . 5 (𝜑 → (𝑉 ∈ 𝒫 𝑆𝑉𝑆))
1644, 163mpbird 247 . . . 4 (𝜑𝑉 ∈ 𝒫 𝑆)
165164adantr 466 . . 3 ((𝜑𝐸𝐷) → 𝑉 ∈ 𝒫 𝑆)
166 ifnefalse 4237 . . . . 5 (𝐸𝐷 → if(𝐸 = 𝐷, ((𝐹𝐷) − 1), (𝐹𝐸)) = (𝐹𝐸))
167166adantl 467 . . . 4 ((𝜑𝐸𝐷) → if(𝐸 = 𝐷, ((𝐹𝐷) − 1), (𝐹𝐸)) = (𝐹𝐸))
16815adantr 466 . . . 4 ((𝜑𝐸𝐷) → if(𝐸 = 𝐷, ((𝐹𝐷) − 1), (𝐹𝐸)) ≤ (♯‘𝑉))
169167, 168eqbrtrrd 4810 . . 3 ((𝜑𝐸𝐷) → (𝐹𝐸) ≤ (♯‘𝑉))
17056adantr 466 . . 3 ((𝜑𝐸𝐷) → (𝑉𝐶𝑀) ⊆ (𝐾 “ {𝐸}))
171 fveq2 6332 . . . . . 6 (𝑧 = 𝑉 → (♯‘𝑧) = (♯‘𝑉))
172171breq2d 4798 . . . . 5 (𝑧 = 𝑉 → ((𝐹𝐸) ≤ (♯‘𝑧) ↔ (𝐹𝐸) ≤ (♯‘𝑉)))
173 oveq1 6800 . . . . . 6 (𝑧 = 𝑉 → (𝑧𝐶𝑀) = (𝑉𝐶𝑀))
174173sseq1d 3781 . . . . 5 (𝑧 = 𝑉 → ((𝑧𝐶𝑀) ⊆ (𝐾 “ {𝐸}) ↔ (𝑉𝐶𝑀) ⊆ (𝐾 “ {𝐸})))
175172, 174anbi12d 616 . . . 4 (𝑧 = 𝑉 → (((𝐹𝐸) ≤ (♯‘𝑧) ∧ (𝑧𝐶𝑀) ⊆ (𝐾 “ {𝐸})) ↔ ((𝐹𝐸) ≤ (♯‘𝑉) ∧ (𝑉𝐶𝑀) ⊆ (𝐾 “ {𝐸}))))
176175rspcev 3460 . . 3 ((𝑉 ∈ 𝒫 𝑆 ∧ ((𝐹𝐸) ≤ (♯‘𝑉) ∧ (𝑉𝐶𝑀) ⊆ (𝐾 “ {𝐸}))) → ∃𝑧 ∈ 𝒫 𝑆((𝐹𝐸) ≤ (♯‘𝑧) ∧ (𝑧𝐶𝑀) ⊆ (𝐾 “ {𝐸})))
177165, 169, 170, 176syl12anc 1474 . 2 ((𝜑𝐸𝐷) → ∃𝑧 ∈ 𝒫 𝑆((𝐹𝐸) ≤ (♯‘𝑧) ∧ (𝑧𝐶𝑀) ⊆ (𝐾 “ {𝐸})))
178161, 177pm2.61dane 3030 1 (𝜑 → ∃𝑧 ∈ 𝒫 𝑆((𝐹𝐸) ≤ (♯‘𝑧) ∧ (𝑧𝐶𝑀) ⊆ (𝐾 “ {𝐸})))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∧ wa 382   ∧ w3a 1071   = wceq 1631   ∈ wcel 2145   ≠ wne 2943  ∃wrex 3062  {crab 3065  Vcvv 3351   ∖ cdif 3720   ∪ cun 3721   ⊆ wss 3723  ifcif 4225  𝒫 cpw 4297  {csn 4316   class class class wbr 4786   ↦ cmpt 4863  ◡ccnv 5248   “ cima 5252   Fn wfn 6026  ⟶wf 6027  ‘cfv 6031  (class class class)co 6793   ↦ cmpt2 6795  Fincfn 8109  ℂcc 10136  ℝcr 10137  1c1 10139   + caddc 10141   ≤ cle 10277   − cmin 10468  ℕcn 11222  ℕ0cn0 11494  ♯chash 13321   Ramsey cram 15910 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-rep 4904  ax-sep 4915  ax-nul 4923  ax-pow 4974  ax-pr 5034  ax-un 7096  ax-cnex 10194  ax-resscn 10195  ax-1cn 10196  ax-icn 10197  ax-addcl 10198  ax-addrcl 10199  ax-mulcl 10200  ax-mulrcl 10201  ax-mulcom 10202  ax-addass 10203  ax-mulass 10204  ax-distr 10205  ax-i2m1 10206  ax-1ne0 10207  ax-1rid 10208  ax-rnegex 10209  ax-rrecex 10210  ax-cnre 10211  ax-pre-lttri 10212  ax-pre-lttrn 10213  ax-pre-ltadd 10214  ax-pre-mulgt0 10215 This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3or 1072  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rmo 3069  df-rab 3070  df-v 3353  df-sbc 3588  df-csb 3683  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-pss 3739  df-nul 4064  df-if 4226  df-pw 4299  df-sn 4317  df-pr 4319  df-tp 4321  df-op 4323  df-uni 4575  df-int 4612  df-iun 4656  df-br 4787  df-opab 4847  df-mpt 4864  df-tr 4887  df-id 5157  df-eprel 5162  df-po 5170  df-so 5171  df-fr 5208  df-we 5210  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-pred 5823  df-ord 5869  df-on 5870  df-lim 5871  df-suc 5872  df-iota 5994  df-fun 6033  df-fn 6034  df-f 6035  df-f1 6036  df-fo 6037  df-f1o 6038  df-fv 6039  df-riota 6754  df-ov 6796  df-oprab 6797  df-mpt2 6798  df-om 7213  df-1st 7315  df-2nd 7316  df-wrecs 7559  df-recs 7621  df-rdg 7659  df-1o 7713  df-oadd 7717  df-er 7896  df-en 8110  df-dom 8111  df-sdom 8112  df-fin 8113  df-card 8965  df-cda 9192  df-pnf 10278  df-mnf 10279  df-xr 10280  df-ltxr 10281  df-le 10282  df-sub 10470  df-neg 10471  df-nn 11223  df-n0 11495  df-z 11580  df-uz 11889  df-fz 12534  df-hash 13322 This theorem is referenced by:  ramub1lem2  15938
 Copyright terms: Public domain W3C validator