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

Theorem ramub1lem1 15711
Description: Lemma for ramub1 15713. (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 3605 . . . . . . 7 (𝜑𝑉 ⊆ (𝑆 ∖ {𝑋}))
43difss2d 3732 . . . . . 6 (𝜑𝑉𝑆)
5 ramub1.x . . . . . . 7 (𝜑𝑋𝑆)
65snssd 4331 . . . . . 6 (𝜑 → {𝑋} ⊆ 𝑆)
74, 6unssd 3781 . . . . 5 (𝜑 → (𝑉 ∪ {𝑋}) ⊆ 𝑆)
8 ramub1.4 . . . . . 6 (𝜑𝑆 ∈ Fin)
9 elpw2g 4818 . . . . . 6 (𝑆 ∈ Fin → ((𝑉 ∪ {𝑋}) ∈ 𝒫 𝑆 ↔ (𝑉 ∪ {𝑋}) ⊆ 𝑆))
108, 9syl 17 . . . . 5 (𝜑 → ((𝑉 ∪ {𝑋}) ∈ 𝒫 𝑆 ↔ (𝑉 ∪ {𝑋}) ⊆ 𝑆))
117, 10mpbird 247 . . . 4 (𝜑 → (𝑉 ∪ {𝑋}) ∈ 𝒫 𝑆)
1211adantr 481 . . 3 ((𝜑𝐸 = 𝐷) → (𝑉 ∪ {𝑋}) ∈ 𝒫 𝑆)
13 iftrue 4083 . . . . . . 7 (𝐸 = 𝐷 → if(𝐸 = 𝐷, ((𝐹𝐷) − 1), (𝐹𝐸)) = ((𝐹𝐷) − 1))
1413adantl 482 . . . . . 6 ((𝜑𝐸 = 𝐷) → if(𝐸 = 𝐷, ((𝐹𝐷) − 1), (𝐹𝐸)) = ((𝐹𝐷) − 1))
15 ramub1.9 . . . . . . 7 (𝜑 → if(𝐸 = 𝐷, ((𝐹𝐷) − 1), (𝐹𝐸)) ≤ (#‘𝑉))
1615adantr 481 . . . . . 6 ((𝜑𝐸 = 𝐷) → if(𝐸 = 𝐷, ((𝐹𝐷) − 1), (𝐹𝐸)) ≤ (#‘𝑉))
1714, 16eqbrtrrd 4668 . . . . 5 ((𝜑𝐸 = 𝐷) → ((𝐹𝐷) − 1) ≤ (#‘𝑉))
18 ramub1.f . . . . . . . . 9 (𝜑𝐹:𝑅⟶ℕ)
19 ramub1.d . . . . . . . . 9 (𝜑𝐷𝑅)
2018, 19ffvelrnd 6346 . . . . . . . 8 (𝜑 → (𝐹𝐷) ∈ ℕ)
2120adantr 481 . . . . . . 7 ((𝜑𝐸 = 𝐷) → (𝐹𝐷) ∈ ℕ)
2221nnred 11020 . . . . . 6 ((𝜑𝐸 = 𝐷) → (𝐹𝐷) ∈ ℝ)
23 1red 10040 . . . . . 6 ((𝜑𝐸 = 𝐷) → 1 ∈ ℝ)
24 ssfi 8165 . . . . . . . . 9 ((𝑆 ∈ Fin ∧ 𝑉𝑆) → 𝑉 ∈ Fin)
258, 4, 24syl2anc 692 . . . . . . . 8 (𝜑𝑉 ∈ Fin)
26 hashcl 13130 . . . . . . . 8 (𝑉 ∈ Fin → (#‘𝑉) ∈ ℕ0)
27 nn0re 11286 . . . . . . . 8 ((#‘𝑉) ∈ ℕ0 → (#‘𝑉) ∈ ℝ)
2825, 26, 273syl 18 . . . . . . 7 (𝜑 → (#‘𝑉) ∈ ℝ)
2928adantr 481 . . . . . 6 ((𝜑𝐸 = 𝐷) → (#‘𝑉) ∈ ℝ)
3022, 23, 29lesubaddd 10609 . . . . 5 ((𝜑𝐸 = 𝐷) → (((𝐹𝐷) − 1) ≤ (#‘𝑉) ↔ (𝐹𝐷) ≤ ((#‘𝑉) + 1)))
3117, 30mpbid 222 . . . 4 ((𝜑𝐸 = 𝐷) → (𝐹𝐷) ≤ ((#‘𝑉) + 1))
32 fveq2 6178 . . . . 5 (𝐸 = 𝐷 → (𝐹𝐸) = (𝐹𝐷))
33 snidg 4197 . . . . . . . 8 (𝑋𝑆𝑋 ∈ {𝑋})
345, 33syl 17 . . . . . . 7 (𝜑𝑋 ∈ {𝑋})
353sseld 3594 . . . . . . . 8 (𝜑 → (𝑋𝑉𝑋 ∈ (𝑆 ∖ {𝑋})))
36 eldifn 3725 . . . . . . . 8 (𝑋 ∈ (𝑆 ∖ {𝑋}) → ¬ 𝑋 ∈ {𝑋})
3735, 36syl6 35 . . . . . . 7 (𝜑 → (𝑋𝑉 → ¬ 𝑋 ∈ {𝑋}))
3834, 37mt2d 131 . . . . . 6 (𝜑 → ¬ 𝑋𝑉)
39 hashunsng 13164 . . . . . . 7 (𝑋𝑆 → ((𝑉 ∈ Fin ∧ ¬ 𝑋𝑉) → (#‘(𝑉 ∪ {𝑋})) = ((#‘𝑉) + 1)))
405, 39syl 17 . . . . . 6 (𝜑 → ((𝑉 ∈ Fin ∧ ¬ 𝑋𝑉) → (#‘(𝑉 ∪ {𝑋})) = ((#‘𝑉) + 1)))
4125, 38, 40mp2and 714 . . . . 5 (𝜑 → (#‘(𝑉 ∪ {𝑋})) = ((#‘𝑉) + 1))
4232, 41breqan12rd 4661 . . . 4 ((𝜑𝐸 = 𝐷) → ((𝐹𝐸) ≤ (#‘(𝑉 ∪ {𝑋})) ↔ (𝐹𝐷) ≤ ((#‘𝑉) + 1)))
4331, 42mpbird 247 . . 3 ((𝜑𝐸 = 𝐷) → (𝐹𝐸) ≤ (#‘(𝑉 ∪ {𝑋})))
44 snfi 8023 . . . . . . 7 {𝑋} ∈ Fin
45 unfi 8212 . . . . . . 7 ((𝑉 ∈ Fin ∧ {𝑋} ∈ Fin) → (𝑉 ∪ {𝑋}) ∈ Fin)
4625, 44, 45sylancl 693 . . . . . 6 (𝜑 → (𝑉 ∪ {𝑋}) ∈ Fin)
47 ramub1.m . . . . . . 7 (𝜑𝑀 ∈ ℕ)
4847nnnn0d 11336 . . . . . 6 (𝜑𝑀 ∈ ℕ0)
49 ramub1.3 . . . . . . 7 𝐶 = (𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (#‘𝑏) = 𝑖})
5049hashbcval 15687 . . . . . 6 (((𝑉 ∪ {𝑋}) ∈ Fin ∧ 𝑀 ∈ ℕ0) → ((𝑉 ∪ {𝑋})𝐶𝑀) = {𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∣ (#‘𝑥) = 𝑀})
5146, 48, 50syl2anc 692 . . . . 5 (𝜑 → ((𝑉 ∪ {𝑋})𝐶𝑀) = {𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∣ (#‘𝑥) = 𝑀})
5251adantr 481 . . . 4 ((𝜑𝐸 = 𝐷) → ((𝑉 ∪ {𝑋})𝐶𝑀) = {𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∣ (#‘𝑥) = 𝑀})
53 simpl1l 1110 . . . . . . . 8 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (#‘𝑥) = 𝑀) ∧ 𝑥 ∈ 𝒫 𝑉) → 𝜑)
5449hashbcval 15687 . . . . . . . . . 10 ((𝑉 ∈ Fin ∧ 𝑀 ∈ ℕ0) → (𝑉𝐶𝑀) = {𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 𝑀})
5525, 48, 54syl2anc 692 . . . . . . . . 9 (𝜑 → (𝑉𝐶𝑀) = {𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 𝑀})
56 ramub1.s . . . . . . . . 9 (𝜑 → (𝑉𝐶𝑀) ⊆ (𝐾 “ {𝐸}))
5755, 56eqsstr3d 3632 . . . . . . . 8 (𝜑 → {𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 𝑀} ⊆ (𝐾 “ {𝐸}))
5853, 57syl 17 . . . . . . 7 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (#‘𝑥) = 𝑀) ∧ 𝑥 ∈ 𝒫 𝑉) → {𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 𝑀} ⊆ (𝐾 “ {𝐸}))
59 simpr 477 . . . . . . . 8 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (#‘𝑥) = 𝑀) ∧ 𝑥 ∈ 𝒫 𝑉) → 𝑥 ∈ 𝒫 𝑉)
60 simpl3 1064 . . . . . . . 8 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (#‘𝑥) = 𝑀) ∧ 𝑥 ∈ 𝒫 𝑉) → (#‘𝑥) = 𝑀)
61 rabid 3111 . . . . . . . 8 (𝑥 ∈ {𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 𝑀} ↔ (𝑥 ∈ 𝒫 𝑉 ∧ (#‘𝑥) = 𝑀))
6259, 60, 61sylanbrc 697 . . . . . . 7 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (#‘𝑥) = 𝑀) ∧ 𝑥 ∈ 𝒫 𝑉) → 𝑥 ∈ {𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 𝑀})
6358, 62sseldd 3596 . . . . . 6 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (#‘𝑥) = 𝑀) ∧ 𝑥 ∈ 𝒫 𝑉) → 𝑥 ∈ (𝐾 “ {𝐸}))
64 simpl2 1063 . . . . . . . . . . . 12 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (#‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}))
6564elpwid 4161 . . . . . . . . . . 11 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (#‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → 𝑥 ⊆ (𝑉 ∪ {𝑋}))
66 simpl1l 1110 . . . . . . . . . . . 12 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (#‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → 𝜑)
6766, 7syl 17 . . . . . . . . . . 11 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (#‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → (𝑉 ∪ {𝑋}) ⊆ 𝑆)
6865, 67sstrd 3605 . . . . . . . . . 10 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (#‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → 𝑥𝑆)
69 vex 3198 . . . . . . . . . . 11 𝑥 ∈ V
7069elpw 4155 . . . . . . . . . 10 (𝑥 ∈ 𝒫 𝑆𝑥𝑆)
7168, 70sylibr 224 . . . . . . . . 9 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (#‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → 𝑥 ∈ 𝒫 𝑆)
72 simpl3 1064 . . . . . . . . 9 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (#‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → (#‘𝑥) = 𝑀)
73 rabid 3111 . . . . . . . . 9 (𝑥 ∈ {𝑥 ∈ 𝒫 𝑆 ∣ (#‘𝑥) = 𝑀} ↔ (𝑥 ∈ 𝒫 𝑆 ∧ (#‘𝑥) = 𝑀))
7471, 72, 73sylanbrc 697 . . . . . . . 8 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (#‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → 𝑥 ∈ {𝑥 ∈ 𝒫 𝑆 ∣ (#‘𝑥) = 𝑀})
7549hashbcval 15687 . . . . . . . . . 10 ((𝑆 ∈ Fin ∧ 𝑀 ∈ ℕ0) → (𝑆𝐶𝑀) = {𝑥 ∈ 𝒫 𝑆 ∣ (#‘𝑥) = 𝑀})
768, 48, 75syl2anc 692 . . . . . . . . 9 (𝜑 → (𝑆𝐶𝑀) = {𝑥 ∈ 𝒫 𝑆 ∣ (#‘𝑥) = 𝑀})
7766, 76syl 17 . . . . . . . 8 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (#‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → (𝑆𝐶𝑀) = {𝑥 ∈ 𝒫 𝑆 ∣ (#‘𝑥) = 𝑀})
7874, 77eleqtrrd 2702 . . . . . . 7 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (#‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → 𝑥 ∈ (𝑆𝐶𝑀))
792difss2d 3732 . . . . . . . . . . . . . . 15 (𝜑𝑊𝑆)
80 ssfi 8165 . . . . . . . . . . . . . . 15 ((𝑆 ∈ Fin ∧ 𝑊𝑆) → 𝑊 ∈ Fin)
818, 79, 80syl2anc 692 . . . . . . . . . . . . . 14 (𝜑𝑊 ∈ Fin)
82 nnm1nn0 11319 . . . . . . . . . . . . . . 15 (𝑀 ∈ ℕ → (𝑀 − 1) ∈ ℕ0)
8347, 82syl 17 . . . . . . . . . . . . . 14 (𝜑 → (𝑀 − 1) ∈ ℕ0)
8449hashbcval 15687 . . . . . . . . . . . . . 14 ((𝑊 ∈ Fin ∧ (𝑀 − 1) ∈ ℕ0) → (𝑊𝐶(𝑀 − 1)) = {𝑢 ∈ 𝒫 𝑊 ∣ (#‘𝑢) = (𝑀 − 1)})
8581, 83, 84syl2anc 692 . . . . . . . . . . . . 13 (𝜑 → (𝑊𝐶(𝑀 − 1)) = {𝑢 ∈ 𝒫 𝑊 ∣ (#‘𝑢) = (𝑀 − 1)})
86 ramub1.8 . . . . . . . . . . . . 13 (𝜑 → (𝑊𝐶(𝑀 − 1)) ⊆ (𝐻 “ {𝐷}))
8785, 86eqsstr3d 3632 . . . . . . . . . . . 12 (𝜑 → {𝑢 ∈ 𝒫 𝑊 ∣ (#‘𝑢) = (𝑀 − 1)} ⊆ (𝐻 “ {𝐷}))
8866, 87syl 17 . . . . . . . . . . 11 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (#‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → {𝑢 ∈ 𝒫 𝑊 ∣ (#‘𝑢) = (𝑀 − 1)} ⊆ (𝐻 “ {𝐷}))
89 uncom 3749 . . . . . . . . . . . . . . . 16 (𝑉 ∪ {𝑋}) = ({𝑋} ∪ 𝑉)
9065, 89syl6sseq 3643 . . . . . . . . . . . . . . 15 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (#‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → 𝑥 ⊆ ({𝑋} ∪ 𝑉))
91 ssundif 4043 . . . . . . . . . . . . . . 15 (𝑥 ⊆ ({𝑋} ∪ 𝑉) ↔ (𝑥 ∖ {𝑋}) ⊆ 𝑉)
9290, 91sylib 208 . . . . . . . . . . . . . 14 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (#‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → (𝑥 ∖ {𝑋}) ⊆ 𝑉)
9366, 1syl 17 . . . . . . . . . . . . . 14 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (#‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → 𝑉𝑊)
9492, 93sstrd 3605 . . . . . . . . . . . . 13 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (#‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → (𝑥 ∖ {𝑋}) ⊆ 𝑊)
95 difexg 4799 . . . . . . . . . . . . . . 15 (𝑥 ∈ V → (𝑥 ∖ {𝑋}) ∈ V)
9669, 95ax-mp 5 . . . . . . . . . . . . . 14 (𝑥 ∖ {𝑋}) ∈ V
9796elpw 4155 . . . . . . . . . . . . 13 ((𝑥 ∖ {𝑋}) ∈ 𝒫 𝑊 ↔ (𝑥 ∖ {𝑋}) ⊆ 𝑊)
9894, 97sylibr 224 . . . . . . . . . . . 12 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (#‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → (𝑥 ∖ {𝑋}) ∈ 𝒫 𝑊)
9966, 8syl 17 . . . . . . . . . . . . . . . . 17 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (#‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → 𝑆 ∈ Fin)
100 ssfi 8165 . . . . . . . . . . . . . . . . 17 ((𝑆 ∈ Fin ∧ 𝑥𝑆) → 𝑥 ∈ Fin)
10199, 68, 100syl2anc 692 . . . . . . . . . . . . . . . 16 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (#‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → 𝑥 ∈ Fin)
102 diffi 8177 . . . . . . . . . . . . . . . 16 (𝑥 ∈ Fin → (𝑥 ∖ {𝑋}) ∈ Fin)
103101, 102syl 17 . . . . . . . . . . . . . . 15 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (#‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → (𝑥 ∖ {𝑋}) ∈ Fin)
104 hashcl 13130 . . . . . . . . . . . . . . 15 ((𝑥 ∖ {𝑋}) ∈ Fin → (#‘(𝑥 ∖ {𝑋})) ∈ ℕ0)
105 nn0cn 11287 . . . . . . . . . . . . . . 15 ((#‘(𝑥 ∖ {𝑋})) ∈ ℕ0 → (#‘(𝑥 ∖ {𝑋})) ∈ ℂ)
106103, 104, 1053syl 18 . . . . . . . . . . . . . 14 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (#‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → (#‘(𝑥 ∖ {𝑋})) ∈ ℂ)
107 ax-1cn 9979 . . . . . . . . . . . . . 14 1 ∈ ℂ
108 pncan 10272 . . . . . . . . . . . . . 14 (((#‘(𝑥 ∖ {𝑋})) ∈ ℂ ∧ 1 ∈ ℂ) → (((#‘(𝑥 ∖ {𝑋})) + 1) − 1) = (#‘(𝑥 ∖ {𝑋})))
109106, 107, 108sylancl 693 . . . . . . . . . . . . 13 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (#‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → (((#‘(𝑥 ∖ {𝑋})) + 1) − 1) = (#‘(𝑥 ∖ {𝑋})))
110 neldifsnd 4313 . . . . . . . . . . . . . . . 16 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (#‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → ¬ 𝑋 ∈ (𝑥 ∖ {𝑋}))
111 hashunsng 13164 . . . . . . . . . . . . . . . . 17 (𝑋𝑆 → (((𝑥 ∖ {𝑋}) ∈ Fin ∧ ¬ 𝑋 ∈ (𝑥 ∖ {𝑋})) → (#‘((𝑥 ∖ {𝑋}) ∪ {𝑋})) = ((#‘(𝑥 ∖ {𝑋})) + 1)))
11266, 5, 1113syl 18 . . . . . . . . . . . . . . . 16 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (#‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → (((𝑥 ∖ {𝑋}) ∈ Fin ∧ ¬ 𝑋 ∈ (𝑥 ∖ {𝑋})) → (#‘((𝑥 ∖ {𝑋}) ∪ {𝑋})) = ((#‘(𝑥 ∖ {𝑋})) + 1)))
113103, 110, 112mp2and 714 . . . . . . . . . . . . . . 15 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (#‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → (#‘((𝑥 ∖ {𝑋}) ∪ {𝑋})) = ((#‘(𝑥 ∖ {𝑋})) + 1))
114 undif1 4034 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∖ {𝑋}) ∪ {𝑋}) = (𝑥 ∪ {𝑋})
115 simpr 477 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (#‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → ¬ 𝑥 ∈ 𝒫 𝑉)
11664, 115eldifd 3578 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (#‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → 𝑥 ∈ (𝒫 (𝑉 ∪ {𝑋}) ∖ 𝒫 𝑉))
117 elpwunsn 4215 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ (𝒫 (𝑉 ∪ {𝑋}) ∖ 𝒫 𝑉) → 𝑋𝑥)
118116, 117syl 17 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (#‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → 𝑋𝑥)
119118snssd 4331 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (#‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → {𝑋} ⊆ 𝑥)
120 ssequn2 3778 . . . . . . . . . . . . . . . . . . 19 ({𝑋} ⊆ 𝑥 ↔ (𝑥 ∪ {𝑋}) = 𝑥)
121119, 120sylib 208 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (#‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → (𝑥 ∪ {𝑋}) = 𝑥)
122114, 121syl5req 2667 . . . . . . . . . . . . . . . . 17 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (#‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → 𝑥 = ((𝑥 ∖ {𝑋}) ∪ {𝑋}))
123122fveq2d 6182 . . . . . . . . . . . . . . . 16 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (#‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → (#‘𝑥) = (#‘((𝑥 ∖ {𝑋}) ∪ {𝑋})))
124123, 72eqtr3d 2656 . . . . . . . . . . . . . . 15 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (#‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → (#‘((𝑥 ∖ {𝑋}) ∪ {𝑋})) = 𝑀)
125113, 124eqtr3d 2656 . . . . . . . . . . . . . 14 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (#‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → ((#‘(𝑥 ∖ {𝑋})) + 1) = 𝑀)
126125oveq1d 6650 . . . . . . . . . . . . 13 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (#‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → (((#‘(𝑥 ∖ {𝑋})) + 1) − 1) = (𝑀 − 1))
127109, 126eqtr3d 2656 . . . . . . . . . . . 12 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (#‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → (#‘(𝑥 ∖ {𝑋})) = (𝑀 − 1))
128 fveq2 6178 . . . . . . . . . . . . . 14 (𝑢 = (𝑥 ∖ {𝑋}) → (#‘𝑢) = (#‘(𝑥 ∖ {𝑋})))
129128eqeq1d 2622 . . . . . . . . . . . . 13 (𝑢 = (𝑥 ∖ {𝑋}) → ((#‘𝑢) = (𝑀 − 1) ↔ (#‘(𝑥 ∖ {𝑋})) = (𝑀 − 1)))
130129elrab 3357 . . . . . . . . . . . 12 ((𝑥 ∖ {𝑋}) ∈ {𝑢 ∈ 𝒫 𝑊 ∣ (#‘𝑢) = (𝑀 − 1)} ↔ ((𝑥 ∖ {𝑋}) ∈ 𝒫 𝑊 ∧ (#‘(𝑥 ∖ {𝑋})) = (𝑀 − 1)))
13198, 127, 130sylanbrc 697 . . . . . . . . . . 11 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (#‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → (𝑥 ∖ {𝑋}) ∈ {𝑢 ∈ 𝒫 𝑊 ∣ (#‘𝑢) = (𝑀 − 1)})
13288, 131sseldd 3596 . . . . . . . . . 10 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (#‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → (𝑥 ∖ {𝑋}) ∈ (𝐻 “ {𝐷}))
133 ramub1.h . . . . . . . . . . . 12 𝐻 = (𝑢 ∈ ((𝑆 ∖ {𝑋})𝐶(𝑀 − 1)) ↦ (𝐾‘(𝑢 ∪ {𝑋})))
134133mptiniseg 5617 . . . . . . . . . . 11 (𝐷𝑅 → (𝐻 “ {𝐷}) = {𝑢 ∈ ((𝑆 ∖ {𝑋})𝐶(𝑀 − 1)) ∣ (𝐾‘(𝑢 ∪ {𝑋})) = 𝐷})
13566, 19, 1343syl 18 . . . . . . . . . 10 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (#‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → (𝐻 “ {𝐷}) = {𝑢 ∈ ((𝑆 ∖ {𝑋})𝐶(𝑀 − 1)) ∣ (𝐾‘(𝑢 ∪ {𝑋})) = 𝐷})
136132, 135eleqtrd 2701 . . . . . . . . 9 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (#‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → (𝑥 ∖ {𝑋}) ∈ {𝑢 ∈ ((𝑆 ∖ {𝑋})𝐶(𝑀 − 1)) ∣ (𝐾‘(𝑢 ∪ {𝑋})) = 𝐷})
137 uneq1 3752 . . . . . . . . . . . . 13 (𝑢 = (𝑥 ∖ {𝑋}) → (𝑢 ∪ {𝑋}) = ((𝑥 ∖ {𝑋}) ∪ {𝑋}))
138137fveq2d 6182 . . . . . . . . . . . 12 (𝑢 = (𝑥 ∖ {𝑋}) → (𝐾‘(𝑢 ∪ {𝑋})) = (𝐾‘((𝑥 ∖ {𝑋}) ∪ {𝑋})))
139138eqeq1d 2622 . . . . . . . . . . 11 (𝑢 = (𝑥 ∖ {𝑋}) → ((𝐾‘(𝑢 ∪ {𝑋})) = 𝐷 ↔ (𝐾‘((𝑥 ∖ {𝑋}) ∪ {𝑋})) = 𝐷))
140139elrab 3357 . . . . . . . . . 10 ((𝑥 ∖ {𝑋}) ∈ {𝑢 ∈ ((𝑆 ∖ {𝑋})𝐶(𝑀 − 1)) ∣ (𝐾‘(𝑢 ∪ {𝑋})) = 𝐷} ↔ ((𝑥 ∖ {𝑋}) ∈ ((𝑆 ∖ {𝑋})𝐶(𝑀 − 1)) ∧ (𝐾‘((𝑥 ∖ {𝑋}) ∪ {𝑋})) = 𝐷))
141140simprbi 480 . . . . . . . . 9 ((𝑥 ∖ {𝑋}) ∈ {𝑢 ∈ ((𝑆 ∖ {𝑋})𝐶(𝑀 − 1)) ∣ (𝐾‘(𝑢 ∪ {𝑋})) = 𝐷} → (𝐾‘((𝑥 ∖ {𝑋}) ∪ {𝑋})) = 𝐷)
142136, 141syl 17 . . . . . . . 8 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (#‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → (𝐾‘((𝑥 ∖ {𝑋}) ∪ {𝑋})) = 𝐷)
143122fveq2d 6182 . . . . . . . 8 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (#‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → (𝐾𝑥) = (𝐾‘((𝑥 ∖ {𝑋}) ∪ {𝑋})))
144 simpl1r 1111 . . . . . . . 8 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (#‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → 𝐸 = 𝐷)
145142, 143, 1443eqtr4d 2664 . . . . . . 7 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (#‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → (𝐾𝑥) = 𝐸)
146 ramub1.6 . . . . . . . . 9 (𝜑𝐾:(𝑆𝐶𝑀)⟶𝑅)
147 ffn 6032 . . . . . . . . 9 (𝐾:(𝑆𝐶𝑀)⟶𝑅𝐾 Fn (𝑆𝐶𝑀))
148146, 147syl 17 . . . . . . . 8 (𝜑𝐾 Fn (𝑆𝐶𝑀))
149 fniniseg 6324 . . . . . . . 8 (𝐾 Fn (𝑆𝐶𝑀) → (𝑥 ∈ (𝐾 “ {𝐸}) ↔ (𝑥 ∈ (𝑆𝐶𝑀) ∧ (𝐾𝑥) = 𝐸)))
15066, 148, 1493syl 18 . . . . . . 7 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (#‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → (𝑥 ∈ (𝐾 “ {𝐸}) ↔ (𝑥 ∈ (𝑆𝐶𝑀) ∧ (𝐾𝑥) = 𝐸)))
15178, 145, 150mpbir2and 956 . . . . . 6 ((((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (#‘𝑥) = 𝑀) ∧ ¬ 𝑥 ∈ 𝒫 𝑉) → 𝑥 ∈ (𝐾 “ {𝐸}))
15263, 151pm2.61dan 831 . . . . 5 (((𝜑𝐸 = 𝐷) ∧ 𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∧ (#‘𝑥) = 𝑀) → 𝑥 ∈ (𝐾 “ {𝐸}))
153152rabssdv 3674 . . . 4 ((𝜑𝐸 = 𝐷) → {𝑥 ∈ 𝒫 (𝑉 ∪ {𝑋}) ∣ (#‘𝑥) = 𝑀} ⊆ (𝐾 “ {𝐸}))
15452, 153eqsstrd 3631 . . 3 ((𝜑𝐸 = 𝐷) → ((𝑉 ∪ {𝑋})𝐶𝑀) ⊆ (𝐾 “ {𝐸}))
155 fveq2 6178 . . . . . 6 (𝑧 = (𝑉 ∪ {𝑋}) → (#‘𝑧) = (#‘(𝑉 ∪ {𝑋})))
156155breq2d 4656 . . . . 5 (𝑧 = (𝑉 ∪ {𝑋}) → ((𝐹𝐸) ≤ (#‘𝑧) ↔ (𝐹𝐸) ≤ (#‘(𝑉 ∪ {𝑋}))))
157 oveq1 6642 . . . . . 6 (𝑧 = (𝑉 ∪ {𝑋}) → (𝑧𝐶𝑀) = ((𝑉 ∪ {𝑋})𝐶𝑀))
158157sseq1d 3624 . . . . 5 (𝑧 = (𝑉 ∪ {𝑋}) → ((𝑧𝐶𝑀) ⊆ (𝐾 “ {𝐸}) ↔ ((𝑉 ∪ {𝑋})𝐶𝑀) ⊆ (𝐾 “ {𝐸})))
159156, 158anbi12d 746 . . . 4 (𝑧 = (𝑉 ∪ {𝑋}) → (((𝐹𝐸) ≤ (#‘𝑧) ∧ (𝑧𝐶𝑀) ⊆ (𝐾 “ {𝐸})) ↔ ((𝐹𝐸) ≤ (#‘(𝑉 ∪ {𝑋})) ∧ ((𝑉 ∪ {𝑋})𝐶𝑀) ⊆ (𝐾 “ {𝐸}))))
160159rspcev 3304 . . 3 (((𝑉 ∪ {𝑋}) ∈ 𝒫 𝑆 ∧ ((𝐹𝐸) ≤ (#‘(𝑉 ∪ {𝑋})) ∧ ((𝑉 ∪ {𝑋})𝐶𝑀) ⊆ (𝐾 “ {𝐸}))) → ∃𝑧 ∈ 𝒫 𝑆((𝐹𝐸) ≤ (#‘𝑧) ∧ (𝑧𝐶𝑀) ⊆ (𝐾 “ {𝐸})))
16112, 43, 154, 160syl12anc 1322 . 2 ((𝜑𝐸 = 𝐷) → ∃𝑧 ∈ 𝒫 𝑆((𝐹𝐸) ≤ (#‘𝑧) ∧ (𝑧𝐶𝑀) ⊆ (𝐾 “ {𝐸})))
162 elpw2g 4818 . . . . . 6 (𝑆 ∈ Fin → (𝑉 ∈ 𝒫 𝑆𝑉𝑆))
1638, 162syl 17 . . . . 5 (𝜑 → (𝑉 ∈ 𝒫 𝑆𝑉𝑆))
1644, 163mpbird 247 . . . 4 (𝜑𝑉 ∈ 𝒫 𝑆)
165164adantr 481 . . 3 ((𝜑𝐸𝐷) → 𝑉 ∈ 𝒫 𝑆)
166 ifnefalse 4089 . . . . 5 (𝐸𝐷 → if(𝐸 = 𝐷, ((𝐹𝐷) − 1), (𝐹𝐸)) = (𝐹𝐸))
167166adantl 482 . . . 4 ((𝜑𝐸𝐷) → if(𝐸 = 𝐷, ((𝐹𝐷) − 1), (𝐹𝐸)) = (𝐹𝐸))
16815adantr 481 . . . 4 ((𝜑𝐸𝐷) → if(𝐸 = 𝐷, ((𝐹𝐷) − 1), (𝐹𝐸)) ≤ (#‘𝑉))
169167, 168eqbrtrrd 4668 . . 3 ((𝜑𝐸𝐷) → (𝐹𝐸) ≤ (#‘𝑉))
17056adantr 481 . . 3 ((𝜑𝐸𝐷) → (𝑉𝐶𝑀) ⊆ (𝐾 “ {𝐸}))
171 fveq2 6178 . . . . . 6 (𝑧 = 𝑉 → (#‘𝑧) = (#‘𝑉))
172171breq2d 4656 . . . . 5 (𝑧 = 𝑉 → ((𝐹𝐸) ≤ (#‘𝑧) ↔ (𝐹𝐸) ≤ (#‘𝑉)))
173 oveq1 6642 . . . . . 6 (𝑧 = 𝑉 → (𝑧𝐶𝑀) = (𝑉𝐶𝑀))
174173sseq1d 3624 . . . . 5 (𝑧 = 𝑉 → ((𝑧𝐶𝑀) ⊆ (𝐾 “ {𝐸}) ↔ (𝑉𝐶𝑀) ⊆ (𝐾 “ {𝐸})))
175172, 174anbi12d 746 . . . 4 (𝑧 = 𝑉 → (((𝐹𝐸) ≤ (#‘𝑧) ∧ (𝑧𝐶𝑀) ⊆ (𝐾 “ {𝐸})) ↔ ((𝐹𝐸) ≤ (#‘𝑉) ∧ (𝑉𝐶𝑀) ⊆ (𝐾 “ {𝐸}))))
176175rspcev 3304 . . 3 ((𝑉 ∈ 𝒫 𝑆 ∧ ((𝐹𝐸) ≤ (#‘𝑉) ∧ (𝑉𝐶𝑀) ⊆ (𝐾 “ {𝐸}))) → ∃𝑧 ∈ 𝒫 𝑆((𝐹𝐸) ≤ (#‘𝑧) ∧ (𝑧𝐶𝑀) ⊆ (𝐾 “ {𝐸})))
177165, 169, 170, 176syl12anc 1322 . 2 ((𝜑𝐸𝐷) → ∃𝑧 ∈ 𝒫 𝑆((𝐹𝐸) ≤ (#‘𝑧) ∧ (𝑧𝐶𝑀) ⊆ (𝐾 “ {𝐸})))
178161, 177pm2.61dane 2878 1 (𝜑 → ∃𝑧 ∈ 𝒫 𝑆((𝐹𝐸) ≤ (#‘𝑧) ∧ (𝑧𝐶𝑀) ⊆ (𝐾 “ {𝐸})))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 384  w3a 1036   = wceq 1481  wcel 1988  wne 2791  wrex 2910  {crab 2913  Vcvv 3195  cdif 3564  cun 3565  wss 3567  ifcif 4077  𝒫 cpw 4149  {csn 4168   class class class wbr 4644  cmpt 4720  ccnv 5103  cima 5107   Fn wfn 5871  wf 5872  cfv 5876  (class class class)co 6635  cmpt2 6637  Fincfn 7940  cc 9919  cr 9920  1c1 9922   + caddc 9924  cle 10060  cmin 10251  cn 11005  0cn0 11277  #chash 13100   Ramsey cram 15684
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-8 1990  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-rep 4762  ax-sep 4772  ax-nul 4780  ax-pow 4834  ax-pr 4897  ax-un 6934  ax-cnex 9977  ax-resscn 9978  ax-1cn 9979  ax-icn 9980  ax-addcl 9981  ax-addrcl 9982  ax-mulcl 9983  ax-mulrcl 9984  ax-mulcom 9985  ax-addass 9986  ax-mulass 9987  ax-distr 9988  ax-i2m1 9989  ax-1ne0 9990  ax-1rid 9991  ax-rnegex 9992  ax-rrecex 9993  ax-cnre 9994  ax-pre-lttri 9995  ax-pre-lttrn 9996  ax-pre-ltadd 9997  ax-pre-mulgt0 9998
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-eu 2472  df-mo 2473  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ne 2792  df-nel 2895  df-ral 2914  df-rex 2915  df-reu 2916  df-rmo 2917  df-rab 2918  df-v 3197  df-sbc 3430  df-csb 3527  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-pss 3583  df-nul 3908  df-if 4078  df-pw 4151  df-sn 4169  df-pr 4171  df-tp 4173  df-op 4175  df-uni 4428  df-int 4467  df-iun 4513  df-br 4645  df-opab 4704  df-mpt 4721  df-tr 4744  df-id 5014  df-eprel 5019  df-po 5025  df-so 5026  df-fr 5063  df-we 5065  df-xp 5110  df-rel 5111  df-cnv 5112  df-co 5113  df-dm 5114  df-rn 5115  df-res 5116  df-ima 5117  df-pred 5668  df-ord 5714  df-on 5715  df-lim 5716  df-suc 5717  df-iota 5839  df-fun 5878  df-fn 5879  df-f 5880  df-f1 5881  df-fo 5882  df-f1o 5883  df-fv 5884  df-riota 6596  df-ov 6638  df-oprab 6639  df-mpt2 6640  df-om 7051  df-1st 7153  df-2nd 7154  df-wrecs 7392  df-recs 7453  df-rdg 7491  df-1o 7545  df-oadd 7549  df-er 7727  df-en 7941  df-dom 7942  df-sdom 7943  df-fin 7944  df-card 8750  df-cda 8975  df-pnf 10061  df-mnf 10062  df-xr 10063  df-ltxr 10064  df-le 10065  df-sub 10253  df-neg 10254  df-nn 11006  df-n0 11278  df-z 11363  df-uz 11673  df-fz 12312  df-hash 13101
This theorem is referenced by:  ramub1lem2  15712
  Copyright terms: Public domain W3C validator