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

Theorem ramub1lem1 16012
Description: Lemma for ramub1 16014. (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 3773 . . . . . . 7 (𝜑𝑉 ⊆ (𝑆 ∖ {𝑋}))
43difss2d 3904 . . . . . 6 (𝜑𝑉𝑆)
5 ramub1.x . . . . . . 7 (𝜑𝑋𝑆)
65snssd 4496 . . . . . 6 (𝜑 → {𝑋} ⊆ 𝑆)
74, 6unssd 3953 . . . . 5 (𝜑 → (𝑉 ∪ {𝑋}) ⊆ 𝑆)
8 ramub1.4 . . . . . 6 (𝜑𝑆 ∈ Fin)
9 elpw2g 4987 . . . . . 6 (𝑆 ∈ Fin → ((𝑉 ∪ {𝑋}) ∈ 𝒫 𝑆 ↔ (𝑉 ∪ {𝑋}) ⊆ 𝑆))
108, 9syl 17 . . . . 5 (𝜑 → ((𝑉 ∪ {𝑋}) ∈ 𝒫 𝑆 ↔ (𝑉 ∪ {𝑋}) ⊆ 𝑆))
117, 10mpbird 248 . . . 4 (𝜑 → (𝑉 ∪ {𝑋}) ∈ 𝒫 𝑆)
1211adantr 472 . . 3 ((𝜑𝐸 = 𝐷) → (𝑉 ∪ {𝑋}) ∈ 𝒫 𝑆)
13 iftrue 4251 . . . . . . 7 (𝐸 = 𝐷 → if(𝐸 = 𝐷, ((𝐹𝐷) − 1), (𝐹𝐸)) = ((𝐹𝐷) − 1))
1413adantl 473 . . . . . 6 ((𝜑𝐸 = 𝐷) → if(𝐸 = 𝐷, ((𝐹𝐷) − 1), (𝐹𝐸)) = ((𝐹𝐷) − 1))
15 ramub1.9 . . . . . . 7 (𝜑 → if(𝐸 = 𝐷, ((𝐹𝐷) − 1), (𝐹𝐸)) ≤ (♯‘𝑉))
1615adantr 472 . . . . . 6 ((𝜑𝐸 = 𝐷) → if(𝐸 = 𝐷, ((𝐹𝐷) − 1), (𝐹𝐸)) ≤ (♯‘𝑉))
1714, 16eqbrtrrd 4835 . . . . 5 ((𝜑𝐸 = 𝐷) → ((𝐹𝐷) − 1) ≤ (♯‘𝑉))
18 ramub1.f . . . . . . . . 9 (𝜑𝐹:𝑅⟶ℕ)
19 ramub1.d . . . . . . . . 9 (𝜑𝐷𝑅)
2018, 19ffvelrnd 6552 . . . . . . . 8 (𝜑 → (𝐹𝐷) ∈ ℕ)
2120adantr 472 . . . . . . 7 ((𝜑𝐸 = 𝐷) → (𝐹𝐷) ∈ ℕ)
2221nnred 11293 . . . . . 6 ((𝜑𝐸 = 𝐷) → (𝐹𝐷) ∈ ℝ)
23 1red 10296 . . . . . 6 ((𝜑𝐸 = 𝐷) → 1 ∈ ℝ)
24 ssfi 8389 . . . . . . . . 9 ((𝑆 ∈ Fin ∧ 𝑉𝑆) → 𝑉 ∈ Fin)
258, 4, 24syl2anc 579 . . . . . . . 8 (𝜑𝑉 ∈ Fin)
26 hashcl 13352 . . . . . . . 8 (𝑉 ∈ Fin → (♯‘𝑉) ∈ ℕ0)
27 nn0re 11550 . . . . . . . 8 ((♯‘𝑉) ∈ ℕ0 → (♯‘𝑉) ∈ ℝ)
2825, 26, 273syl 18 . . . . . . 7 (𝜑 → (♯‘𝑉) ∈ ℝ)
2928adantr 472 . . . . . 6 ((𝜑𝐸 = 𝐷) → (♯‘𝑉) ∈ ℝ)
3022, 23, 29lesubaddd 10880 . . . . 5 ((𝜑𝐸 = 𝐷) → (((𝐹𝐷) − 1) ≤ (♯‘𝑉) ↔ (𝐹𝐷) ≤ ((♯‘𝑉) + 1)))
3117, 30mpbid 223 . . . 4 ((𝜑𝐸 = 𝐷) → (𝐹𝐷) ≤ ((♯‘𝑉) + 1))
32 fveq2 6377 . . . . 5 (𝐸 = 𝐷 → (𝐹𝐸) = (𝐹𝐷))
33 snidg 4366 . . . . . . . 8 (𝑋𝑆𝑋 ∈ {𝑋})
345, 33syl 17 . . . . . . 7 (𝜑𝑋 ∈ {𝑋})
353sseld 3762 . . . . . . . 8 (𝜑 → (𝑋𝑉𝑋 ∈ (𝑆 ∖ {𝑋})))
36 eldifn 3897 . . . . . . . 8 (𝑋 ∈ (𝑆 ∖ {𝑋}) → ¬ 𝑋 ∈ {𝑋})
3735, 36syl6 35 . . . . . . 7 (𝜑 → (𝑋𝑉 → ¬ 𝑋 ∈ {𝑋}))
3834, 37mt2d 133 . . . . . 6 (𝜑 → ¬ 𝑋𝑉)
39 hashunsng 13386 . . . . . . 7 (𝑋𝑆 → ((𝑉 ∈ Fin ∧ ¬ 𝑋𝑉) → (♯‘(𝑉 ∪ {𝑋})) = ((♯‘𝑉) + 1)))
405, 39syl 17 . . . . . 6 (𝜑 → ((𝑉 ∈ Fin ∧ ¬ 𝑋𝑉) → (♯‘(𝑉 ∪ {𝑋})) = ((♯‘𝑉) + 1)))
4125, 38, 40mp2and 690 . . . . 5 (𝜑 → (♯‘(𝑉 ∪ {𝑋})) = ((♯‘𝑉) + 1))
4232, 41breqan12rd 4828 . . . 4 ((𝜑𝐸 = 𝐷) → ((𝐹𝐸) ≤ (♯‘(𝑉 ∪ {𝑋})) ↔ (𝐹𝐷) ≤ ((♯‘𝑉) + 1)))
4331, 42mpbird 248 . . 3 ((𝜑𝐸 = 𝐷) → (𝐹𝐸) ≤ (♯‘(𝑉 ∪ {𝑋})))
44 snfi 8247 . . . . . . 7 {𝑋} ∈ Fin
45 unfi 8436 . . . . . . 7 ((𝑉 ∈ Fin ∧ {𝑋} ∈ Fin) → (𝑉 ∪ {𝑋}) ∈ Fin)
4625, 44, 45sylancl 580 . . . . . 6 (𝜑 → (𝑉 ∪ {𝑋}) ∈ Fin)
47 ramub1.m . . . . . . 7 (𝜑𝑀 ∈ ℕ)
4847nnnn0d 11600 . . . . . 6 (𝜑𝑀 ∈ ℕ0)
49 ramub1.3 . . . . . . 7 𝐶 = (𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (♯‘𝑏) = 𝑖})
5049hashbcval 15988 . . . . . 6 (((𝑉 ∪ {𝑋}) ∈ Fin ∧ 𝑀 ∈ ℕ0) → ((𝑉 ∪ {𝑋})𝐶𝑀) = {𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∣ (♯‘𝑥) = 𝑀})
5146, 48, 50syl2anc 579 . . . . 5 (𝜑 → ((𝑉 ∪ {𝑋})𝐶𝑀) = {𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∣ (♯‘𝑥) = 𝑀})
5251adantr 472 . . . 4 ((𝜑𝐸 = 𝐷) → ((𝑉 ∪ {𝑋})𝐶𝑀) = {𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∣ (♯‘𝑥) = 𝑀})
53 simpl1l 1293 . . . . . . . 8 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (♯‘𝑥) = 𝑀) ∧ 𝑥 ∈ 𝒫 𝑉) → 𝜑)
5449hashbcval 15988 . . . . . . . . . 10 ((𝑉 ∈ Fin ∧ 𝑀 ∈ ℕ0) → (𝑉𝐶𝑀) = {𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 𝑀})
5525, 48, 54syl2anc 579 . . . . . . . . 9 (𝜑 → (𝑉𝐶𝑀) = {𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 𝑀})
56 ramub1.s . . . . . . . . 9 (𝜑 → (𝑉𝐶𝑀) ⊆ (𝐾 “ {𝐸}))
5755, 56eqsstr3d 3802 . . . . . . . 8 (𝜑 → {𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 𝑀} ⊆ (𝐾 “ {𝐸}))
5853, 57syl 17 . . . . . . 7 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (♯‘𝑥) = 𝑀) ∧ 𝑥 ∈ 𝒫 𝑉) → {𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 𝑀} ⊆ (𝐾 “ {𝐸}))
59 simpr 477 . . . . . . . 8 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (♯‘𝑥) = 𝑀) ∧ 𝑥 ∈ 𝒫 𝑉) → 𝑥 ∈ 𝒫 𝑉)
60 simpl3 1246 . . . . . . . 8 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (♯‘𝑥) = 𝑀) ∧ 𝑥 ∈ 𝒫 𝑉) → (♯‘𝑥) = 𝑀)
61 rabid 3263 . . . . . . . 8 (𝑥 ∈ {𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 𝑀} ↔ (𝑥 ∈ 𝒫 𝑉 ∧ (♯‘𝑥) = 𝑀))
6259, 60, 61sylanbrc 578 . . . . . . 7 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (♯‘𝑥) = 𝑀) ∧ 𝑥 ∈ 𝒫 𝑉) → 𝑥 ∈ {𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 𝑀})
6358, 62sseldd 3764 . . . . . 6 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (♯‘𝑥) = 𝑀) ∧ 𝑥 ∈ 𝒫 𝑉) → 𝑥 ∈ (𝐾 “ {𝐸}))
64 simpl2 1244 . . . . . . . . . . . 12 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (♯‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}))
6564elpwid 4329 . . . . . . . . . . 11 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (♯‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → 𝑥 ⊆ (𝑉 ∪ {𝑋}))
66 simpl1l 1293 . . . . . . . . . . . 12 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (♯‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → 𝜑)
6766, 7syl 17 . . . . . . . . . . 11 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (♯‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → (𝑉 ∪ {𝑋}) ⊆ 𝑆)
6865, 67sstrd 3773 . . . . . . . . . 10 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (♯‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → 𝑥𝑆)
69 vex 3353 . . . . . . . . . . 11 𝑥 ∈ V
7069elpw 4323 . . . . . . . . . 10 (𝑥 ∈ 𝒫 𝑆𝑥𝑆)
7168, 70sylibr 225 . . . . . . . . 9 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (♯‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → 𝑥 ∈ 𝒫 𝑆)
72 simpl3 1246 . . . . . . . . 9 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (♯‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → (♯‘𝑥) = 𝑀)
73 rabid 3263 . . . . . . . . 9 (𝑥 ∈ {𝑥 ∈ 𝒫 𝑆 ∣ (♯‘𝑥) = 𝑀} ↔ (𝑥 ∈ 𝒫 𝑆 ∧ (♯‘𝑥) = 𝑀))
7471, 72, 73sylanbrc 578 . . . . . . . 8 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (♯‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → 𝑥 ∈ {𝑥 ∈ 𝒫 𝑆 ∣ (♯‘𝑥) = 𝑀})
7549hashbcval 15988 . . . . . . . . . 10 ((𝑆 ∈ Fin ∧ 𝑀 ∈ ℕ0) → (𝑆𝐶𝑀) = {𝑥 ∈ 𝒫 𝑆 ∣ (♯‘𝑥) = 𝑀})
768, 48, 75syl2anc 579 . . . . . . . . 9 (𝜑 → (𝑆𝐶𝑀) = {𝑥 ∈ 𝒫 𝑆 ∣ (♯‘𝑥) = 𝑀})
7766, 76syl 17 . . . . . . . 8 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (♯‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → (𝑆𝐶𝑀) = {𝑥 ∈ 𝒫 𝑆 ∣ (♯‘𝑥) = 𝑀})
7874, 77eleqtrrd 2847 . . . . . . 7 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (♯‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → 𝑥 ∈ (𝑆𝐶𝑀))
792difss2d 3904 . . . . . . . . . . . . . . 15 (𝜑𝑊𝑆)
80 ssfi 8389 . . . . . . . . . . . . . . 15 ((𝑆 ∈ Fin ∧ 𝑊𝑆) → 𝑊 ∈ Fin)
818, 79, 80syl2anc 579 . . . . . . . . . . . . . 14 (𝜑𝑊 ∈ Fin)
82 nnm1nn0 11583 . . . . . . . . . . . . . . 15 (𝑀 ∈ ℕ → (𝑀 − 1) ∈ ℕ0)
8347, 82syl 17 . . . . . . . . . . . . . 14 (𝜑 → (𝑀 − 1) ∈ ℕ0)
8449hashbcval 15988 . . . . . . . . . . . . . 14 ((𝑊 ∈ Fin ∧ (𝑀 − 1) ∈ ℕ0) → (𝑊𝐶(𝑀 − 1)) = {𝑢 ∈ 𝒫 𝑊 ∣ (♯‘𝑢) = (𝑀 − 1)})
8581, 83, 84syl2anc 579 . . . . . . . . . . . . 13 (𝜑 → (𝑊𝐶(𝑀 − 1)) = {𝑢 ∈ 𝒫 𝑊 ∣ (♯‘𝑢) = (𝑀 − 1)})
86 ramub1.8 . . . . . . . . . . . . 13 (𝜑 → (𝑊𝐶(𝑀 − 1)) ⊆ (𝐻 “ {𝐷}))
8785, 86eqsstr3d 3802 . . . . . . . . . . . 12 (𝜑 → {𝑢 ∈ 𝒫 𝑊 ∣ (♯‘𝑢) = (𝑀 − 1)} ⊆ (𝐻 “ {𝐷}))
8866, 87syl 17 . . . . . . . . . . 11 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (♯‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → {𝑢 ∈ 𝒫 𝑊 ∣ (♯‘𝑢) = (𝑀 − 1)} ⊆ (𝐻 “ {𝐷}))
89 uncom 3921 . . . . . . . . . . . . . . . 16 (𝑉 ∪ {𝑋}) = ({𝑋} ∪ 𝑉)
9065, 89syl6sseq 3813 . . . . . . . . . . . . . . 15 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (♯‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → 𝑥 ⊆ ({𝑋} ∪ 𝑉))
91 ssundif 4214 . . . . . . . . . . . . . . 15 (𝑥 ⊆ ({𝑋} ∪ 𝑉) ↔ (𝑥 ∖ {𝑋}) ⊆ 𝑉)
9290, 91sylib 209 . . . . . . . . . . . . . 14 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (♯‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → (𝑥 ∖ {𝑋}) ⊆ 𝑉)
9366, 1syl 17 . . . . . . . . . . . . . 14 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (♯‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → 𝑉𝑊)
9492, 93sstrd 3773 . . . . . . . . . . . . 13 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (♯‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → (𝑥 ∖ {𝑋}) ⊆ 𝑊)
95 difexg 4971 . . . . . . . . . . . . . . 15 (𝑥 ∈ V → (𝑥 ∖ {𝑋}) ∈ V)
9669, 95ax-mp 5 . . . . . . . . . . . . . 14 (𝑥 ∖ {𝑋}) ∈ V
9796elpw 4323 . . . . . . . . . . . . 13 ((𝑥 ∖ {𝑋}) ∈ 𝒫 𝑊 ↔ (𝑥 ∖ {𝑋}) ⊆ 𝑊)
9894, 97sylibr 225 . . . . . . . . . . . 12 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (♯‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → (𝑥 ∖ {𝑋}) ∈ 𝒫 𝑊)
9966, 8syl 17 . . . . . . . . . . . . . . . . 17 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (♯‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → 𝑆 ∈ Fin)
100 ssfi 8389 . . . . . . . . . . . . . . . . 17 ((𝑆 ∈ Fin ∧ 𝑥𝑆) → 𝑥 ∈ Fin)
10199, 68, 100syl2anc 579 . . . . . . . . . . . . . . . 16 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (♯‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → 𝑥 ∈ Fin)
102 diffi 8401 . . . . . . . . . . . . . . . 16 (𝑥 ∈ Fin → (𝑥 ∖ {𝑋}) ∈ Fin)
103101, 102syl 17 . . . . . . . . . . . . . . 15 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (♯‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → (𝑥 ∖ {𝑋}) ∈ Fin)
104 hashcl 13352 . . . . . . . . . . . . . . 15 ((𝑥 ∖ {𝑋}) ∈ Fin → (♯‘(𝑥 ∖ {𝑋})) ∈ ℕ0)
105 nn0cn 11551 . . . . . . . . . . . . . . 15 ((♯‘(𝑥 ∖ {𝑋})) ∈ ℕ0 → (♯‘(𝑥 ∖ {𝑋})) ∈ ℂ)
106103, 104, 1053syl 18 . . . . . . . . . . . . . 14 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (♯‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → (♯‘(𝑥 ∖ {𝑋})) ∈ ℂ)
107 ax-1cn 10249 . . . . . . . . . . . . . 14 1 ∈ ℂ
108 pncan 10543 . . . . . . . . . . . . . 14 (((♯‘(𝑥 ∖ {𝑋})) ∈ ℂ ∧ 1 ∈ ℂ) → (((♯‘(𝑥 ∖ {𝑋})) + 1) − 1) = (♯‘(𝑥 ∖ {𝑋})))
109106, 107, 108sylancl 580 . . . . . . . . . . . . 13 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (♯‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → (((♯‘(𝑥 ∖ {𝑋})) + 1) − 1) = (♯‘(𝑥 ∖ {𝑋})))
110 neldifsnd 4480 . . . . . . . . . . . . . . . 16 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (♯‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → ¬ 𝑋 ∈ (𝑥 ∖ {𝑋}))
111 hashunsng 13386 . . . . . . . . . . . . . . . . 17 (𝑋𝑆 → (((𝑥 ∖ {𝑋}) ∈ Fin ∧ ¬ 𝑋 ∈ (𝑥 ∖ {𝑋})) → (♯‘((𝑥 ∖ {𝑋}) ∪ {𝑋})) = ((♯‘(𝑥 ∖ {𝑋})) + 1)))
11266, 5, 1113syl 18 . . . . . . . . . . . . . . . 16 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (♯‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → (((𝑥 ∖ {𝑋}) ∈ Fin ∧ ¬ 𝑋 ∈ (𝑥 ∖ {𝑋})) → (♯‘((𝑥 ∖ {𝑋}) ∪ {𝑋})) = ((♯‘(𝑥 ∖ {𝑋})) + 1)))
113103, 110, 112mp2and 690 . . . . . . . . . . . . . . 15 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (♯‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → (♯‘((𝑥 ∖ {𝑋}) ∪ {𝑋})) = ((♯‘(𝑥 ∖ {𝑋})) + 1))
114 undif1 4205 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∖ {𝑋}) ∪ {𝑋}) = (𝑥 ∪ {𝑋})
115 simpr 477 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (♯‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → ¬ 𝑥 ∈ 𝒫 𝑉)
11664, 115eldifd 3745 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (♯‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → 𝑥 ∈ (𝒫 (𝑉 ∪ {𝑋}) ∖ 𝒫 𝑉))
117 elpwunsn 4383 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ (𝒫 (𝑉 ∪ {𝑋}) ∖ 𝒫 𝑉) → 𝑋𝑥)
118116, 117syl 17 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (♯‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → 𝑋𝑥)
119118snssd 4496 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (♯‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → {𝑋} ⊆ 𝑥)
120 ssequn2 3950 . . . . . . . . . . . . . . . . . . 19 ({𝑋} ⊆ 𝑥 ↔ (𝑥 ∪ {𝑋}) = 𝑥)
121119, 120sylib 209 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (♯‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → (𝑥 ∪ {𝑋}) = 𝑥)
122114, 121syl5req 2812 . . . . . . . . . . . . . . . . 17 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (♯‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → 𝑥 = ((𝑥 ∖ {𝑋}) ∪ {𝑋}))
123122fveq2d 6381 . . . . . . . . . . . . . . . 16 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (♯‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → (♯‘𝑥) = (♯‘((𝑥 ∖ {𝑋}) ∪ {𝑋})))
124123, 72eqtr3d 2801 . . . . . . . . . . . . . . 15 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (♯‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → (♯‘((𝑥 ∖ {𝑋}) ∪ {𝑋})) = 𝑀)
125113, 124eqtr3d 2801 . . . . . . . . . . . . . 14 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (♯‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → ((♯‘(𝑥 ∖ {𝑋})) + 1) = 𝑀)
126125oveq1d 6859 . . . . . . . . . . . . 13 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (♯‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → (((♯‘(𝑥 ∖ {𝑋})) + 1) − 1) = (𝑀 − 1))
127109, 126eqtr3d 2801 . . . . . . . . . . . 12 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (♯‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → (♯‘(𝑥 ∖ {𝑋})) = (𝑀 − 1))
128 fveqeq2 6386 . . . . . . . . . . . . 13 (𝑢 = (𝑥 ∖ {𝑋}) → ((♯‘𝑢) = (𝑀 − 1) ↔ (♯‘(𝑥 ∖ {𝑋})) = (𝑀 − 1)))
129128elrab 3521 . . . . . . . . . . . 12 ((𝑥 ∖ {𝑋}) ∈ {𝑢 ∈ 𝒫 𝑊 ∣ (♯‘𝑢) = (𝑀 − 1)} ↔ ((𝑥 ∖ {𝑋}) ∈ 𝒫 𝑊 ∧ (♯‘(𝑥 ∖ {𝑋})) = (𝑀 − 1)))
13098, 127, 129sylanbrc 578 . . . . . . . . . . 11 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (♯‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → (𝑥 ∖ {𝑋}) ∈ {𝑢 ∈ 𝒫 𝑊 ∣ (♯‘𝑢) = (𝑀 − 1)})
13188, 130sseldd 3764 . . . . . . . . . 10 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (♯‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → (𝑥 ∖ {𝑋}) ∈ (𝐻 “ {𝐷}))
132 ramub1.h . . . . . . . . . . . 12 𝐻 = (𝑢 ∈ ((𝑆 ∖ {𝑋})𝐶(𝑀 − 1)) ↦ (𝐾‘(𝑢 ∪ {𝑋})))
133132mptiniseg 5817 . . . . . . . . . . 11 (𝐷𝑅 → (𝐻 “ {𝐷}) = {𝑢 ∈ ((𝑆 ∖ {𝑋})𝐶(𝑀 − 1)) ∣ (𝐾‘(𝑢 ∪ {𝑋})) = 𝐷})
13466, 19, 1333syl 18 . . . . . . . . . 10 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (♯‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → (𝐻 “ {𝐷}) = {𝑢 ∈ ((𝑆 ∖ {𝑋})𝐶(𝑀 − 1)) ∣ (𝐾‘(𝑢 ∪ {𝑋})) = 𝐷})
135131, 134eleqtrd 2846 . . . . . . . . 9 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (♯‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → (𝑥 ∖ {𝑋}) ∈ {𝑢 ∈ ((𝑆 ∖ {𝑋})𝐶(𝑀 − 1)) ∣ (𝐾‘(𝑢 ∪ {𝑋})) = 𝐷})
136 uneq1 3924 . . . . . . . . . . . 12 (𝑢 = (𝑥 ∖ {𝑋}) → (𝑢 ∪ {𝑋}) = ((𝑥 ∖ {𝑋}) ∪ {𝑋}))
137136fveqeq2d 6385 . . . . . . . . . . 11 (𝑢 = (𝑥 ∖ {𝑋}) → ((𝐾‘(𝑢 ∪ {𝑋})) = 𝐷 ↔ (𝐾‘((𝑥 ∖ {𝑋}) ∪ {𝑋})) = 𝐷))
138137elrab 3521 . . . . . . . . . 10 ((𝑥 ∖ {𝑋}) ∈ {𝑢 ∈ ((𝑆 ∖ {𝑋})𝐶(𝑀 − 1)) ∣ (𝐾‘(𝑢 ∪ {𝑋})) = 𝐷} ↔ ((𝑥 ∖ {𝑋}) ∈ ((𝑆 ∖ {𝑋})𝐶(𝑀 − 1)) ∧ (𝐾‘((𝑥 ∖ {𝑋}) ∪ {𝑋})) = 𝐷))
139138simprbi 490 . . . . . . . . 9 ((𝑥 ∖ {𝑋}) ∈ {𝑢 ∈ ((𝑆 ∖ {𝑋})𝐶(𝑀 − 1)) ∣ (𝐾‘(𝑢 ∪ {𝑋})) = 𝐷} → (𝐾‘((𝑥 ∖ {𝑋}) ∪ {𝑋})) = 𝐷)
140135, 139syl 17 . . . . . . . 8 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (♯‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → (𝐾‘((𝑥 ∖ {𝑋}) ∪ {𝑋})) = 𝐷)
141122fveq2d 6381 . . . . . . . 8 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (♯‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → (𝐾𝑥) = (𝐾‘((𝑥 ∖ {𝑋}) ∪ {𝑋})))
142 simpl1r 1295 . . . . . . . 8 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (♯‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → 𝐸 = 𝐷)
143140, 141, 1423eqtr4d 2809 . . . . . . 7 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (♯‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → (𝐾𝑥) = 𝐸)
144 ramub1.6 . . . . . . . . 9 (𝜑𝐾:(𝑆𝐶𝑀)⟶𝑅)
145144ffnd 6226 . . . . . . . 8 (𝜑𝐾 Fn (𝑆𝐶𝑀))
146 fniniseg 6530 . . . . . . . 8 (𝐾 Fn (𝑆𝐶𝑀) → (𝑥 ∈ (𝐾 “ {𝐸}) ↔ (𝑥 ∈ (𝑆𝐶𝑀) ∧ (𝐾𝑥) = 𝐸)))
14766, 145, 1463syl 18 . . . . . . 7 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (♯‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → (𝑥 ∈ (𝐾 “ {𝐸}) ↔ (𝑥 ∈ (𝑆𝐶𝑀) ∧ (𝐾𝑥) = 𝐸)))
14878, 143, 147mpbir2and 704 . . . . . 6 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (♯‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → 𝑥 ∈ (𝐾 “ {𝐸}))
14963, 148pm2.61dan 847 . . . . 5 (((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (♯‘𝑥) = 𝑀) → 𝑥 ∈ (𝐾 “ {𝐸}))
150149rabssdv 3844 . . . 4 ((𝜑𝐸 = 𝐷) → {𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∣ (♯‘𝑥) = 𝑀} ⊆ (𝐾 “ {𝐸}))
15152, 150eqsstrd 3801 . . 3 ((𝜑𝐸 = 𝐷) → ((𝑉 ∪ {𝑋})𝐶𝑀) ⊆ (𝐾 “ {𝐸}))
152 fveq2 6377 . . . . . 6 (𝑧 = (𝑉 ∪ {𝑋}) → (♯‘𝑧) = (♯‘(𝑉 ∪ {𝑋})))
153152breq2d 4823 . . . . 5 (𝑧 = (𝑉 ∪ {𝑋}) → ((𝐹𝐸) ≤ (♯‘𝑧) ↔ (𝐹𝐸) ≤ (♯‘(𝑉 ∪ {𝑋}))))
154 oveq1 6851 . . . . . 6 (𝑧 = (𝑉 ∪ {𝑋}) → (𝑧𝐶𝑀) = ((𝑉 ∪ {𝑋})𝐶𝑀))
155154sseq1d 3794 . . . . 5 (𝑧 = (𝑉 ∪ {𝑋}) → ((𝑧𝐶𝑀) ⊆ (𝐾 “ {𝐸}) ↔ ((𝑉 ∪ {𝑋})𝐶𝑀) ⊆ (𝐾 “ {𝐸})))
156153, 155anbi12d 624 . . . 4 (𝑧 = (𝑉 ∪ {𝑋}) → (((𝐹𝐸) ≤ (♯‘𝑧) ∧ (𝑧𝐶𝑀) ⊆ (𝐾 “ {𝐸})) ↔ ((𝐹𝐸) ≤ (♯‘(𝑉 ∪ {𝑋})) ∧ ((𝑉 ∪ {𝑋})𝐶𝑀) ⊆ (𝐾 “ {𝐸}))))
157156rspcev 3462 . . 3 (((𝑉 ∪ {𝑋}) ∈ 𝒫 𝑆 ∧ ((𝐹𝐸) ≤ (♯‘(𝑉 ∪ {𝑋})) ∧ ((𝑉 ∪ {𝑋})𝐶𝑀) ⊆ (𝐾 “ {𝐸}))) → ∃𝑧 ∈ 𝒫 𝑆((𝐹𝐸) ≤ (♯‘𝑧) ∧ (𝑧𝐶𝑀) ⊆ (𝐾 “ {𝐸})))
15812, 43, 151, 157syl12anc 865 . 2 ((𝜑𝐸 = 𝐷) → ∃𝑧 ∈ 𝒫 𝑆((𝐹𝐸) ≤ (♯‘𝑧) ∧ (𝑧𝐶𝑀) ⊆ (𝐾 “ {𝐸})))
159 elpw2g 4987 . . . . . 6 (𝑆 ∈ Fin → (𝑉 ∈ 𝒫 𝑆𝑉𝑆))
1608, 159syl 17 . . . . 5 (𝜑 → (𝑉 ∈ 𝒫 𝑆𝑉𝑆))
1614, 160mpbird 248 . . . 4 (𝜑𝑉 ∈ 𝒫 𝑆)
162161adantr 472 . . 3 ((𝜑𝐸𝐷) → 𝑉 ∈ 𝒫 𝑆)
163 ifnefalse 4257 . . . . 5 (𝐸𝐷 → if(𝐸 = 𝐷, ((𝐹𝐷) − 1), (𝐹𝐸)) = (𝐹𝐸))
164163adantl 473 . . . 4 ((𝜑𝐸𝐷) → if(𝐸 = 𝐷, ((𝐹𝐷) − 1), (𝐹𝐸)) = (𝐹𝐸))
16515adantr 472 . . . 4 ((𝜑𝐸𝐷) → if(𝐸 = 𝐷, ((𝐹𝐷) − 1), (𝐹𝐸)) ≤ (♯‘𝑉))
166164, 165eqbrtrrd 4835 . . 3 ((𝜑𝐸𝐷) → (𝐹𝐸) ≤ (♯‘𝑉))
16756adantr 472 . . 3 ((𝜑𝐸𝐷) → (𝑉𝐶𝑀) ⊆ (𝐾 “ {𝐸}))
168 fveq2 6377 . . . . . 6 (𝑧 = 𝑉 → (♯‘𝑧) = (♯‘𝑉))
169168breq2d 4823 . . . . 5 (𝑧 = 𝑉 → ((𝐹𝐸) ≤ (♯‘𝑧) ↔ (𝐹𝐸) ≤ (♯‘𝑉)))
170 oveq1 6851 . . . . . 6 (𝑧 = 𝑉 → (𝑧𝐶𝑀) = (𝑉𝐶𝑀))
171170sseq1d 3794 . . . . 5 (𝑧 = 𝑉 → ((𝑧𝐶𝑀) ⊆ (𝐾 “ {𝐸}) ↔ (𝑉𝐶𝑀) ⊆ (𝐾 “ {𝐸})))
172169, 171anbi12d 624 . . . 4 (𝑧 = 𝑉 → (((𝐹𝐸) ≤ (♯‘𝑧) ∧ (𝑧𝐶𝑀) ⊆ (𝐾 “ {𝐸})) ↔ ((𝐹𝐸) ≤ (♯‘𝑉) ∧ (𝑉𝐶𝑀) ⊆ (𝐾 “ {𝐸}))))
173172rspcev 3462 . . 3 ((𝑉 ∈ 𝒫 𝑆 ∧ ((𝐹𝐸) ≤ (♯‘𝑉) ∧ (𝑉𝐶𝑀) ⊆ (𝐾 “ {𝐸}))) → ∃𝑧 ∈ 𝒫 𝑆((𝐹𝐸) ≤ (♯‘𝑧) ∧ (𝑧𝐶𝑀) ⊆ (𝐾 “ {𝐸})))
174162, 166, 167, 173syl12anc 865 . 2 ((𝜑𝐸𝐷) → ∃𝑧 ∈ 𝒫 𝑆((𝐹𝐸) ≤ (♯‘𝑧) ∧ (𝑧𝐶𝑀) ⊆ (𝐾 “ {𝐸})))
175158, 174pm2.61dane 3024 1 (𝜑 → ∃𝑧 ∈ 𝒫 𝑆((𝐹𝐸) ≤ (♯‘𝑧) ∧ (𝑧𝐶𝑀) ⊆ (𝐾 “ {𝐸})))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  w3a 1107   = wceq 1652  wcel 2155  wne 2937  wrex 3056  {crab 3059  Vcvv 3350  cdif 3731  cun 3732  wss 3734  ifcif 4245  𝒫 cpw 4317  {csn 4336   class class class wbr 4811  cmpt 4890  ccnv 5278  cima 5282   Fn wfn 6065  wf 6066  cfv 6070  (class class class)co 6844  cmpt2 6846  Fincfn 8162  cc 10189  cr 10190  1c1 10192   + caddc 10194  cle 10331  cmin 10522  cn 11276  0cn0 11540  chash 13324   Ramsey cram 15985
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-rep 4932  ax-sep 4943  ax-nul 4951  ax-pow 5003  ax-pr 5064  ax-un 7149  ax-cnex 10247  ax-resscn 10248  ax-1cn 10249  ax-icn 10250  ax-addcl 10251  ax-addrcl 10252  ax-mulcl 10253  ax-mulrcl 10254  ax-mulcom 10255  ax-addass 10256  ax-mulass 10257  ax-distr 10258  ax-i2m1 10259  ax-1ne0 10260  ax-1rid 10261  ax-rnegex 10262  ax-rrecex 10263  ax-cnre 10264  ax-pre-lttri 10265  ax-pre-lttrn 10266  ax-pre-ltadd 10267  ax-pre-mulgt0 10268
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-nel 3041  df-ral 3060  df-rex 3061  df-reu 3062  df-rmo 3063  df-rab 3064  df-v 3352  df-sbc 3599  df-csb 3694  df-dif 3737  df-un 3739  df-in 3741  df-ss 3748  df-pss 3750  df-nul 4082  df-if 4246  df-pw 4319  df-sn 4337  df-pr 4339  df-tp 4341  df-op 4343  df-uni 4597  df-int 4636  df-iun 4680  df-br 4812  df-opab 4874  df-mpt 4891  df-tr 4914  df-id 5187  df-eprel 5192  df-po 5200  df-so 5201  df-fr 5238  df-we 5240  df-xp 5285  df-rel 5286  df-cnv 5287  df-co 5288  df-dm 5289  df-rn 5290  df-res 5291  df-ima 5292  df-pred 5867  df-ord 5913  df-on 5914  df-lim 5915  df-suc 5916  df-iota 6033  df-fun 6072  df-fn 6073  df-f 6074  df-f1 6075  df-fo 6076  df-f1o 6077  df-fv 6078  df-riota 6805  df-ov 6847  df-oprab 6848  df-mpt2 6849  df-om 7266  df-1st 7368  df-2nd 7369  df-wrecs 7612  df-recs 7674  df-rdg 7712  df-1o 7766  df-oadd 7770  df-er 7949  df-en 8163  df-dom 8164  df-sdom 8165  df-fin 8166  df-card 9018  df-cda 9245  df-pnf 10332  df-mnf 10333  df-xr 10334  df-ltxr 10335  df-le 10336  df-sub 10524  df-neg 10525  df-nn 11277  df-n0 11541  df-z 11627  df-uz 11890  df-fz 12537  df-hash 13325
This theorem is referenced by:  ramub1lem2  16013
  Copyright terms: Public domain W3C validator