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

Theorem ramub1lem1 16963
Description: Lemma for ramub1 16965. (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 3991 . . . . . . 7 (πœ‘ β†’ 𝑉 βŠ† (𝑆 βˆ– {𝑋}))
54difss2d 4133 . . . . . 6 (πœ‘ β†’ 𝑉 βŠ† 𝑆)
6 ramub1.x . . . . . . 7 (πœ‘ β†’ 𝑋 ∈ 𝑆)
76snssd 4811 . . . . . 6 (πœ‘ β†’ {𝑋} βŠ† 𝑆)
85, 7unssd 4185 . . . . 5 (πœ‘ β†’ (𝑉 βˆͺ {𝑋}) βŠ† 𝑆)
91, 8sselpwd 5325 . . . 4 (πœ‘ β†’ (𝑉 βˆͺ {𝑋}) ∈ 𝒫 𝑆)
109adantr 479 . . 3 ((πœ‘ ∧ 𝐸 = 𝐷) β†’ (𝑉 βˆͺ {𝑋}) ∈ 𝒫 𝑆)
11 iftrue 4533 . . . . . . 7 (𝐸 = 𝐷 β†’ if(𝐸 = 𝐷, ((πΉβ€˜π·) βˆ’ 1), (πΉβ€˜πΈ)) = ((πΉβ€˜π·) βˆ’ 1))
1211adantl 480 . . . . . 6 ((πœ‘ ∧ 𝐸 = 𝐷) β†’ if(𝐸 = 𝐷, ((πΉβ€˜π·) βˆ’ 1), (πΉβ€˜πΈ)) = ((πΉβ€˜π·) βˆ’ 1))
13 ramub1.9 . . . . . . 7 (πœ‘ β†’ if(𝐸 = 𝐷, ((πΉβ€˜π·) βˆ’ 1), (πΉβ€˜πΈ)) ≀ (β™―β€˜π‘‰))
1413adantr 479 . . . . . 6 ((πœ‘ ∧ 𝐸 = 𝐷) β†’ if(𝐸 = 𝐷, ((πΉβ€˜π·) βˆ’ 1), (πΉβ€˜πΈ)) ≀ (β™―β€˜π‘‰))
1512, 14eqbrtrrd 5171 . . . . 5 ((πœ‘ ∧ 𝐸 = 𝐷) β†’ ((πΉβ€˜π·) βˆ’ 1) ≀ (β™―β€˜π‘‰))
16 ramub1.f . . . . . . . . 9 (πœ‘ β†’ 𝐹:π‘…βŸΆβ„•)
17 ramub1.d . . . . . . . . 9 (πœ‘ β†’ 𝐷 ∈ 𝑅)
1816, 17ffvelcdmd 7086 . . . . . . . 8 (πœ‘ β†’ (πΉβ€˜π·) ∈ β„•)
1918adantr 479 . . . . . . 7 ((πœ‘ ∧ 𝐸 = 𝐷) β†’ (πΉβ€˜π·) ∈ β„•)
2019nnred 12231 . . . . . 6 ((πœ‘ ∧ 𝐸 = 𝐷) β†’ (πΉβ€˜π·) ∈ ℝ)
21 1red 11219 . . . . . 6 ((πœ‘ ∧ 𝐸 = 𝐷) β†’ 1 ∈ ℝ)
221, 5ssfid 9269 . . . . . . . 8 (πœ‘ β†’ 𝑉 ∈ Fin)
23 hashcl 14320 . . . . . . . 8 (𝑉 ∈ Fin β†’ (β™―β€˜π‘‰) ∈ β„•0)
24 nn0re 12485 . . . . . . . 8 ((β™―β€˜π‘‰) ∈ β„•0 β†’ (β™―β€˜π‘‰) ∈ ℝ)
2522, 23, 243syl 18 . . . . . . 7 (πœ‘ β†’ (β™―β€˜π‘‰) ∈ ℝ)
2625adantr 479 . . . . . 6 ((πœ‘ ∧ 𝐸 = 𝐷) β†’ (β™―β€˜π‘‰) ∈ ℝ)
2720, 21, 26lesubaddd 11815 . . . . 5 ((πœ‘ ∧ 𝐸 = 𝐷) β†’ (((πΉβ€˜π·) βˆ’ 1) ≀ (β™―β€˜π‘‰) ↔ (πΉβ€˜π·) ≀ ((β™―β€˜π‘‰) + 1)))
2815, 27mpbid 231 . . . 4 ((πœ‘ ∧ 𝐸 = 𝐷) β†’ (πΉβ€˜π·) ≀ ((β™―β€˜π‘‰) + 1))
29 fveq2 6890 . . . . 5 (𝐸 = 𝐷 β†’ (πΉβ€˜πΈ) = (πΉβ€˜π·))
30 snidg 4661 . . . . . . . 8 (𝑋 ∈ 𝑆 β†’ 𝑋 ∈ {𝑋})
316, 30syl 17 . . . . . . 7 (πœ‘ β†’ 𝑋 ∈ {𝑋})
324sseld 3980 . . . . . . . 8 (πœ‘ β†’ (𝑋 ∈ 𝑉 β†’ 𝑋 ∈ (𝑆 βˆ– {𝑋})))
33 eldifn 4126 . . . . . . . 8 (𝑋 ∈ (𝑆 βˆ– {𝑋}) β†’ Β¬ 𝑋 ∈ {𝑋})
3432, 33syl6 35 . . . . . . 7 (πœ‘ β†’ (𝑋 ∈ 𝑉 β†’ Β¬ 𝑋 ∈ {𝑋}))
3531, 34mt2d 136 . . . . . 6 (πœ‘ β†’ Β¬ 𝑋 ∈ 𝑉)
36 hashunsng 14356 . . . . . . 7 (𝑋 ∈ 𝑆 β†’ ((𝑉 ∈ Fin ∧ Β¬ 𝑋 ∈ 𝑉) β†’ (β™―β€˜(𝑉 βˆͺ {𝑋})) = ((β™―β€˜π‘‰) + 1)))
376, 36syl 17 . . . . . 6 (πœ‘ β†’ ((𝑉 ∈ Fin ∧ Β¬ 𝑋 ∈ 𝑉) β†’ (β™―β€˜(𝑉 βˆͺ {𝑋})) = ((β™―β€˜π‘‰) + 1)))
3822, 35, 37mp2and 695 . . . . 5 (πœ‘ β†’ (β™―β€˜(𝑉 βˆͺ {𝑋})) = ((β™―β€˜π‘‰) + 1))
3929, 38breqan12rd 5164 . . . 4 ((πœ‘ ∧ 𝐸 = 𝐷) β†’ ((πΉβ€˜πΈ) ≀ (β™―β€˜(𝑉 βˆͺ {𝑋})) ↔ (πΉβ€˜π·) ≀ ((β™―β€˜π‘‰) + 1)))
4028, 39mpbird 256 . . 3 ((πœ‘ ∧ 𝐸 = 𝐷) β†’ (πΉβ€˜πΈ) ≀ (β™―β€˜(𝑉 βˆͺ {𝑋})))
41 snfi 9046 . . . . . . 7 {𝑋} ∈ Fin
42 unfi 9174 . . . . . . 7 ((𝑉 ∈ Fin ∧ {𝑋} ∈ Fin) β†’ (𝑉 βˆͺ {𝑋}) ∈ Fin)
4322, 41, 42sylancl 584 . . . . . 6 (πœ‘ β†’ (𝑉 βˆͺ {𝑋}) ∈ Fin)
44 ramub1.m . . . . . . 7 (πœ‘ β†’ 𝑀 ∈ β„•)
4544nnnn0d 12536 . . . . . 6 (πœ‘ β†’ 𝑀 ∈ β„•0)
46 ramub1.3 . . . . . . 7 𝐢 = (π‘Ž ∈ V, 𝑖 ∈ β„•0 ↦ {𝑏 ∈ 𝒫 π‘Ž ∣ (β™―β€˜π‘) = 𝑖})
4746hashbcval 16939 . . . . . 6 (((𝑉 βˆͺ {𝑋}) ∈ Fin ∧ 𝑀 ∈ β„•0) β†’ ((𝑉 βˆͺ {𝑋})𝐢𝑀) = {π‘₯ ∈ 𝒫 (𝑉 βˆͺ {𝑋}) ∣ (β™―β€˜π‘₯) = 𝑀})
4843, 45, 47syl2anc 582 . . . . 5 (πœ‘ β†’ ((𝑉 βˆͺ {𝑋})𝐢𝑀) = {π‘₯ ∈ 𝒫 (𝑉 βˆͺ {𝑋}) ∣ (β™―β€˜π‘₯) = 𝑀})
4948adantr 479 . . . 4 ((πœ‘ ∧ 𝐸 = 𝐷) β†’ ((𝑉 βˆͺ {𝑋})𝐢𝑀) = {π‘₯ ∈ 𝒫 (𝑉 βˆͺ {𝑋}) ∣ (β™―β€˜π‘₯) = 𝑀})
50 simpl1l 1222 . . . . . . . 8 ((((πœ‘ ∧ 𝐸 = 𝐷) ∧ π‘₯ ∈ 𝒫 (𝑉 βˆͺ {𝑋}) ∧ (β™―β€˜π‘₯) = 𝑀) ∧ π‘₯ ∈ 𝒫 𝑉) β†’ πœ‘)
5146hashbcval 16939 . . . . . . . . . 10 ((𝑉 ∈ Fin ∧ 𝑀 ∈ β„•0) β†’ (𝑉𝐢𝑀) = {π‘₯ ∈ 𝒫 𝑉 ∣ (β™―β€˜π‘₯) = 𝑀})
5222, 45, 51syl2anc 582 . . . . . . . . 9 (πœ‘ β†’ (𝑉𝐢𝑀) = {π‘₯ ∈ 𝒫 𝑉 ∣ (β™―β€˜π‘₯) = 𝑀})
53 ramub1.s . . . . . . . . 9 (πœ‘ β†’ (𝑉𝐢𝑀) βŠ† (◑𝐾 β€œ {𝐸}))
5452, 53eqsstrrd 4020 . . . . . . . 8 (πœ‘ β†’ {π‘₯ ∈ 𝒫 𝑉 ∣ (β™―β€˜π‘₯) = 𝑀} βŠ† (◑𝐾 β€œ {𝐸}))
5550, 54syl 17 . . . . . . 7 ((((πœ‘ ∧ 𝐸 = 𝐷) ∧ π‘₯ ∈ 𝒫 (𝑉 βˆͺ {𝑋}) ∧ (β™―β€˜π‘₯) = 𝑀) ∧ π‘₯ ∈ 𝒫 𝑉) β†’ {π‘₯ ∈ 𝒫 𝑉 ∣ (β™―β€˜π‘₯) = 𝑀} βŠ† (◑𝐾 β€œ {𝐸}))
56 simpr 483 . . . . . . . 8 ((((πœ‘ ∧ 𝐸 = 𝐷) ∧ π‘₯ ∈ 𝒫 (𝑉 βˆͺ {𝑋}) ∧ (β™―β€˜π‘₯) = 𝑀) ∧ π‘₯ ∈ 𝒫 𝑉) β†’ π‘₯ ∈ 𝒫 𝑉)
57 simpl3 1191 . . . . . . . 8 ((((πœ‘ ∧ 𝐸 = 𝐷) ∧ π‘₯ ∈ 𝒫 (𝑉 βˆͺ {𝑋}) ∧ (β™―β€˜π‘₯) = 𝑀) ∧ π‘₯ ∈ 𝒫 𝑉) β†’ (β™―β€˜π‘₯) = 𝑀)
58 rabid 3450 . . . . . . . 8 (π‘₯ ∈ {π‘₯ ∈ 𝒫 𝑉 ∣ (β™―β€˜π‘₯) = 𝑀} ↔ (π‘₯ ∈ 𝒫 𝑉 ∧ (β™―β€˜π‘₯) = 𝑀))
5956, 57, 58sylanbrc 581 . . . . . . 7 ((((πœ‘ ∧ 𝐸 = 𝐷) ∧ π‘₯ ∈ 𝒫 (𝑉 βˆͺ {𝑋}) ∧ (β™―β€˜π‘₯) = 𝑀) ∧ π‘₯ ∈ 𝒫 𝑉) β†’ π‘₯ ∈ {π‘₯ ∈ 𝒫 𝑉 ∣ (β™―β€˜π‘₯) = 𝑀})
6055, 59sseldd 3982 . . . . . 6 ((((πœ‘ ∧ 𝐸 = 𝐷) ∧ π‘₯ ∈ 𝒫 (𝑉 βˆͺ {𝑋}) ∧ (β™―β€˜π‘₯) = 𝑀) ∧ π‘₯ ∈ 𝒫 𝑉) β†’ π‘₯ ∈ (◑𝐾 β€œ {𝐸}))
61 simpl2 1190 . . . . . . . . . . . 12 ((((πœ‘ ∧ 𝐸 = 𝐷) ∧ π‘₯ ∈ 𝒫 (𝑉 βˆͺ {𝑋}) ∧ (β™―β€˜π‘₯) = 𝑀) ∧ Β¬ π‘₯ ∈ 𝒫 𝑉) β†’ π‘₯ ∈ 𝒫 (𝑉 βˆͺ {𝑋}))
6261elpwid 4610 . . . . . . . . . . 11 ((((πœ‘ ∧ 𝐸 = 𝐷) ∧ π‘₯ ∈ 𝒫 (𝑉 βˆͺ {𝑋}) ∧ (β™―β€˜π‘₯) = 𝑀) ∧ Β¬ π‘₯ ∈ 𝒫 𝑉) β†’ π‘₯ βŠ† (𝑉 βˆͺ {𝑋}))
63 simpl1l 1222 . . . . . . . . . . . 12 ((((πœ‘ ∧ 𝐸 = 𝐷) ∧ π‘₯ ∈ 𝒫 (𝑉 βˆͺ {𝑋}) ∧ (β™―β€˜π‘₯) = 𝑀) ∧ Β¬ π‘₯ ∈ 𝒫 𝑉) β†’ πœ‘)
6463, 8syl 17 . . . . . . . . . . 11 ((((πœ‘ ∧ 𝐸 = 𝐷) ∧ π‘₯ ∈ 𝒫 (𝑉 βˆͺ {𝑋}) ∧ (β™―β€˜π‘₯) = 𝑀) ∧ Β¬ π‘₯ ∈ 𝒫 𝑉) β†’ (𝑉 βˆͺ {𝑋}) βŠ† 𝑆)
6562, 64sstrd 3991 . . . . . . . . . 10 ((((πœ‘ ∧ 𝐸 = 𝐷) ∧ π‘₯ ∈ 𝒫 (𝑉 βˆͺ {𝑋}) ∧ (β™―β€˜π‘₯) = 𝑀) ∧ Β¬ π‘₯ ∈ 𝒫 𝑉) β†’ π‘₯ βŠ† 𝑆)
66 vex 3476 . . . . . . . . . . 11 π‘₯ ∈ V
6766elpw 4605 . . . . . . . . . 10 (π‘₯ ∈ 𝒫 𝑆 ↔ π‘₯ βŠ† 𝑆)
6865, 67sylibr 233 . . . . . . . . 9 ((((πœ‘ ∧ 𝐸 = 𝐷) ∧ π‘₯ ∈ 𝒫 (𝑉 βˆͺ {𝑋}) ∧ (β™―β€˜π‘₯) = 𝑀) ∧ Β¬ π‘₯ ∈ 𝒫 𝑉) β†’ π‘₯ ∈ 𝒫 𝑆)
69 simpl3 1191 . . . . . . . . 9 ((((πœ‘ ∧ 𝐸 = 𝐷) ∧ π‘₯ ∈ 𝒫 (𝑉 βˆͺ {𝑋}) ∧ (β™―β€˜π‘₯) = 𝑀) ∧ Β¬ π‘₯ ∈ 𝒫 𝑉) β†’ (β™―β€˜π‘₯) = 𝑀)
70 rabid 3450 . . . . . . . . 9 (π‘₯ ∈ {π‘₯ ∈ 𝒫 𝑆 ∣ (β™―β€˜π‘₯) = 𝑀} ↔ (π‘₯ ∈ 𝒫 𝑆 ∧ (β™―β€˜π‘₯) = 𝑀))
7168, 69, 70sylanbrc 581 . . . . . . . 8 ((((πœ‘ ∧ 𝐸 = 𝐷) ∧ π‘₯ ∈ 𝒫 (𝑉 βˆͺ {𝑋}) ∧ (β™―β€˜π‘₯) = 𝑀) ∧ Β¬ π‘₯ ∈ 𝒫 𝑉) β†’ π‘₯ ∈ {π‘₯ ∈ 𝒫 𝑆 ∣ (β™―β€˜π‘₯) = 𝑀})
7246hashbcval 16939 . . . . . . . . . 10 ((𝑆 ∈ Fin ∧ 𝑀 ∈ β„•0) β†’ (𝑆𝐢𝑀) = {π‘₯ ∈ 𝒫 𝑆 ∣ (β™―β€˜π‘₯) = 𝑀})
731, 45, 72syl2anc 582 . . . . . . . . 9 (πœ‘ β†’ (𝑆𝐢𝑀) = {π‘₯ ∈ 𝒫 𝑆 ∣ (β™―β€˜π‘₯) = 𝑀})
7463, 73syl 17 . . . . . . . 8 ((((πœ‘ ∧ 𝐸 = 𝐷) ∧ π‘₯ ∈ 𝒫 (𝑉 βˆͺ {𝑋}) ∧ (β™―β€˜π‘₯) = 𝑀) ∧ Β¬ π‘₯ ∈ 𝒫 𝑉) β†’ (𝑆𝐢𝑀) = {π‘₯ ∈ 𝒫 𝑆 ∣ (β™―β€˜π‘₯) = 𝑀})
7571, 74eleqtrrd 2834 . . . . . . 7 ((((πœ‘ ∧ 𝐸 = 𝐷) ∧ π‘₯ ∈ 𝒫 (𝑉 βˆͺ {𝑋}) ∧ (β™―β€˜π‘₯) = 𝑀) ∧ Β¬ π‘₯ ∈ 𝒫 𝑉) β†’ π‘₯ ∈ (𝑆𝐢𝑀))
763difss2d 4133 . . . . . . . . . . . . . . 15 (πœ‘ β†’ π‘Š βŠ† 𝑆)
771, 76ssfid 9269 . . . . . . . . . . . . . 14 (πœ‘ β†’ π‘Š ∈ Fin)
78 nnm1nn0 12517 . . . . . . . . . . . . . . 15 (𝑀 ∈ β„• β†’ (𝑀 βˆ’ 1) ∈ β„•0)
7944, 78syl 17 . . . . . . . . . . . . . 14 (πœ‘ β†’ (𝑀 βˆ’ 1) ∈ β„•0)
8046hashbcval 16939 . . . . . . . . . . . . . 14 ((π‘Š ∈ Fin ∧ (𝑀 βˆ’ 1) ∈ β„•0) β†’ (π‘ŠπΆ(𝑀 βˆ’ 1)) = {𝑒 ∈ 𝒫 π‘Š ∣ (β™―β€˜π‘’) = (𝑀 βˆ’ 1)})
8177, 79, 80syl2anc 582 . . . . . . . . . . . . 13 (πœ‘ β†’ (π‘ŠπΆ(𝑀 βˆ’ 1)) = {𝑒 ∈ 𝒫 π‘Š ∣ (β™―β€˜π‘’) = (𝑀 βˆ’ 1)})
82 ramub1.8 . . . . . . . . . . . . 13 (πœ‘ β†’ (π‘ŠπΆ(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝐷}))
8381, 82eqsstrrd 4020 . . . . . . . . . . . 12 (πœ‘ β†’ {𝑒 ∈ 𝒫 π‘Š ∣ (β™―β€˜π‘’) = (𝑀 βˆ’ 1)} βŠ† (◑𝐻 β€œ {𝐷}))
8463, 83syl 17 . . . . . . . . . . 11 ((((πœ‘ ∧ 𝐸 = 𝐷) ∧ π‘₯ ∈ 𝒫 (𝑉 βˆͺ {𝑋}) ∧ (β™―β€˜π‘₯) = 𝑀) ∧ Β¬ π‘₯ ∈ 𝒫 𝑉) β†’ {𝑒 ∈ 𝒫 π‘Š ∣ (β™―β€˜π‘’) = (𝑀 βˆ’ 1)} βŠ† (◑𝐻 β€œ {𝐷}))
85 fveqeq2 6899 . . . . . . . . . . . 12 (𝑒 = (π‘₯ βˆ– {𝑋}) β†’ ((β™―β€˜π‘’) = (𝑀 βˆ’ 1) ↔ (β™―β€˜(π‘₯ βˆ– {𝑋})) = (𝑀 βˆ’ 1)))
86 uncom 4152 . . . . . . . . . . . . . . . 16 (𝑉 βˆͺ {𝑋}) = ({𝑋} βˆͺ 𝑉)
8762, 86sseqtrdi 4031 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ 𝐸 = 𝐷) ∧ π‘₯ ∈ 𝒫 (𝑉 βˆͺ {𝑋}) ∧ (β™―β€˜π‘₯) = 𝑀) ∧ Β¬ π‘₯ ∈ 𝒫 𝑉) β†’ π‘₯ βŠ† ({𝑋} βˆͺ 𝑉))
88 ssundif 4486 . . . . . . . . . . . . . . 15 (π‘₯ βŠ† ({𝑋} βˆͺ 𝑉) ↔ (π‘₯ βˆ– {𝑋}) βŠ† 𝑉)
8987, 88sylib 217 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ 𝐸 = 𝐷) ∧ π‘₯ ∈ 𝒫 (𝑉 βˆͺ {𝑋}) ∧ (β™―β€˜π‘₯) = 𝑀) ∧ Β¬ π‘₯ ∈ 𝒫 𝑉) β†’ (π‘₯ βˆ– {𝑋}) βŠ† 𝑉)
9063, 2syl 17 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ 𝐸 = 𝐷) ∧ π‘₯ ∈ 𝒫 (𝑉 βˆͺ {𝑋}) ∧ (β™―β€˜π‘₯) = 𝑀) ∧ Β¬ π‘₯ ∈ 𝒫 𝑉) β†’ 𝑉 βŠ† π‘Š)
9189, 90sstrd 3991 . . . . . . . . . . . . 13 ((((πœ‘ ∧ 𝐸 = 𝐷) ∧ π‘₯ ∈ 𝒫 (𝑉 βˆͺ {𝑋}) ∧ (β™―β€˜π‘₯) = 𝑀) ∧ Β¬ π‘₯ ∈ 𝒫 𝑉) β†’ (π‘₯ βˆ– {𝑋}) βŠ† π‘Š)
9266difexi 5327 . . . . . . . . . . . . . 14 (π‘₯ βˆ– {𝑋}) ∈ V
9392elpw 4605 . . . . . . . . . . . . 13 ((π‘₯ βˆ– {𝑋}) ∈ 𝒫 π‘Š ↔ (π‘₯ βˆ– {𝑋}) βŠ† π‘Š)
9491, 93sylibr 233 . . . . . . . . . . . 12 ((((πœ‘ ∧ 𝐸 = 𝐷) ∧ π‘₯ ∈ 𝒫 (𝑉 βˆͺ {𝑋}) ∧ (β™―β€˜π‘₯) = 𝑀) ∧ Β¬ π‘₯ ∈ 𝒫 𝑉) β†’ (π‘₯ βˆ– {𝑋}) ∈ 𝒫 π‘Š)
9563, 1syl 17 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ 𝐸 = 𝐷) ∧ π‘₯ ∈ 𝒫 (𝑉 βˆͺ {𝑋}) ∧ (β™―β€˜π‘₯) = 𝑀) ∧ Β¬ π‘₯ ∈ 𝒫 𝑉) β†’ 𝑆 ∈ Fin)
9695, 65ssfid 9269 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ 𝐸 = 𝐷) ∧ π‘₯ ∈ 𝒫 (𝑉 βˆͺ {𝑋}) ∧ (β™―β€˜π‘₯) = 𝑀) ∧ Β¬ π‘₯ ∈ 𝒫 𝑉) β†’ π‘₯ ∈ Fin)
97 diffi 9181 . . . . . . . . . . . . . . . 16 (π‘₯ ∈ Fin β†’ (π‘₯ βˆ– {𝑋}) ∈ Fin)
9896, 97syl 17 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ 𝐸 = 𝐷) ∧ π‘₯ ∈ 𝒫 (𝑉 βˆͺ {𝑋}) ∧ (β™―β€˜π‘₯) = 𝑀) ∧ Β¬ π‘₯ ∈ 𝒫 𝑉) β†’ (π‘₯ βˆ– {𝑋}) ∈ Fin)
99 hashcl 14320 . . . . . . . . . . . . . . 15 ((π‘₯ βˆ– {𝑋}) ∈ Fin β†’ (β™―β€˜(π‘₯ βˆ– {𝑋})) ∈ β„•0)
100 nn0cn 12486 . . . . . . . . . . . . . . 15 ((β™―β€˜(π‘₯ βˆ– {𝑋})) ∈ β„•0 β†’ (β™―β€˜(π‘₯ βˆ– {𝑋})) ∈ β„‚)
10198, 99, 1003syl 18 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ 𝐸 = 𝐷) ∧ π‘₯ ∈ 𝒫 (𝑉 βˆͺ {𝑋}) ∧ (β™―β€˜π‘₯) = 𝑀) ∧ Β¬ π‘₯ ∈ 𝒫 𝑉) β†’ (β™―β€˜(π‘₯ βˆ– {𝑋})) ∈ β„‚)
102 ax-1cn 11170 . . . . . . . . . . . . . 14 1 ∈ β„‚
103 pncan 11470 . . . . . . . . . . . . . 14 (((β™―β€˜(π‘₯ βˆ– {𝑋})) ∈ β„‚ ∧ 1 ∈ β„‚) β†’ (((β™―β€˜(π‘₯ βˆ– {𝑋})) + 1) βˆ’ 1) = (β™―β€˜(π‘₯ βˆ– {𝑋})))
104101, 102, 103sylancl 584 . . . . . . . . . . . . 13 ((((πœ‘ ∧ 𝐸 = 𝐷) ∧ π‘₯ ∈ 𝒫 (𝑉 βˆͺ {𝑋}) ∧ (β™―β€˜π‘₯) = 𝑀) ∧ Β¬ π‘₯ ∈ 𝒫 𝑉) β†’ (((β™―β€˜(π‘₯ βˆ– {𝑋})) + 1) βˆ’ 1) = (β™―β€˜(π‘₯ βˆ– {𝑋})))
105 neldifsnd 4795 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ 𝐸 = 𝐷) ∧ π‘₯ ∈ 𝒫 (𝑉 βˆͺ {𝑋}) ∧ (β™―β€˜π‘₯) = 𝑀) ∧ Β¬ π‘₯ ∈ 𝒫 𝑉) β†’ Β¬ 𝑋 ∈ (π‘₯ βˆ– {𝑋}))
106 hashunsng 14356 . . . . . . . . . . . . . . . . 17 (𝑋 ∈ 𝑆 β†’ (((π‘₯ βˆ– {𝑋}) ∈ Fin ∧ Β¬ 𝑋 ∈ (π‘₯ βˆ– {𝑋})) β†’ (β™―β€˜((π‘₯ βˆ– {𝑋}) βˆͺ {𝑋})) = ((β™―β€˜(π‘₯ βˆ– {𝑋})) + 1)))
10763, 6, 1063syl 18 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ 𝐸 = 𝐷) ∧ π‘₯ ∈ 𝒫 (𝑉 βˆͺ {𝑋}) ∧ (β™―β€˜π‘₯) = 𝑀) ∧ Β¬ π‘₯ ∈ 𝒫 𝑉) β†’ (((π‘₯ βˆ– {𝑋}) ∈ Fin ∧ Β¬ 𝑋 ∈ (π‘₯ βˆ– {𝑋})) β†’ (β™―β€˜((π‘₯ βˆ– {𝑋}) βˆͺ {𝑋})) = ((β™―β€˜(π‘₯ βˆ– {𝑋})) + 1)))
10898, 105, 107mp2and 695 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ 𝐸 = 𝐷) ∧ π‘₯ ∈ 𝒫 (𝑉 βˆͺ {𝑋}) ∧ (β™―β€˜π‘₯) = 𝑀) ∧ Β¬ π‘₯ ∈ 𝒫 𝑉) β†’ (β™―β€˜((π‘₯ βˆ– {𝑋}) βˆͺ {𝑋})) = ((β™―β€˜(π‘₯ βˆ– {𝑋})) + 1))
109 undif1 4474 . . . . . . . . . . . . . . . . . 18 ((π‘₯ βˆ– {𝑋}) βˆͺ {𝑋}) = (π‘₯ βˆͺ {𝑋})
110 simpr 483 . . . . . . . . . . . . . . . . . . . . . 22 ((((πœ‘ ∧ 𝐸 = 𝐷) ∧ π‘₯ ∈ 𝒫 (𝑉 βˆͺ {𝑋}) ∧ (β™―β€˜π‘₯) = 𝑀) ∧ Β¬ π‘₯ ∈ 𝒫 𝑉) β†’ Β¬ π‘₯ ∈ 𝒫 𝑉)
11161, 110eldifd 3958 . . . . . . . . . . . . . . . . . . . . 21 ((((πœ‘ ∧ 𝐸 = 𝐷) ∧ π‘₯ ∈ 𝒫 (𝑉 βˆͺ {𝑋}) ∧ (β™―β€˜π‘₯) = 𝑀) ∧ Β¬ π‘₯ ∈ 𝒫 𝑉) β†’ π‘₯ ∈ (𝒫 (𝑉 βˆͺ {𝑋}) βˆ– 𝒫 𝑉))
112 elpwunsn 4686 . . . . . . . . . . . . . . . . . . . . 21 (π‘₯ ∈ (𝒫 (𝑉 βˆͺ {𝑋}) βˆ– 𝒫 𝑉) β†’ 𝑋 ∈ π‘₯)
113111, 112syl 17 . . . . . . . . . . . . . . . . . . . 20 ((((πœ‘ ∧ 𝐸 = 𝐷) ∧ π‘₯ ∈ 𝒫 (𝑉 βˆͺ {𝑋}) ∧ (β™―β€˜π‘₯) = 𝑀) ∧ Β¬ π‘₯ ∈ 𝒫 𝑉) β†’ 𝑋 ∈ π‘₯)
114113snssd 4811 . . . . . . . . . . . . . . . . . . 19 ((((πœ‘ ∧ 𝐸 = 𝐷) ∧ π‘₯ ∈ 𝒫 (𝑉 βˆͺ {𝑋}) ∧ (β™―β€˜π‘₯) = 𝑀) ∧ Β¬ π‘₯ ∈ 𝒫 𝑉) β†’ {𝑋} βŠ† π‘₯)
115 ssequn2 4182 . . . . . . . . . . . . . . . . . . 19 ({𝑋} βŠ† π‘₯ ↔ (π‘₯ βˆͺ {𝑋}) = π‘₯)
116114, 115sylib 217 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ 𝐸 = 𝐷) ∧ π‘₯ ∈ 𝒫 (𝑉 βˆͺ {𝑋}) ∧ (β™―β€˜π‘₯) = 𝑀) ∧ Β¬ π‘₯ ∈ 𝒫 𝑉) β†’ (π‘₯ βˆͺ {𝑋}) = π‘₯)
117109, 116eqtr2id 2783 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ 𝐸 = 𝐷) ∧ π‘₯ ∈ 𝒫 (𝑉 βˆͺ {𝑋}) ∧ (β™―β€˜π‘₯) = 𝑀) ∧ Β¬ π‘₯ ∈ 𝒫 𝑉) β†’ π‘₯ = ((π‘₯ βˆ– {𝑋}) βˆͺ {𝑋}))
118117fveq2d 6894 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ 𝐸 = 𝐷) ∧ π‘₯ ∈ 𝒫 (𝑉 βˆͺ {𝑋}) ∧ (β™―β€˜π‘₯) = 𝑀) ∧ Β¬ π‘₯ ∈ 𝒫 𝑉) β†’ (β™―β€˜π‘₯) = (β™―β€˜((π‘₯ βˆ– {𝑋}) βˆͺ {𝑋})))
119118, 69eqtr3d 2772 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ 𝐸 = 𝐷) ∧ π‘₯ ∈ 𝒫 (𝑉 βˆͺ {𝑋}) ∧ (β™―β€˜π‘₯) = 𝑀) ∧ Β¬ π‘₯ ∈ 𝒫 𝑉) β†’ (β™―β€˜((π‘₯ βˆ– {𝑋}) βˆͺ {𝑋})) = 𝑀)
120108, 119eqtr3d 2772 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ 𝐸 = 𝐷) ∧ π‘₯ ∈ 𝒫 (𝑉 βˆͺ {𝑋}) ∧ (β™―β€˜π‘₯) = 𝑀) ∧ Β¬ π‘₯ ∈ 𝒫 𝑉) β†’ ((β™―β€˜(π‘₯ βˆ– {𝑋})) + 1) = 𝑀)
121120oveq1d 7426 . . . . . . . . . . . . 13 ((((πœ‘ ∧ 𝐸 = 𝐷) ∧ π‘₯ ∈ 𝒫 (𝑉 βˆͺ {𝑋}) ∧ (β™―β€˜π‘₯) = 𝑀) ∧ Β¬ π‘₯ ∈ 𝒫 𝑉) β†’ (((β™―β€˜(π‘₯ βˆ– {𝑋})) + 1) βˆ’ 1) = (𝑀 βˆ’ 1))
122104, 121eqtr3d 2772 . . . . . . . . . . . 12 ((((πœ‘ ∧ 𝐸 = 𝐷) ∧ π‘₯ ∈ 𝒫 (𝑉 βˆͺ {𝑋}) ∧ (β™―β€˜π‘₯) = 𝑀) ∧ Β¬ π‘₯ ∈ 𝒫 𝑉) β†’ (β™―β€˜(π‘₯ βˆ– {𝑋})) = (𝑀 βˆ’ 1))
12385, 94, 122elrabd 3684 . . . . . . . . . . 11 ((((πœ‘ ∧ 𝐸 = 𝐷) ∧ π‘₯ ∈ 𝒫 (𝑉 βˆͺ {𝑋}) ∧ (β™―β€˜π‘₯) = 𝑀) ∧ Β¬ π‘₯ ∈ 𝒫 𝑉) β†’ (π‘₯ βˆ– {𝑋}) ∈ {𝑒 ∈ 𝒫 π‘Š ∣ (β™―β€˜π‘’) = (𝑀 βˆ’ 1)})
12484, 123sseldd 3982 . . . . . . . . . 10 ((((πœ‘ ∧ 𝐸 = 𝐷) ∧ π‘₯ ∈ 𝒫 (𝑉 βˆͺ {𝑋}) ∧ (β™―β€˜π‘₯) = 𝑀) ∧ Β¬ π‘₯ ∈ 𝒫 𝑉) β†’ (π‘₯ βˆ– {𝑋}) ∈ (◑𝐻 β€œ {𝐷}))
125 ramub1.h . . . . . . . . . . . 12 𝐻 = (𝑒 ∈ ((𝑆 βˆ– {𝑋})𝐢(𝑀 βˆ’ 1)) ↦ (πΎβ€˜(𝑒 βˆͺ {𝑋})))
126125mptiniseg 6237 . . . . . . . . . . 11 (𝐷 ∈ 𝑅 β†’ (◑𝐻 β€œ {𝐷}) = {𝑒 ∈ ((𝑆 βˆ– {𝑋})𝐢(𝑀 βˆ’ 1)) ∣ (πΎβ€˜(𝑒 βˆͺ {𝑋})) = 𝐷})
12763, 17, 1263syl 18 . . . . . . . . . 10 ((((πœ‘ ∧ 𝐸 = 𝐷) ∧ π‘₯ ∈ 𝒫 (𝑉 βˆͺ {𝑋}) ∧ (β™―β€˜π‘₯) = 𝑀) ∧ Β¬ π‘₯ ∈ 𝒫 𝑉) β†’ (◑𝐻 β€œ {𝐷}) = {𝑒 ∈ ((𝑆 βˆ– {𝑋})𝐢(𝑀 βˆ’ 1)) ∣ (πΎβ€˜(𝑒 βˆͺ {𝑋})) = 𝐷})
128124, 127eleqtrd 2833 . . . . . . . . 9 ((((πœ‘ ∧ 𝐸 = 𝐷) ∧ π‘₯ ∈ 𝒫 (𝑉 βˆͺ {𝑋}) ∧ (β™―β€˜π‘₯) = 𝑀) ∧ Β¬ π‘₯ ∈ 𝒫 𝑉) β†’ (π‘₯ βˆ– {𝑋}) ∈ {𝑒 ∈ ((𝑆 βˆ– {𝑋})𝐢(𝑀 βˆ’ 1)) ∣ (πΎβ€˜(𝑒 βˆͺ {𝑋})) = 𝐷})
129 uneq1 4155 . . . . . . . . . . . 12 (𝑒 = (π‘₯ βˆ– {𝑋}) β†’ (𝑒 βˆͺ {𝑋}) = ((π‘₯ βˆ– {𝑋}) βˆͺ {𝑋}))
130129fveqeq2d 6898 . . . . . . . . . . 11 (𝑒 = (π‘₯ βˆ– {𝑋}) β†’ ((πΎβ€˜(𝑒 βˆͺ {𝑋})) = 𝐷 ↔ (πΎβ€˜((π‘₯ βˆ– {𝑋}) βˆͺ {𝑋})) = 𝐷))
131130elrab 3682 . . . . . . . . . 10 ((π‘₯ βˆ– {𝑋}) ∈ {𝑒 ∈ ((𝑆 βˆ– {𝑋})𝐢(𝑀 βˆ’ 1)) ∣ (πΎβ€˜(𝑒 βˆͺ {𝑋})) = 𝐷} ↔ ((π‘₯ βˆ– {𝑋}) ∈ ((𝑆 βˆ– {𝑋})𝐢(𝑀 βˆ’ 1)) ∧ (πΎβ€˜((π‘₯ βˆ– {𝑋}) βˆͺ {𝑋})) = 𝐷))
132131simprbi 495 . . . . . . . . 9 ((π‘₯ βˆ– {𝑋}) ∈ {𝑒 ∈ ((𝑆 βˆ– {𝑋})𝐢(𝑀 βˆ’ 1)) ∣ (πΎβ€˜(𝑒 βˆͺ {𝑋})) = 𝐷} β†’ (πΎβ€˜((π‘₯ βˆ– {𝑋}) βˆͺ {𝑋})) = 𝐷)
133128, 132syl 17 . . . . . . . 8 ((((πœ‘ ∧ 𝐸 = 𝐷) ∧ π‘₯ ∈ 𝒫 (𝑉 βˆͺ {𝑋}) ∧ (β™―β€˜π‘₯) = 𝑀) ∧ Β¬ π‘₯ ∈ 𝒫 𝑉) β†’ (πΎβ€˜((π‘₯ βˆ– {𝑋}) βˆͺ {𝑋})) = 𝐷)
134117fveq2d 6894 . . . . . . . 8 ((((πœ‘ ∧ 𝐸 = 𝐷) ∧ π‘₯ ∈ 𝒫 (𝑉 βˆͺ {𝑋}) ∧ (β™―β€˜π‘₯) = 𝑀) ∧ Β¬ π‘₯ ∈ 𝒫 𝑉) β†’ (πΎβ€˜π‘₯) = (πΎβ€˜((π‘₯ βˆ– {𝑋}) βˆͺ {𝑋})))
135 simpl1r 1223 . . . . . . . 8 ((((πœ‘ ∧ 𝐸 = 𝐷) ∧ π‘₯ ∈ 𝒫 (𝑉 βˆͺ {𝑋}) ∧ (β™―β€˜π‘₯) = 𝑀) ∧ Β¬ π‘₯ ∈ 𝒫 𝑉) β†’ 𝐸 = 𝐷)
136133, 134, 1353eqtr4d 2780 . . . . . . 7 ((((πœ‘ ∧ 𝐸 = 𝐷) ∧ π‘₯ ∈ 𝒫 (𝑉 βˆͺ {𝑋}) ∧ (β™―β€˜π‘₯) = 𝑀) ∧ Β¬ π‘₯ ∈ 𝒫 𝑉) β†’ (πΎβ€˜π‘₯) = 𝐸)
137 ramub1.6 . . . . . . . . 9 (πœ‘ β†’ 𝐾:(𝑆𝐢𝑀)βŸΆπ‘…)
138137ffnd 6717 . . . . . . . 8 (πœ‘ β†’ 𝐾 Fn (𝑆𝐢𝑀))
139 fniniseg 7060 . . . . . . . 8 (𝐾 Fn (𝑆𝐢𝑀) β†’ (π‘₯ ∈ (◑𝐾 β€œ {𝐸}) ↔ (π‘₯ ∈ (𝑆𝐢𝑀) ∧ (πΎβ€˜π‘₯) = 𝐸)))
14063, 138, 1393syl 18 . . . . . . 7 ((((πœ‘ ∧ 𝐸 = 𝐷) ∧ π‘₯ ∈ 𝒫 (𝑉 βˆͺ {𝑋}) ∧ (β™―β€˜π‘₯) = 𝑀) ∧ Β¬ π‘₯ ∈ 𝒫 𝑉) β†’ (π‘₯ ∈ (◑𝐾 β€œ {𝐸}) ↔ (π‘₯ ∈ (𝑆𝐢𝑀) ∧ (πΎβ€˜π‘₯) = 𝐸)))
14175, 136, 140mpbir2and 709 . . . . . 6 ((((πœ‘ ∧ 𝐸 = 𝐷) ∧ π‘₯ ∈ 𝒫 (𝑉 βˆͺ {𝑋}) ∧ (β™―β€˜π‘₯) = 𝑀) ∧ Β¬ π‘₯ ∈ 𝒫 𝑉) β†’ π‘₯ ∈ (◑𝐾 β€œ {𝐸}))
14260, 141pm2.61dan 809 . . . . 5 (((πœ‘ ∧ 𝐸 = 𝐷) ∧ π‘₯ ∈ 𝒫 (𝑉 βˆͺ {𝑋}) ∧ (β™―β€˜π‘₯) = 𝑀) β†’ π‘₯ ∈ (◑𝐾 β€œ {𝐸}))
143142rabssdv 4071 . . . 4 ((πœ‘ ∧ 𝐸 = 𝐷) β†’ {π‘₯ ∈ 𝒫 (𝑉 βˆͺ {𝑋}) ∣ (β™―β€˜π‘₯) = 𝑀} βŠ† (◑𝐾 β€œ {𝐸}))
14449, 143eqsstrd 4019 . . 3 ((πœ‘ ∧ 𝐸 = 𝐷) β†’ ((𝑉 βˆͺ {𝑋})𝐢𝑀) βŠ† (◑𝐾 β€œ {𝐸}))
145 fveq2 6890 . . . . . 6 (𝑧 = (𝑉 βˆͺ {𝑋}) β†’ (β™―β€˜π‘§) = (β™―β€˜(𝑉 βˆͺ {𝑋})))
146145breq2d 5159 . . . . 5 (𝑧 = (𝑉 βˆͺ {𝑋}) β†’ ((πΉβ€˜πΈ) ≀ (β™―β€˜π‘§) ↔ (πΉβ€˜πΈ) ≀ (β™―β€˜(𝑉 βˆͺ {𝑋}))))
147 oveq1 7418 . . . . . 6 (𝑧 = (𝑉 βˆͺ {𝑋}) β†’ (𝑧𝐢𝑀) = ((𝑉 βˆͺ {𝑋})𝐢𝑀))
148147sseq1d 4012 . . . . 5 (𝑧 = (𝑉 βˆͺ {𝑋}) β†’ ((𝑧𝐢𝑀) βŠ† (◑𝐾 β€œ {𝐸}) ↔ ((𝑉 βˆͺ {𝑋})𝐢𝑀) βŠ† (◑𝐾 β€œ {𝐸})))
149146, 148anbi12d 629 . . . 4 (𝑧 = (𝑉 βˆͺ {𝑋}) β†’ (((πΉβ€˜πΈ) ≀ (β™―β€˜π‘§) ∧ (𝑧𝐢𝑀) βŠ† (◑𝐾 β€œ {𝐸})) ↔ ((πΉβ€˜πΈ) ≀ (β™―β€˜(𝑉 βˆͺ {𝑋})) ∧ ((𝑉 βˆͺ {𝑋})𝐢𝑀) βŠ† (◑𝐾 β€œ {𝐸}))))
150149rspcev 3611 . . 3 (((𝑉 βˆͺ {𝑋}) ∈ 𝒫 𝑆 ∧ ((πΉβ€˜πΈ) ≀ (β™―β€˜(𝑉 βˆͺ {𝑋})) ∧ ((𝑉 βˆͺ {𝑋})𝐢𝑀) βŠ† (◑𝐾 β€œ {𝐸}))) β†’ βˆƒπ‘§ ∈ 𝒫 𝑆((πΉβ€˜πΈ) ≀ (β™―β€˜π‘§) ∧ (𝑧𝐢𝑀) βŠ† (◑𝐾 β€œ {𝐸})))
15110, 40, 144, 150syl12anc 833 . 2 ((πœ‘ ∧ 𝐸 = 𝐷) β†’ βˆƒπ‘§ ∈ 𝒫 𝑆((πΉβ€˜πΈ) ≀ (β™―β€˜π‘§) ∧ (𝑧𝐢𝑀) βŠ† (◑𝐾 β€œ {𝐸})))
1521, 5sselpwd 5325 . . . 4 (πœ‘ β†’ 𝑉 ∈ 𝒫 𝑆)
153152adantr 479 . . 3 ((πœ‘ ∧ 𝐸 β‰  𝐷) β†’ 𝑉 ∈ 𝒫 𝑆)
154 ifnefalse 4539 . . . . 5 (𝐸 β‰  𝐷 β†’ if(𝐸 = 𝐷, ((πΉβ€˜π·) βˆ’ 1), (πΉβ€˜πΈ)) = (πΉβ€˜πΈ))
155154adantl 480 . . . 4 ((πœ‘ ∧ 𝐸 β‰  𝐷) β†’ if(𝐸 = 𝐷, ((πΉβ€˜π·) βˆ’ 1), (πΉβ€˜πΈ)) = (πΉβ€˜πΈ))
15613adantr 479 . . . 4 ((πœ‘ ∧ 𝐸 β‰  𝐷) β†’ if(𝐸 = 𝐷, ((πΉβ€˜π·) βˆ’ 1), (πΉβ€˜πΈ)) ≀ (β™―β€˜π‘‰))
157155, 156eqbrtrrd 5171 . . 3 ((πœ‘ ∧ 𝐸 β‰  𝐷) β†’ (πΉβ€˜πΈ) ≀ (β™―β€˜π‘‰))
15853adantr 479 . . 3 ((πœ‘ ∧ 𝐸 β‰  𝐷) β†’ (𝑉𝐢𝑀) βŠ† (◑𝐾 β€œ {𝐸}))
159 fveq2 6890 . . . . . 6 (𝑧 = 𝑉 β†’ (β™―β€˜π‘§) = (β™―β€˜π‘‰))
160159breq2d 5159 . . . . 5 (𝑧 = 𝑉 β†’ ((πΉβ€˜πΈ) ≀ (β™―β€˜π‘§) ↔ (πΉβ€˜πΈ) ≀ (β™―β€˜π‘‰)))
161 oveq1 7418 . . . . . 6 (𝑧 = 𝑉 β†’ (𝑧𝐢𝑀) = (𝑉𝐢𝑀))
162161sseq1d 4012 . . . . 5 (𝑧 = 𝑉 β†’ ((𝑧𝐢𝑀) βŠ† (◑𝐾 β€œ {𝐸}) ↔ (𝑉𝐢𝑀) βŠ† (◑𝐾 β€œ {𝐸})))
163160, 162anbi12d 629 . . . 4 (𝑧 = 𝑉 β†’ (((πΉβ€˜πΈ) ≀ (β™―β€˜π‘§) ∧ (𝑧𝐢𝑀) βŠ† (◑𝐾 β€œ {𝐸})) ↔ ((πΉβ€˜πΈ) ≀ (β™―β€˜π‘‰) ∧ (𝑉𝐢𝑀) βŠ† (◑𝐾 β€œ {𝐸}))))
164163rspcev 3611 . . 3 ((𝑉 ∈ 𝒫 𝑆 ∧ ((πΉβ€˜πΈ) ≀ (β™―β€˜π‘‰) ∧ (𝑉𝐢𝑀) βŠ† (◑𝐾 β€œ {𝐸}))) β†’ βˆƒπ‘§ ∈ 𝒫 𝑆((πΉβ€˜πΈ) ≀ (β™―β€˜π‘§) ∧ (𝑧𝐢𝑀) βŠ† (◑𝐾 β€œ {𝐸})))
165153, 157, 158, 164syl12anc 833 . 2 ((πœ‘ ∧ 𝐸 β‰  𝐷) β†’ βˆƒπ‘§ ∈ 𝒫 𝑆((πΉβ€˜πΈ) ≀ (β™―β€˜π‘§) ∧ (𝑧𝐢𝑀) βŠ† (◑𝐾 β€œ {𝐸})))
166151, 165pm2.61dane 3027 1 (πœ‘ β†’ βˆƒπ‘§ ∈ 𝒫 𝑆((πΉβ€˜πΈ) ≀ (β™―β€˜π‘§) ∧ (𝑧𝐢𝑀) βŠ† (◑𝐾 β€œ {𝐸})))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 394   ∧ w3a 1085   = wceq 1539   ∈ wcel 2104   β‰  wne 2938  βˆƒwrex 3068  {crab 3430  Vcvv 3472   βˆ– cdif 3944   βˆͺ cun 3945   βŠ† wss 3947  ifcif 4527  π’« cpw 4601  {csn 4627   class class class wbr 5147   ↦ cmpt 5230  β—‘ccnv 5674   β€œ cima 5678   Fn wfn 6537  βŸΆwf 6538  β€˜cfv 6542  (class class class)co 7411   ∈ cmpo 7413  Fincfn 8941  β„‚cc 11110  β„cr 11111  1c1 11113   + caddc 11115   ≀ cle 11253   βˆ’ cmin 11448  β„•cn 12216  β„•0cn0 12476  β™―chash 14294   Ramsey cram 16936
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7727  ax-cnex 11168  ax-resscn 11169  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-addrcl 11173  ax-mulcl 11174  ax-mulrcl 11175  ax-mulcom 11176  ax-addass 11177  ax-mulass 11178  ax-distr 11179  ax-i2m1 11180  ax-1ne0 11181  ax-1rid 11182  ax-rnegex 11183  ax-rrecex 11184  ax-cnre 11185  ax-pre-lttri 11186  ax-pre-lttrn 11187  ax-pre-ltadd 11188  ax-pre-mulgt0 11189
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-reu 3375  df-rab 3431  df-v 3474  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-int 4950  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6299  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-riota 7367  df-ov 7414  df-oprab 7415  df-mpo 7416  df-om 7858  df-1st 7977  df-2nd 7978  df-frecs 8268  df-wrecs 8299  df-recs 8373  df-rdg 8412  df-1o 8468  df-oadd 8472  df-er 8705  df-en 8942  df-dom 8943  df-sdom 8944  df-fin 8945  df-dju 9898  df-card 9936  df-pnf 11254  df-mnf 11255  df-xr 11256  df-ltxr 11257  df-le 11258  df-sub 11450  df-neg 11451  df-nn 12217  df-n0 12477  df-z 12563  df-uz 12827  df-fz 13489  df-hash 14295
This theorem is referenced by:  ramub1lem2  16964
  Copyright terms: Public domain W3C validator