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

Theorem ramub1lem1 16959
Description: Lemma for ramub1 16961. (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.4 . . . . 5 (πœ‘ β†’ 𝑆 ∈ Fin)
2 ramub1.v . . . . . . . 8 (πœ‘ β†’ 𝑉 βŠ† π‘Š)
3 ramub1.w . . . . . . . 8 (πœ‘ β†’ π‘Š βŠ† (𝑆 βˆ– {𝑋}))
42, 3sstrd 3993 . . . . . . 7 (πœ‘ β†’ 𝑉 βŠ† (𝑆 βˆ– {𝑋}))
54difss2d 4135 . . . . . 6 (πœ‘ β†’ 𝑉 βŠ† 𝑆)
6 ramub1.x . . . . . . 7 (πœ‘ β†’ 𝑋 ∈ 𝑆)
76snssd 4813 . . . . . 6 (πœ‘ β†’ {𝑋} βŠ† 𝑆)
85, 7unssd 4187 . . . . 5 (πœ‘ β†’ (𝑉 βˆͺ {𝑋}) βŠ† 𝑆)
91, 8sselpwd 5327 . . . 4 (πœ‘ β†’ (𝑉 βˆͺ {𝑋}) ∈ 𝒫 𝑆)
109adantr 482 . . 3 ((πœ‘ ∧ 𝐸 = 𝐷) β†’ (𝑉 βˆͺ {𝑋}) ∈ 𝒫 𝑆)
11 iftrue 4535 . . . . . . 7 (𝐸 = 𝐷 β†’ if(𝐸 = 𝐷, ((πΉβ€˜π·) βˆ’ 1), (πΉβ€˜πΈ)) = ((πΉβ€˜π·) βˆ’ 1))
1211adantl 483 . . . . . 6 ((πœ‘ ∧ 𝐸 = 𝐷) β†’ if(𝐸 = 𝐷, ((πΉβ€˜π·) βˆ’ 1), (πΉβ€˜πΈ)) = ((πΉβ€˜π·) βˆ’ 1))
13 ramub1.9 . . . . . . 7 (πœ‘ β†’ if(𝐸 = 𝐷, ((πΉβ€˜π·) βˆ’ 1), (πΉβ€˜πΈ)) ≀ (β™―β€˜π‘‰))
1413adantr 482 . . . . . 6 ((πœ‘ ∧ 𝐸 = 𝐷) β†’ if(𝐸 = 𝐷, ((πΉβ€˜π·) βˆ’ 1), (πΉβ€˜πΈ)) ≀ (β™―β€˜π‘‰))
1512, 14eqbrtrrd 5173 . . . . 5 ((πœ‘ ∧ 𝐸 = 𝐷) β†’ ((πΉβ€˜π·) βˆ’ 1) ≀ (β™―β€˜π‘‰))
16 ramub1.f . . . . . . . . 9 (πœ‘ β†’ 𝐹:π‘…βŸΆβ„•)
17 ramub1.d . . . . . . . . 9 (πœ‘ β†’ 𝐷 ∈ 𝑅)
1816, 17ffvelcdmd 7088 . . . . . . . 8 (πœ‘ β†’ (πΉβ€˜π·) ∈ β„•)
1918adantr 482 . . . . . . 7 ((πœ‘ ∧ 𝐸 = 𝐷) β†’ (πΉβ€˜π·) ∈ β„•)
2019nnred 12227 . . . . . 6 ((πœ‘ ∧ 𝐸 = 𝐷) β†’ (πΉβ€˜π·) ∈ ℝ)
21 1red 11215 . . . . . 6 ((πœ‘ ∧ 𝐸 = 𝐷) β†’ 1 ∈ ℝ)
221, 5ssfid 9267 . . . . . . . 8 (πœ‘ β†’ 𝑉 ∈ Fin)
23 hashcl 14316 . . . . . . . 8 (𝑉 ∈ Fin β†’ (β™―β€˜π‘‰) ∈ β„•0)
24 nn0re 12481 . . . . . . . 8 ((β™―β€˜π‘‰) ∈ β„•0 β†’ (β™―β€˜π‘‰) ∈ ℝ)
2522, 23, 243syl 18 . . . . . . 7 (πœ‘ β†’ (β™―β€˜π‘‰) ∈ ℝ)
2625adantr 482 . . . . . 6 ((πœ‘ ∧ 𝐸 = 𝐷) β†’ (β™―β€˜π‘‰) ∈ ℝ)
2720, 21, 26lesubaddd 11811 . . . . 5 ((πœ‘ ∧ 𝐸 = 𝐷) β†’ (((πΉβ€˜π·) βˆ’ 1) ≀ (β™―β€˜π‘‰) ↔ (πΉβ€˜π·) ≀ ((β™―β€˜π‘‰) + 1)))
2815, 27mpbid 231 . . . 4 ((πœ‘ ∧ 𝐸 = 𝐷) β†’ (πΉβ€˜π·) ≀ ((β™―β€˜π‘‰) + 1))
29 fveq2 6892 . . . . 5 (𝐸 = 𝐷 β†’ (πΉβ€˜πΈ) = (πΉβ€˜π·))
30 snidg 4663 . . . . . . . 8 (𝑋 ∈ 𝑆 β†’ 𝑋 ∈ {𝑋})
316, 30syl 17 . . . . . . 7 (πœ‘ β†’ 𝑋 ∈ {𝑋})
324sseld 3982 . . . . . . . 8 (πœ‘ β†’ (𝑋 ∈ 𝑉 β†’ 𝑋 ∈ (𝑆 βˆ– {𝑋})))
33 eldifn 4128 . . . . . . . 8 (𝑋 ∈ (𝑆 βˆ– {𝑋}) β†’ Β¬ 𝑋 ∈ {𝑋})
3432, 33syl6 35 . . . . . . 7 (πœ‘ β†’ (𝑋 ∈ 𝑉 β†’ Β¬ 𝑋 ∈ {𝑋}))
3531, 34mt2d 136 . . . . . 6 (πœ‘ β†’ Β¬ 𝑋 ∈ 𝑉)
36 hashunsng 14352 . . . . . . 7 (𝑋 ∈ 𝑆 β†’ ((𝑉 ∈ Fin ∧ Β¬ 𝑋 ∈ 𝑉) β†’ (β™―β€˜(𝑉 βˆͺ {𝑋})) = ((β™―β€˜π‘‰) + 1)))
376, 36syl 17 . . . . . 6 (πœ‘ β†’ ((𝑉 ∈ Fin ∧ Β¬ 𝑋 ∈ 𝑉) β†’ (β™―β€˜(𝑉 βˆͺ {𝑋})) = ((β™―β€˜π‘‰) + 1)))
3822, 35, 37mp2and 698 . . . . 5 (πœ‘ β†’ (β™―β€˜(𝑉 βˆͺ {𝑋})) = ((β™―β€˜π‘‰) + 1))
3929, 38breqan12rd 5166 . . . 4 ((πœ‘ ∧ 𝐸 = 𝐷) β†’ ((πΉβ€˜πΈ) ≀ (β™―β€˜(𝑉 βˆͺ {𝑋})) ↔ (πΉβ€˜π·) ≀ ((β™―β€˜π‘‰) + 1)))
4028, 39mpbird 257 . . 3 ((πœ‘ ∧ 𝐸 = 𝐷) β†’ (πΉβ€˜πΈ) ≀ (β™―β€˜(𝑉 βˆͺ {𝑋})))
41 snfi 9044 . . . . . . 7 {𝑋} ∈ Fin
42 unfi 9172 . . . . . . 7 ((𝑉 ∈ Fin ∧ {𝑋} ∈ Fin) β†’ (𝑉 βˆͺ {𝑋}) ∈ Fin)
4322, 41, 42sylancl 587 . . . . . 6 (πœ‘ β†’ (𝑉 βˆͺ {𝑋}) ∈ Fin)
44 ramub1.m . . . . . . 7 (πœ‘ β†’ 𝑀 ∈ β„•)
4544nnnn0d 12532 . . . . . 6 (πœ‘ β†’ 𝑀 ∈ β„•0)
46 ramub1.3 . . . . . . 7 𝐢 = (π‘Ž ∈ V, 𝑖 ∈ β„•0 ↦ {𝑏 ∈ 𝒫 π‘Ž ∣ (β™―β€˜π‘) = 𝑖})
4746hashbcval 16935 . . . . . 6 (((𝑉 βˆͺ {𝑋}) ∈ Fin ∧ 𝑀 ∈ β„•0) β†’ ((𝑉 βˆͺ {𝑋})𝐢𝑀) = {π‘₯ ∈ 𝒫 (𝑉 βˆͺ {𝑋}) ∣ (β™―β€˜π‘₯) = 𝑀})
4843, 45, 47syl2anc 585 . . . . 5 (πœ‘ β†’ ((𝑉 βˆͺ {𝑋})𝐢𝑀) = {π‘₯ ∈ 𝒫 (𝑉 βˆͺ {𝑋}) ∣ (β™―β€˜π‘₯) = 𝑀})
4948adantr 482 . . . 4 ((πœ‘ ∧ 𝐸 = 𝐷) β†’ ((𝑉 βˆͺ {𝑋})𝐢𝑀) = {π‘₯ ∈ 𝒫 (𝑉 βˆͺ {𝑋}) ∣ (β™―β€˜π‘₯) = 𝑀})
50 simpl1l 1225 . . . . . . . 8 ((((πœ‘ ∧ 𝐸 = 𝐷) ∧ π‘₯ ∈ 𝒫 (𝑉 βˆͺ {𝑋}) ∧ (β™―β€˜π‘₯) = 𝑀) ∧ π‘₯ ∈ 𝒫 𝑉) β†’ πœ‘)
5146hashbcval 16935 . . . . . . . . . 10 ((𝑉 ∈ Fin ∧ 𝑀 ∈ β„•0) β†’ (𝑉𝐢𝑀) = {π‘₯ ∈ 𝒫 𝑉 ∣ (β™―β€˜π‘₯) = 𝑀})
5222, 45, 51syl2anc 585 . . . . . . . . 9 (πœ‘ β†’ (𝑉𝐢𝑀) = {π‘₯ ∈ 𝒫 𝑉 ∣ (β™―β€˜π‘₯) = 𝑀})
53 ramub1.s . . . . . . . . 9 (πœ‘ β†’ (𝑉𝐢𝑀) βŠ† (◑𝐾 β€œ {𝐸}))
5452, 53eqsstrrd 4022 . . . . . . . 8 (πœ‘ β†’ {π‘₯ ∈ 𝒫 𝑉 ∣ (β™―β€˜π‘₯) = 𝑀} βŠ† (◑𝐾 β€œ {𝐸}))
5550, 54syl 17 . . . . . . 7 ((((πœ‘ ∧ 𝐸 = 𝐷) ∧ π‘₯ ∈ 𝒫 (𝑉 βˆͺ {𝑋}) ∧ (β™―β€˜π‘₯) = 𝑀) ∧ π‘₯ ∈ 𝒫 𝑉) β†’ {π‘₯ ∈ 𝒫 𝑉 ∣ (β™―β€˜π‘₯) = 𝑀} βŠ† (◑𝐾 β€œ {𝐸}))
56 simpr 486 . . . . . . . 8 ((((πœ‘ ∧ 𝐸 = 𝐷) ∧ π‘₯ ∈ 𝒫 (𝑉 βˆͺ {𝑋}) ∧ (β™―β€˜π‘₯) = 𝑀) ∧ π‘₯ ∈ 𝒫 𝑉) β†’ π‘₯ ∈ 𝒫 𝑉)
57 simpl3 1194 . . . . . . . 8 ((((πœ‘ ∧ 𝐸 = 𝐷) ∧ π‘₯ ∈ 𝒫 (𝑉 βˆͺ {𝑋}) ∧ (β™―β€˜π‘₯) = 𝑀) ∧ π‘₯ ∈ 𝒫 𝑉) β†’ (β™―β€˜π‘₯) = 𝑀)
58 rabid 3453 . . . . . . . 8 (π‘₯ ∈ {π‘₯ ∈ 𝒫 𝑉 ∣ (β™―β€˜π‘₯) = 𝑀} ↔ (π‘₯ ∈ 𝒫 𝑉 ∧ (β™―β€˜π‘₯) = 𝑀))
5956, 57, 58sylanbrc 584 . . . . . . 7 ((((πœ‘ ∧ 𝐸 = 𝐷) ∧ π‘₯ ∈ 𝒫 (𝑉 βˆͺ {𝑋}) ∧ (β™―β€˜π‘₯) = 𝑀) ∧ π‘₯ ∈ 𝒫 𝑉) β†’ π‘₯ ∈ {π‘₯ ∈ 𝒫 𝑉 ∣ (β™―β€˜π‘₯) = 𝑀})
6055, 59sseldd 3984 . . . . . 6 ((((πœ‘ ∧ 𝐸 = 𝐷) ∧ π‘₯ ∈ 𝒫 (𝑉 βˆͺ {𝑋}) ∧ (β™―β€˜π‘₯) = 𝑀) ∧ π‘₯ ∈ 𝒫 𝑉) β†’ π‘₯ ∈ (◑𝐾 β€œ {𝐸}))
61 simpl2 1193 . . . . . . . . . . . 12 ((((πœ‘ ∧ 𝐸 = 𝐷) ∧ π‘₯ ∈ 𝒫 (𝑉 βˆͺ {𝑋}) ∧ (β™―β€˜π‘₯) = 𝑀) ∧ Β¬ π‘₯ ∈ 𝒫 𝑉) β†’ π‘₯ ∈ 𝒫 (𝑉 βˆͺ {𝑋}))
6261elpwid 4612 . . . . . . . . . . 11 ((((πœ‘ ∧ 𝐸 = 𝐷) ∧ π‘₯ ∈ 𝒫 (𝑉 βˆͺ {𝑋}) ∧ (β™―β€˜π‘₯) = 𝑀) ∧ Β¬ π‘₯ ∈ 𝒫 𝑉) β†’ π‘₯ βŠ† (𝑉 βˆͺ {𝑋}))
63 simpl1l 1225 . . . . . . . . . . . 12 ((((πœ‘ ∧ 𝐸 = 𝐷) ∧ π‘₯ ∈ 𝒫 (𝑉 βˆͺ {𝑋}) ∧ (β™―β€˜π‘₯) = 𝑀) ∧ Β¬ π‘₯ ∈ 𝒫 𝑉) β†’ πœ‘)
6463, 8syl 17 . . . . . . . . . . 11 ((((πœ‘ ∧ 𝐸 = 𝐷) ∧ π‘₯ ∈ 𝒫 (𝑉 βˆͺ {𝑋}) ∧ (β™―β€˜π‘₯) = 𝑀) ∧ Β¬ π‘₯ ∈ 𝒫 𝑉) β†’ (𝑉 βˆͺ {𝑋}) βŠ† 𝑆)
6562, 64sstrd 3993 . . . . . . . . . 10 ((((πœ‘ ∧ 𝐸 = 𝐷) ∧ π‘₯ ∈ 𝒫 (𝑉 βˆͺ {𝑋}) ∧ (β™―β€˜π‘₯) = 𝑀) ∧ Β¬ π‘₯ ∈ 𝒫 𝑉) β†’ π‘₯ βŠ† 𝑆)
66 vex 3479 . . . . . . . . . . 11 π‘₯ ∈ V
6766elpw 4607 . . . . . . . . . 10 (π‘₯ ∈ 𝒫 𝑆 ↔ π‘₯ βŠ† 𝑆)
6865, 67sylibr 233 . . . . . . . . 9 ((((πœ‘ ∧ 𝐸 = 𝐷) ∧ π‘₯ ∈ 𝒫 (𝑉 βˆͺ {𝑋}) ∧ (β™―β€˜π‘₯) = 𝑀) ∧ Β¬ π‘₯ ∈ 𝒫 𝑉) β†’ π‘₯ ∈ 𝒫 𝑆)
69 simpl3 1194 . . . . . . . . 9 ((((πœ‘ ∧ 𝐸 = 𝐷) ∧ π‘₯ ∈ 𝒫 (𝑉 βˆͺ {𝑋}) ∧ (β™―β€˜π‘₯) = 𝑀) ∧ Β¬ π‘₯ ∈ 𝒫 𝑉) β†’ (β™―β€˜π‘₯) = 𝑀)
70 rabid 3453 . . . . . . . . 9 (π‘₯ ∈ {π‘₯ ∈ 𝒫 𝑆 ∣ (β™―β€˜π‘₯) = 𝑀} ↔ (π‘₯ ∈ 𝒫 𝑆 ∧ (β™―β€˜π‘₯) = 𝑀))
7168, 69, 70sylanbrc 584 . . . . . . . 8 ((((πœ‘ ∧ 𝐸 = 𝐷) ∧ π‘₯ ∈ 𝒫 (𝑉 βˆͺ {𝑋}) ∧ (β™―β€˜π‘₯) = 𝑀) ∧ Β¬ π‘₯ ∈ 𝒫 𝑉) β†’ π‘₯ ∈ {π‘₯ ∈ 𝒫 𝑆 ∣ (β™―β€˜π‘₯) = 𝑀})
7246hashbcval 16935 . . . . . . . . . 10 ((𝑆 ∈ Fin ∧ 𝑀 ∈ β„•0) β†’ (𝑆𝐢𝑀) = {π‘₯ ∈ 𝒫 𝑆 ∣ (β™―β€˜π‘₯) = 𝑀})
731, 45, 72syl2anc 585 . . . . . . . . 9 (πœ‘ β†’ (𝑆𝐢𝑀) = {π‘₯ ∈ 𝒫 𝑆 ∣ (β™―β€˜π‘₯) = 𝑀})
7463, 73syl 17 . . . . . . . 8 ((((πœ‘ ∧ 𝐸 = 𝐷) ∧ π‘₯ ∈ 𝒫 (𝑉 βˆͺ {𝑋}) ∧ (β™―β€˜π‘₯) = 𝑀) ∧ Β¬ π‘₯ ∈ 𝒫 𝑉) β†’ (𝑆𝐢𝑀) = {π‘₯ ∈ 𝒫 𝑆 ∣ (β™―β€˜π‘₯) = 𝑀})
7571, 74eleqtrrd 2837 . . . . . . 7 ((((πœ‘ ∧ 𝐸 = 𝐷) ∧ π‘₯ ∈ 𝒫 (𝑉 βˆͺ {𝑋}) ∧ (β™―β€˜π‘₯) = 𝑀) ∧ Β¬ π‘₯ ∈ 𝒫 𝑉) β†’ π‘₯ ∈ (𝑆𝐢𝑀))
763difss2d 4135 . . . . . . . . . . . . . . 15 (πœ‘ β†’ π‘Š βŠ† 𝑆)
771, 76ssfid 9267 . . . . . . . . . . . . . 14 (πœ‘ β†’ π‘Š ∈ Fin)
78 nnm1nn0 12513 . . . . . . . . . . . . . . 15 (𝑀 ∈ β„• β†’ (𝑀 βˆ’ 1) ∈ β„•0)
7944, 78syl 17 . . . . . . . . . . . . . 14 (πœ‘ β†’ (𝑀 βˆ’ 1) ∈ β„•0)
8046hashbcval 16935 . . . . . . . . . . . . . 14 ((π‘Š ∈ Fin ∧ (𝑀 βˆ’ 1) ∈ β„•0) β†’ (π‘ŠπΆ(𝑀 βˆ’ 1)) = {𝑒 ∈ 𝒫 π‘Š ∣ (β™―β€˜π‘’) = (𝑀 βˆ’ 1)})
8177, 79, 80syl2anc 585 . . . . . . . . . . . . 13 (πœ‘ β†’ (π‘ŠπΆ(𝑀 βˆ’ 1)) = {𝑒 ∈ 𝒫 π‘Š ∣ (β™―β€˜π‘’) = (𝑀 βˆ’ 1)})
82 ramub1.8 . . . . . . . . . . . . 13 (πœ‘ β†’ (π‘ŠπΆ(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝐷}))
8381, 82eqsstrrd 4022 . . . . . . . . . . . 12 (πœ‘ β†’ {𝑒 ∈ 𝒫 π‘Š ∣ (β™―β€˜π‘’) = (𝑀 βˆ’ 1)} βŠ† (◑𝐻 β€œ {𝐷}))
8463, 83syl 17 . . . . . . . . . . 11 ((((πœ‘ ∧ 𝐸 = 𝐷) ∧ π‘₯ ∈ 𝒫 (𝑉 βˆͺ {𝑋}) ∧ (β™―β€˜π‘₯) = 𝑀) ∧ Β¬ π‘₯ ∈ 𝒫 𝑉) β†’ {𝑒 ∈ 𝒫 π‘Š ∣ (β™―β€˜π‘’) = (𝑀 βˆ’ 1)} βŠ† (◑𝐻 β€œ {𝐷}))
85 fveqeq2 6901 . . . . . . . . . . . 12 (𝑒 = (π‘₯ βˆ– {𝑋}) β†’ ((β™―β€˜π‘’) = (𝑀 βˆ’ 1) ↔ (β™―β€˜(π‘₯ βˆ– {𝑋})) = (𝑀 βˆ’ 1)))
86 uncom 4154 . . . . . . . . . . . . . . . 16 (𝑉 βˆͺ {𝑋}) = ({𝑋} βˆͺ 𝑉)
8762, 86sseqtrdi 4033 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ 𝐸 = 𝐷) ∧ π‘₯ ∈ 𝒫 (𝑉 βˆͺ {𝑋}) ∧ (β™―β€˜π‘₯) = 𝑀) ∧ Β¬ π‘₯ ∈ 𝒫 𝑉) β†’ π‘₯ βŠ† ({𝑋} βˆͺ 𝑉))
88 ssundif 4488 . . . . . . . . . . . . . . 15 (π‘₯ βŠ† ({𝑋} βˆͺ 𝑉) ↔ (π‘₯ βˆ– {𝑋}) βŠ† 𝑉)
8987, 88sylib 217 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ 𝐸 = 𝐷) ∧ π‘₯ ∈ 𝒫 (𝑉 βˆͺ {𝑋}) ∧ (β™―β€˜π‘₯) = 𝑀) ∧ Β¬ π‘₯ ∈ 𝒫 𝑉) β†’ (π‘₯ βˆ– {𝑋}) βŠ† 𝑉)
9063, 2syl 17 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ 𝐸 = 𝐷) ∧ π‘₯ ∈ 𝒫 (𝑉 βˆͺ {𝑋}) ∧ (β™―β€˜π‘₯) = 𝑀) ∧ Β¬ π‘₯ ∈ 𝒫 𝑉) β†’ 𝑉 βŠ† π‘Š)
9189, 90sstrd 3993 . . . . . . . . . . . . 13 ((((πœ‘ ∧ 𝐸 = 𝐷) ∧ π‘₯ ∈ 𝒫 (𝑉 βˆͺ {𝑋}) ∧ (β™―β€˜π‘₯) = 𝑀) ∧ Β¬ π‘₯ ∈ 𝒫 𝑉) β†’ (π‘₯ βˆ– {𝑋}) βŠ† π‘Š)
9266difexi 5329 . . . . . . . . . . . . . 14 (π‘₯ βˆ– {𝑋}) ∈ V
9392elpw 4607 . . . . . . . . . . . . 13 ((π‘₯ βˆ– {𝑋}) ∈ 𝒫 π‘Š ↔ (π‘₯ βˆ– {𝑋}) βŠ† π‘Š)
9491, 93sylibr 233 . . . . . . . . . . . 12 ((((πœ‘ ∧ 𝐸 = 𝐷) ∧ π‘₯ ∈ 𝒫 (𝑉 βˆͺ {𝑋}) ∧ (β™―β€˜π‘₯) = 𝑀) ∧ Β¬ π‘₯ ∈ 𝒫 𝑉) β†’ (π‘₯ βˆ– {𝑋}) ∈ 𝒫 π‘Š)
9563, 1syl 17 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ 𝐸 = 𝐷) ∧ π‘₯ ∈ 𝒫 (𝑉 βˆͺ {𝑋}) ∧ (β™―β€˜π‘₯) = 𝑀) ∧ Β¬ π‘₯ ∈ 𝒫 𝑉) β†’ 𝑆 ∈ Fin)
9695, 65ssfid 9267 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ 𝐸 = 𝐷) ∧ π‘₯ ∈ 𝒫 (𝑉 βˆͺ {𝑋}) ∧ (β™―β€˜π‘₯) = 𝑀) ∧ Β¬ π‘₯ ∈ 𝒫 𝑉) β†’ π‘₯ ∈ Fin)
97 diffi 9179 . . . . . . . . . . . . . . . 16 (π‘₯ ∈ Fin β†’ (π‘₯ βˆ– {𝑋}) ∈ Fin)
9896, 97syl 17 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ 𝐸 = 𝐷) ∧ π‘₯ ∈ 𝒫 (𝑉 βˆͺ {𝑋}) ∧ (β™―β€˜π‘₯) = 𝑀) ∧ Β¬ π‘₯ ∈ 𝒫 𝑉) β†’ (π‘₯ βˆ– {𝑋}) ∈ Fin)
99 hashcl 14316 . . . . . . . . . . . . . . 15 ((π‘₯ βˆ– {𝑋}) ∈ Fin β†’ (β™―β€˜(π‘₯ βˆ– {𝑋})) ∈ β„•0)
100 nn0cn 12482 . . . . . . . . . . . . . . 15 ((β™―β€˜(π‘₯ βˆ– {𝑋})) ∈ β„•0 β†’ (β™―β€˜(π‘₯ βˆ– {𝑋})) ∈ β„‚)
10198, 99, 1003syl 18 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ 𝐸 = 𝐷) ∧ π‘₯ ∈ 𝒫 (𝑉 βˆͺ {𝑋}) ∧ (β™―β€˜π‘₯) = 𝑀) ∧ Β¬ π‘₯ ∈ 𝒫 𝑉) β†’ (β™―β€˜(π‘₯ βˆ– {𝑋})) ∈ β„‚)
102 ax-1cn 11168 . . . . . . . . . . . . . 14 1 ∈ β„‚
103 pncan 11466 . . . . . . . . . . . . . 14 (((β™―β€˜(π‘₯ βˆ– {𝑋})) ∈ β„‚ ∧ 1 ∈ β„‚) β†’ (((β™―β€˜(π‘₯ βˆ– {𝑋})) + 1) βˆ’ 1) = (β™―β€˜(π‘₯ βˆ– {𝑋})))
104101, 102, 103sylancl 587 . . . . . . . . . . . . 13 ((((πœ‘ ∧ 𝐸 = 𝐷) ∧ π‘₯ ∈ 𝒫 (𝑉 βˆͺ {𝑋}) ∧ (β™―β€˜π‘₯) = 𝑀) ∧ Β¬ π‘₯ ∈ 𝒫 𝑉) β†’ (((β™―β€˜(π‘₯ βˆ– {𝑋})) + 1) βˆ’ 1) = (β™―β€˜(π‘₯ βˆ– {𝑋})))
105 neldifsnd 4797 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ 𝐸 = 𝐷) ∧ π‘₯ ∈ 𝒫 (𝑉 βˆͺ {𝑋}) ∧ (β™―β€˜π‘₯) = 𝑀) ∧ Β¬ π‘₯ ∈ 𝒫 𝑉) β†’ Β¬ 𝑋 ∈ (π‘₯ βˆ– {𝑋}))
106 hashunsng 14352 . . . . . . . . . . . . . . . . 17 (𝑋 ∈ 𝑆 β†’ (((π‘₯ βˆ– {𝑋}) ∈ Fin ∧ Β¬ 𝑋 ∈ (π‘₯ βˆ– {𝑋})) β†’ (β™―β€˜((π‘₯ βˆ– {𝑋}) βˆͺ {𝑋})) = ((β™―β€˜(π‘₯ βˆ– {𝑋})) + 1)))
10763, 6, 1063syl 18 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ 𝐸 = 𝐷) ∧ π‘₯ ∈ 𝒫 (𝑉 βˆͺ {𝑋}) ∧ (β™―β€˜π‘₯) = 𝑀) ∧ Β¬ π‘₯ ∈ 𝒫 𝑉) β†’ (((π‘₯ βˆ– {𝑋}) ∈ Fin ∧ Β¬ 𝑋 ∈ (π‘₯ βˆ– {𝑋})) β†’ (β™―β€˜((π‘₯ βˆ– {𝑋}) βˆͺ {𝑋})) = ((β™―β€˜(π‘₯ βˆ– {𝑋})) + 1)))
10898, 105, 107mp2and 698 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ 𝐸 = 𝐷) ∧ π‘₯ ∈ 𝒫 (𝑉 βˆͺ {𝑋}) ∧ (β™―β€˜π‘₯) = 𝑀) ∧ Β¬ π‘₯ ∈ 𝒫 𝑉) β†’ (β™―β€˜((π‘₯ βˆ– {𝑋}) βˆͺ {𝑋})) = ((β™―β€˜(π‘₯ βˆ– {𝑋})) + 1))
109 undif1 4476 . . . . . . . . . . . . . . . . . 18 ((π‘₯ βˆ– {𝑋}) βˆͺ {𝑋}) = (π‘₯ βˆͺ {𝑋})
110 simpr 486 . . . . . . . . . . . . . . . . . . . . . 22 ((((πœ‘ ∧ 𝐸 = 𝐷) ∧ π‘₯ ∈ 𝒫 (𝑉 βˆͺ {𝑋}) ∧ (β™―β€˜π‘₯) = 𝑀) ∧ Β¬ π‘₯ ∈ 𝒫 𝑉) β†’ Β¬ π‘₯ ∈ 𝒫 𝑉)
11161, 110eldifd 3960 . . . . . . . . . . . . . . . . . . . . 21 ((((πœ‘ ∧ 𝐸 = 𝐷) ∧ π‘₯ ∈ 𝒫 (𝑉 βˆͺ {𝑋}) ∧ (β™―β€˜π‘₯) = 𝑀) ∧ Β¬ π‘₯ ∈ 𝒫 𝑉) β†’ π‘₯ ∈ (𝒫 (𝑉 βˆͺ {𝑋}) βˆ– 𝒫 𝑉))
112 elpwunsn 4688 . . . . . . . . . . . . . . . . . . . . 21 (π‘₯ ∈ (𝒫 (𝑉 βˆͺ {𝑋}) βˆ– 𝒫 𝑉) β†’ 𝑋 ∈ π‘₯)
113111, 112syl 17 . . . . . . . . . . . . . . . . . . . 20 ((((πœ‘ ∧ 𝐸 = 𝐷) ∧ π‘₯ ∈ 𝒫 (𝑉 βˆͺ {𝑋}) ∧ (β™―β€˜π‘₯) = 𝑀) ∧ Β¬ π‘₯ ∈ 𝒫 𝑉) β†’ 𝑋 ∈ π‘₯)
114113snssd 4813 . . . . . . . . . . . . . . . . . . 19 ((((πœ‘ ∧ 𝐸 = 𝐷) ∧ π‘₯ ∈ 𝒫 (𝑉 βˆͺ {𝑋}) ∧ (β™―β€˜π‘₯) = 𝑀) ∧ Β¬ π‘₯ ∈ 𝒫 𝑉) β†’ {𝑋} βŠ† π‘₯)
115 ssequn2 4184 . . . . . . . . . . . . . . . . . . 19 ({𝑋} βŠ† π‘₯ ↔ (π‘₯ βˆͺ {𝑋}) = π‘₯)
116114, 115sylib 217 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ 𝐸 = 𝐷) ∧ π‘₯ ∈ 𝒫 (𝑉 βˆͺ {𝑋}) ∧ (β™―β€˜π‘₯) = 𝑀) ∧ Β¬ π‘₯ ∈ 𝒫 𝑉) β†’ (π‘₯ βˆͺ {𝑋}) = π‘₯)
117109, 116eqtr2id 2786 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ 𝐸 = 𝐷) ∧ π‘₯ ∈ 𝒫 (𝑉 βˆͺ {𝑋}) ∧ (β™―β€˜π‘₯) = 𝑀) ∧ Β¬ π‘₯ ∈ 𝒫 𝑉) β†’ π‘₯ = ((π‘₯ βˆ– {𝑋}) βˆͺ {𝑋}))
118117fveq2d 6896 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ 𝐸 = 𝐷) ∧ π‘₯ ∈ 𝒫 (𝑉 βˆͺ {𝑋}) ∧ (β™―β€˜π‘₯) = 𝑀) ∧ Β¬ π‘₯ ∈ 𝒫 𝑉) β†’ (β™―β€˜π‘₯) = (β™―β€˜((π‘₯ βˆ– {𝑋}) βˆͺ {𝑋})))
119118, 69eqtr3d 2775 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ 𝐸 = 𝐷) ∧ π‘₯ ∈ 𝒫 (𝑉 βˆͺ {𝑋}) ∧ (β™―β€˜π‘₯) = 𝑀) ∧ Β¬ π‘₯ ∈ 𝒫 𝑉) β†’ (β™―β€˜((π‘₯ βˆ– {𝑋}) βˆͺ {𝑋})) = 𝑀)
120108, 119eqtr3d 2775 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ 𝐸 = 𝐷) ∧ π‘₯ ∈ 𝒫 (𝑉 βˆͺ {𝑋}) ∧ (β™―β€˜π‘₯) = 𝑀) ∧ Β¬ π‘₯ ∈ 𝒫 𝑉) β†’ ((β™―β€˜(π‘₯ βˆ– {𝑋})) + 1) = 𝑀)
121120oveq1d 7424 . . . . . . . . . . . . 13 ((((πœ‘ ∧ 𝐸 = 𝐷) ∧ π‘₯ ∈ 𝒫 (𝑉 βˆͺ {𝑋}) ∧ (β™―β€˜π‘₯) = 𝑀) ∧ Β¬ π‘₯ ∈ 𝒫 𝑉) β†’ (((β™―β€˜(π‘₯ βˆ– {𝑋})) + 1) βˆ’ 1) = (𝑀 βˆ’ 1))
122104, 121eqtr3d 2775 . . . . . . . . . . . 12 ((((πœ‘ ∧ 𝐸 = 𝐷) ∧ π‘₯ ∈ 𝒫 (𝑉 βˆͺ {𝑋}) ∧ (β™―β€˜π‘₯) = 𝑀) ∧ Β¬ π‘₯ ∈ 𝒫 𝑉) β†’ (β™―β€˜(π‘₯ βˆ– {𝑋})) = (𝑀 βˆ’ 1))
12385, 94, 122elrabd 3686 . . . . . . . . . . 11 ((((πœ‘ ∧ 𝐸 = 𝐷) ∧ π‘₯ ∈ 𝒫 (𝑉 βˆͺ {𝑋}) ∧ (β™―β€˜π‘₯) = 𝑀) ∧ Β¬ π‘₯ ∈ 𝒫 𝑉) β†’ (π‘₯ βˆ– {𝑋}) ∈ {𝑒 ∈ 𝒫 π‘Š ∣ (β™―β€˜π‘’) = (𝑀 βˆ’ 1)})
12484, 123sseldd 3984 . . . . . . . . . 10 ((((πœ‘ ∧ 𝐸 = 𝐷) ∧ π‘₯ ∈ 𝒫 (𝑉 βˆͺ {𝑋}) ∧ (β™―β€˜π‘₯) = 𝑀) ∧ Β¬ π‘₯ ∈ 𝒫 𝑉) β†’ (π‘₯ βˆ– {𝑋}) ∈ (◑𝐻 β€œ {𝐷}))
125 ramub1.h . . . . . . . . . . . 12 𝐻 = (𝑒 ∈ ((𝑆 βˆ– {𝑋})𝐢(𝑀 βˆ’ 1)) ↦ (πΎβ€˜(𝑒 βˆͺ {𝑋})))
126125mptiniseg 6239 . . . . . . . . . . 11 (𝐷 ∈ 𝑅 β†’ (◑𝐻 β€œ {𝐷}) = {𝑒 ∈ ((𝑆 βˆ– {𝑋})𝐢(𝑀 βˆ’ 1)) ∣ (πΎβ€˜(𝑒 βˆͺ {𝑋})) = 𝐷})
12763, 17, 1263syl 18 . . . . . . . . . 10 ((((πœ‘ ∧ 𝐸 = 𝐷) ∧ π‘₯ ∈ 𝒫 (𝑉 βˆͺ {𝑋}) ∧ (β™―β€˜π‘₯) = 𝑀) ∧ Β¬ π‘₯ ∈ 𝒫 𝑉) β†’ (◑𝐻 β€œ {𝐷}) = {𝑒 ∈ ((𝑆 βˆ– {𝑋})𝐢(𝑀 βˆ’ 1)) ∣ (πΎβ€˜(𝑒 βˆͺ {𝑋})) = 𝐷})
128124, 127eleqtrd 2836 . . . . . . . . 9 ((((πœ‘ ∧ 𝐸 = 𝐷) ∧ π‘₯ ∈ 𝒫 (𝑉 βˆͺ {𝑋}) ∧ (β™―β€˜π‘₯) = 𝑀) ∧ Β¬ π‘₯ ∈ 𝒫 𝑉) β†’ (π‘₯ βˆ– {𝑋}) ∈ {𝑒 ∈ ((𝑆 βˆ– {𝑋})𝐢(𝑀 βˆ’ 1)) ∣ (πΎβ€˜(𝑒 βˆͺ {𝑋})) = 𝐷})
129 uneq1 4157 . . . . . . . . . . . 12 (𝑒 = (π‘₯ βˆ– {𝑋}) β†’ (𝑒 βˆͺ {𝑋}) = ((π‘₯ βˆ– {𝑋}) βˆͺ {𝑋}))
130129fveqeq2d 6900 . . . . . . . . . . 11 (𝑒 = (π‘₯ βˆ– {𝑋}) β†’ ((πΎβ€˜(𝑒 βˆͺ {𝑋})) = 𝐷 ↔ (πΎβ€˜((π‘₯ βˆ– {𝑋}) βˆͺ {𝑋})) = 𝐷))
131130elrab 3684 . . . . . . . . . 10 ((π‘₯ βˆ– {𝑋}) ∈ {𝑒 ∈ ((𝑆 βˆ– {𝑋})𝐢(𝑀 βˆ’ 1)) ∣ (πΎβ€˜(𝑒 βˆͺ {𝑋})) = 𝐷} ↔ ((π‘₯ βˆ– {𝑋}) ∈ ((𝑆 βˆ– {𝑋})𝐢(𝑀 βˆ’ 1)) ∧ (πΎβ€˜((π‘₯ βˆ– {𝑋}) βˆͺ {𝑋})) = 𝐷))
132131simprbi 498 . . . . . . . . 9 ((π‘₯ βˆ– {𝑋}) ∈ {𝑒 ∈ ((𝑆 βˆ– {𝑋})𝐢(𝑀 βˆ’ 1)) ∣ (πΎβ€˜(𝑒 βˆͺ {𝑋})) = 𝐷} β†’ (πΎβ€˜((π‘₯ βˆ– {𝑋}) βˆͺ {𝑋})) = 𝐷)
133128, 132syl 17 . . . . . . . 8 ((((πœ‘ ∧ 𝐸 = 𝐷) ∧ π‘₯ ∈ 𝒫 (𝑉 βˆͺ {𝑋}) ∧ (β™―β€˜π‘₯) = 𝑀) ∧ Β¬ π‘₯ ∈ 𝒫 𝑉) β†’ (πΎβ€˜((π‘₯ βˆ– {𝑋}) βˆͺ {𝑋})) = 𝐷)
134117fveq2d 6896 . . . . . . . 8 ((((πœ‘ ∧ 𝐸 = 𝐷) ∧ π‘₯ ∈ 𝒫 (𝑉 βˆͺ {𝑋}) ∧ (β™―β€˜π‘₯) = 𝑀) ∧ Β¬ π‘₯ ∈ 𝒫 𝑉) β†’ (πΎβ€˜π‘₯) = (πΎβ€˜((π‘₯ βˆ– {𝑋}) βˆͺ {𝑋})))
135 simpl1r 1226 . . . . . . . 8 ((((πœ‘ ∧ 𝐸 = 𝐷) ∧ π‘₯ ∈ 𝒫 (𝑉 βˆͺ {𝑋}) ∧ (β™―β€˜π‘₯) = 𝑀) ∧ Β¬ π‘₯ ∈ 𝒫 𝑉) β†’ 𝐸 = 𝐷)
136133, 134, 1353eqtr4d 2783 . . . . . . 7 ((((πœ‘ ∧ 𝐸 = 𝐷) ∧ π‘₯ ∈ 𝒫 (𝑉 βˆͺ {𝑋}) ∧ (β™―β€˜π‘₯) = 𝑀) ∧ Β¬ π‘₯ ∈ 𝒫 𝑉) β†’ (πΎβ€˜π‘₯) = 𝐸)
137 ramub1.6 . . . . . . . . 9 (πœ‘ β†’ 𝐾:(𝑆𝐢𝑀)βŸΆπ‘…)
138137ffnd 6719 . . . . . . . 8 (πœ‘ β†’ 𝐾 Fn (𝑆𝐢𝑀))
139 fniniseg 7062 . . . . . . . 8 (𝐾 Fn (𝑆𝐢𝑀) β†’ (π‘₯ ∈ (◑𝐾 β€œ {𝐸}) ↔ (π‘₯ ∈ (𝑆𝐢𝑀) ∧ (πΎβ€˜π‘₯) = 𝐸)))
14063, 138, 1393syl 18 . . . . . . 7 ((((πœ‘ ∧ 𝐸 = 𝐷) ∧ π‘₯ ∈ 𝒫 (𝑉 βˆͺ {𝑋}) ∧ (β™―β€˜π‘₯) = 𝑀) ∧ Β¬ π‘₯ ∈ 𝒫 𝑉) β†’ (π‘₯ ∈ (◑𝐾 β€œ {𝐸}) ↔ (π‘₯ ∈ (𝑆𝐢𝑀) ∧ (πΎβ€˜π‘₯) = 𝐸)))
14175, 136, 140mpbir2and 712 . . . . . 6 ((((πœ‘ ∧ 𝐸 = 𝐷) ∧ π‘₯ ∈ 𝒫 (𝑉 βˆͺ {𝑋}) ∧ (β™―β€˜π‘₯) = 𝑀) ∧ Β¬ π‘₯ ∈ 𝒫 𝑉) β†’ π‘₯ ∈ (◑𝐾 β€œ {𝐸}))
14260, 141pm2.61dan 812 . . . . 5 (((πœ‘ ∧ 𝐸 = 𝐷) ∧ π‘₯ ∈ 𝒫 (𝑉 βˆͺ {𝑋}) ∧ (β™―β€˜π‘₯) = 𝑀) β†’ π‘₯ ∈ (◑𝐾 β€œ {𝐸}))
143142rabssdv 4073 . . . 4 ((πœ‘ ∧ 𝐸 = 𝐷) β†’ {π‘₯ ∈ 𝒫 (𝑉 βˆͺ {𝑋}) ∣ (β™―β€˜π‘₯) = 𝑀} βŠ† (◑𝐾 β€œ {𝐸}))
14449, 143eqsstrd 4021 . . 3 ((πœ‘ ∧ 𝐸 = 𝐷) β†’ ((𝑉 βˆͺ {𝑋})𝐢𝑀) βŠ† (◑𝐾 β€œ {𝐸}))
145 fveq2 6892 . . . . . 6 (𝑧 = (𝑉 βˆͺ {𝑋}) β†’ (β™―β€˜π‘§) = (β™―β€˜(𝑉 βˆͺ {𝑋})))
146145breq2d 5161 . . . . 5 (𝑧 = (𝑉 βˆͺ {𝑋}) β†’ ((πΉβ€˜πΈ) ≀ (β™―β€˜π‘§) ↔ (πΉβ€˜πΈ) ≀ (β™―β€˜(𝑉 βˆͺ {𝑋}))))
147 oveq1 7416 . . . . . 6 (𝑧 = (𝑉 βˆͺ {𝑋}) β†’ (𝑧𝐢𝑀) = ((𝑉 βˆͺ {𝑋})𝐢𝑀))
148147sseq1d 4014 . . . . 5 (𝑧 = (𝑉 βˆͺ {𝑋}) β†’ ((𝑧𝐢𝑀) βŠ† (◑𝐾 β€œ {𝐸}) ↔ ((𝑉 βˆͺ {𝑋})𝐢𝑀) βŠ† (◑𝐾 β€œ {𝐸})))
149146, 148anbi12d 632 . . . 4 (𝑧 = (𝑉 βˆͺ {𝑋}) β†’ (((πΉβ€˜πΈ) ≀ (β™―β€˜π‘§) ∧ (𝑧𝐢𝑀) βŠ† (◑𝐾 β€œ {𝐸})) ↔ ((πΉβ€˜πΈ) ≀ (β™―β€˜(𝑉 βˆͺ {𝑋})) ∧ ((𝑉 βˆͺ {𝑋})𝐢𝑀) βŠ† (◑𝐾 β€œ {𝐸}))))
150149rspcev 3613 . . 3 (((𝑉 βˆͺ {𝑋}) ∈ 𝒫 𝑆 ∧ ((πΉβ€˜πΈ) ≀ (β™―β€˜(𝑉 βˆͺ {𝑋})) ∧ ((𝑉 βˆͺ {𝑋})𝐢𝑀) βŠ† (◑𝐾 β€œ {𝐸}))) β†’ βˆƒπ‘§ ∈ 𝒫 𝑆((πΉβ€˜πΈ) ≀ (β™―β€˜π‘§) ∧ (𝑧𝐢𝑀) βŠ† (◑𝐾 β€œ {𝐸})))
15110, 40, 144, 150syl12anc 836 . 2 ((πœ‘ ∧ 𝐸 = 𝐷) β†’ βˆƒπ‘§ ∈ 𝒫 𝑆((πΉβ€˜πΈ) ≀ (β™―β€˜π‘§) ∧ (𝑧𝐢𝑀) βŠ† (◑𝐾 β€œ {𝐸})))
1521, 5sselpwd 5327 . . . 4 (πœ‘ β†’ 𝑉 ∈ 𝒫 𝑆)
153152adantr 482 . . 3 ((πœ‘ ∧ 𝐸 β‰  𝐷) β†’ 𝑉 ∈ 𝒫 𝑆)
154 ifnefalse 4541 . . . . 5 (𝐸 β‰  𝐷 β†’ if(𝐸 = 𝐷, ((πΉβ€˜π·) βˆ’ 1), (πΉβ€˜πΈ)) = (πΉβ€˜πΈ))
155154adantl 483 . . . 4 ((πœ‘ ∧ 𝐸 β‰  𝐷) β†’ if(𝐸 = 𝐷, ((πΉβ€˜π·) βˆ’ 1), (πΉβ€˜πΈ)) = (πΉβ€˜πΈ))
15613adantr 482 . . . 4 ((πœ‘ ∧ 𝐸 β‰  𝐷) β†’ if(𝐸 = 𝐷, ((πΉβ€˜π·) βˆ’ 1), (πΉβ€˜πΈ)) ≀ (β™―β€˜π‘‰))
157155, 156eqbrtrrd 5173 . . 3 ((πœ‘ ∧ 𝐸 β‰  𝐷) β†’ (πΉβ€˜πΈ) ≀ (β™―β€˜π‘‰))
15853adantr 482 . . 3 ((πœ‘ ∧ 𝐸 β‰  𝐷) β†’ (𝑉𝐢𝑀) βŠ† (◑𝐾 β€œ {𝐸}))
159 fveq2 6892 . . . . . 6 (𝑧 = 𝑉 β†’ (β™―β€˜π‘§) = (β™―β€˜π‘‰))
160159breq2d 5161 . . . . 5 (𝑧 = 𝑉 β†’ ((πΉβ€˜πΈ) ≀ (β™―β€˜π‘§) ↔ (πΉβ€˜πΈ) ≀ (β™―β€˜π‘‰)))
161 oveq1 7416 . . . . . 6 (𝑧 = 𝑉 β†’ (𝑧𝐢𝑀) = (𝑉𝐢𝑀))
162161sseq1d 4014 . . . . 5 (𝑧 = 𝑉 β†’ ((𝑧𝐢𝑀) βŠ† (◑𝐾 β€œ {𝐸}) ↔ (𝑉𝐢𝑀) βŠ† (◑𝐾 β€œ {𝐸})))
163160, 162anbi12d 632 . . . 4 (𝑧 = 𝑉 β†’ (((πΉβ€˜πΈ) ≀ (β™―β€˜π‘§) ∧ (𝑧𝐢𝑀) βŠ† (◑𝐾 β€œ {𝐸})) ↔ ((πΉβ€˜πΈ) ≀ (β™―β€˜π‘‰) ∧ (𝑉𝐢𝑀) βŠ† (◑𝐾 β€œ {𝐸}))))
164163rspcev 3613 . . 3 ((𝑉 ∈ 𝒫 𝑆 ∧ ((πΉβ€˜πΈ) ≀ (β™―β€˜π‘‰) ∧ (𝑉𝐢𝑀) βŠ† (◑𝐾 β€œ {𝐸}))) β†’ βˆƒπ‘§ ∈ 𝒫 𝑆((πΉβ€˜πΈ) ≀ (β™―β€˜π‘§) ∧ (𝑧𝐢𝑀) βŠ† (◑𝐾 β€œ {𝐸})))
165153, 157, 158, 164syl12anc 836 . 2 ((πœ‘ ∧ 𝐸 β‰  𝐷) β†’ βˆƒπ‘§ ∈ 𝒫 𝑆((πΉβ€˜πΈ) ≀ (β™―β€˜π‘§) ∧ (𝑧𝐢𝑀) βŠ† (◑𝐾 β€œ {𝐸})))
166151, 165pm2.61dane 3030 1 (πœ‘ β†’ βˆƒπ‘§ ∈ 𝒫 𝑆((πΉβ€˜πΈ) ≀ (β™―β€˜π‘§) ∧ (𝑧𝐢𝑀) βŠ† (◑𝐾 β€œ {𝐸})))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 397   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107   β‰  wne 2941  βˆƒwrex 3071  {crab 3433  Vcvv 3475   βˆ– cdif 3946   βˆͺ cun 3947   βŠ† wss 3949  ifcif 4529  π’« cpw 4603  {csn 4629   class class class wbr 5149   ↦ cmpt 5232  β—‘ccnv 5676   β€œ cima 5680   Fn wfn 6539  βŸΆwf 6540  β€˜cfv 6544  (class class class)co 7409   ∈ cmpo 7411  Fincfn 8939  β„‚cc 11108  β„cr 11109  1c1 11111   + caddc 11113   ≀ cle 11249   βˆ’ cmin 11444  β„•cn 12212  β„•0cn0 12472  β™―chash 14290   Ramsey cram 16932
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725  ax-cnex 11166  ax-resscn 11167  ax-1cn 11168  ax-icn 11169  ax-addcl 11170  ax-addrcl 11171  ax-mulcl 11172  ax-mulrcl 11173  ax-mulcom 11174  ax-addass 11175  ax-mulass 11176  ax-distr 11177  ax-i2m1 11178  ax-1ne0 11179  ax-1rid 11180  ax-rnegex 11181  ax-rrecex 11182  ax-cnre 11183  ax-pre-lttri 11184  ax-pre-lttrn 11185  ax-pre-ltadd 11186  ax-pre-mulgt0 11187
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-int 4952  df-iun 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-riota 7365  df-ov 7412  df-oprab 7413  df-mpo 7414  df-om 7856  df-1st 7975  df-2nd 7976  df-frecs 8266  df-wrecs 8297  df-recs 8371  df-rdg 8410  df-1o 8466  df-oadd 8470  df-er 8703  df-en 8940  df-dom 8941  df-sdom 8942  df-fin 8943  df-dju 9896  df-card 9934  df-pnf 11250  df-mnf 11251  df-xr 11252  df-ltxr 11253  df-le 11254  df-sub 11446  df-neg 11447  df-nn 12213  df-n0 12473  df-z 12559  df-uz 12823  df-fz 13485  df-hash 14291
This theorem is referenced by:  ramub1lem2  16960
  Copyright terms: Public domain W3C validator