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

Theorem ramub1lem2 16769
Description: Lemma for ramub1 16770. (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)) ↦ (πΎβ€˜(𝑒 βˆͺ {𝑋})))
Assertion
Ref Expression
ramub1lem2 (πœ‘ β†’ βˆƒπ‘ ∈ 𝑅 βˆƒπ‘§ ∈ 𝒫 𝑆((πΉβ€˜π‘) ≀ (β™―β€˜π‘§) ∧ (𝑧𝐢𝑀) βŠ† (◑𝐾 β€œ {𝑐})))
Distinct variable groups:   π‘₯,𝑒,𝑐,𝑦,𝑧,𝐹   π‘Ž,𝑏,𝑐,𝑖,𝑒,π‘₯,𝑦,𝑧,𝑀   𝐺,π‘Ž,𝑐,𝑖,𝑒,π‘₯,𝑦,𝑧   𝑅,𝑐,𝑒,π‘₯,𝑦,𝑧   πœ‘,𝑐,𝑒,π‘₯,𝑦,𝑧   𝑆,π‘Ž,𝑐,𝑖,𝑒,π‘₯,𝑦,𝑧   𝐢,𝑐,𝑒,π‘₯,𝑦,𝑧   𝐻,𝑐,𝑒,π‘₯,𝑦,𝑧   𝐾,𝑐,𝑒,π‘₯,𝑦,𝑧   𝑋,π‘Ž,𝑐,𝑖,𝑒,π‘₯,𝑦,𝑧
Allowed substitution hints:   πœ‘(𝑖,π‘Ž,𝑏)   𝐢(𝑖,π‘Ž,𝑏)   𝑅(𝑖,π‘Ž,𝑏)   𝑆(𝑏)   𝐹(𝑖,π‘Ž,𝑏)   𝐺(𝑏)   𝐻(𝑖,π‘Ž,𝑏)   𝐾(𝑖,π‘Ž,𝑏)   𝑋(𝑏)

Proof of Theorem ramub1lem2
Dummy variables 𝑑 𝑣 𝑀 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ramub1.3 . . 3 𝐢 = (π‘Ž ∈ V, 𝑖 ∈ β„•0 ↦ {𝑏 ∈ 𝒫 π‘Ž ∣ (β™―β€˜π‘) = 𝑖})
2 ramub1.m . . . 4 (πœ‘ β†’ 𝑀 ∈ β„•)
3 nnm1nn0 12316 . . . 4 (𝑀 ∈ β„• β†’ (𝑀 βˆ’ 1) ∈ β„•0)
42, 3syl 17 . . 3 (πœ‘ β†’ (𝑀 βˆ’ 1) ∈ β„•0)
5 ramub1.r . . 3 (πœ‘ β†’ 𝑅 ∈ Fin)
6 ramub1.1 . . 3 (πœ‘ β†’ 𝐺:π‘…βŸΆβ„•0)
7 ramub1.2 . . 3 (πœ‘ β†’ ((𝑀 βˆ’ 1) Ramsey 𝐺) ∈ β„•0)
8 ramub1.4 . . . 4 (πœ‘ β†’ 𝑆 ∈ Fin)
9 diffi 8996 . . . 4 (𝑆 ∈ Fin β†’ (𝑆 βˆ– {𝑋}) ∈ Fin)
108, 9syl 17 . . 3 (πœ‘ β†’ (𝑆 βˆ– {𝑋}) ∈ Fin)
117nn0red 12336 . . . . 5 (πœ‘ β†’ ((𝑀 βˆ’ 1) Ramsey 𝐺) ∈ ℝ)
1211leidd 11583 . . . 4 (πœ‘ β†’ ((𝑀 βˆ’ 1) Ramsey 𝐺) ≀ ((𝑀 βˆ’ 1) Ramsey 𝐺))
13 hashcl 14112 . . . . . . 7 ((𝑆 βˆ– {𝑋}) ∈ Fin β†’ (β™―β€˜(𝑆 βˆ– {𝑋})) ∈ β„•0)
1410, 13syl 17 . . . . . 6 (πœ‘ β†’ (β™―β€˜(𝑆 βˆ– {𝑋})) ∈ β„•0)
1514nn0cnd 12337 . . . . 5 (πœ‘ β†’ (β™―β€˜(𝑆 βˆ– {𝑋})) ∈ β„‚)
167nn0cnd 12337 . . . . 5 (πœ‘ β†’ ((𝑀 βˆ’ 1) Ramsey 𝐺) ∈ β„‚)
17 1cnd 11012 . . . . 5 (πœ‘ β†’ 1 ∈ β„‚)
18 undif1 4415 . . . . . . . 8 ((𝑆 βˆ– {𝑋}) βˆͺ {𝑋}) = (𝑆 βˆͺ {𝑋})
19 ramub1.x . . . . . . . . . 10 (πœ‘ β†’ 𝑋 ∈ 𝑆)
2019snssd 4748 . . . . . . . . 9 (πœ‘ β†’ {𝑋} βŠ† 𝑆)
21 ssequn2 4123 . . . . . . . . 9 ({𝑋} βŠ† 𝑆 ↔ (𝑆 βˆͺ {𝑋}) = 𝑆)
2220, 21sylib 217 . . . . . . . 8 (πœ‘ β†’ (𝑆 βˆͺ {𝑋}) = 𝑆)
2318, 22eqtrid 2788 . . . . . . 7 (πœ‘ β†’ ((𝑆 βˆ– {𝑋}) βˆͺ {𝑋}) = 𝑆)
2423fveq2d 6804 . . . . . 6 (πœ‘ β†’ (β™―β€˜((𝑆 βˆ– {𝑋}) βˆͺ {𝑋})) = (β™―β€˜π‘†))
25 neldifsnd 4732 . . . . . . 7 (πœ‘ β†’ Β¬ 𝑋 ∈ (𝑆 βˆ– {𝑋}))
26 hashunsng 14148 . . . . . . . 8 (𝑋 ∈ 𝑆 β†’ (((𝑆 βˆ– {𝑋}) ∈ Fin ∧ Β¬ 𝑋 ∈ (𝑆 βˆ– {𝑋})) β†’ (β™―β€˜((𝑆 βˆ– {𝑋}) βˆͺ {𝑋})) = ((β™―β€˜(𝑆 βˆ– {𝑋})) + 1)))
2719, 26syl 17 . . . . . . 7 (πœ‘ β†’ (((𝑆 βˆ– {𝑋}) ∈ Fin ∧ Β¬ 𝑋 ∈ (𝑆 βˆ– {𝑋})) β†’ (β™―β€˜((𝑆 βˆ– {𝑋}) βˆͺ {𝑋})) = ((β™―β€˜(𝑆 βˆ– {𝑋})) + 1)))
2810, 25, 27mp2and 697 . . . . . 6 (πœ‘ β†’ (β™―β€˜((𝑆 βˆ– {𝑋}) βˆͺ {𝑋})) = ((β™―β€˜(𝑆 βˆ– {𝑋})) + 1))
29 ramub1.5 . . . . . 6 (πœ‘ β†’ (β™―β€˜π‘†) = (((𝑀 βˆ’ 1) Ramsey 𝐺) + 1))
3024, 28, 293eqtr3d 2784 . . . . 5 (πœ‘ β†’ ((β™―β€˜(𝑆 βˆ– {𝑋})) + 1) = (((𝑀 βˆ’ 1) Ramsey 𝐺) + 1))
3115, 16, 17, 30addcan2ad 11223 . . . 4 (πœ‘ β†’ (β™―β€˜(𝑆 βˆ– {𝑋})) = ((𝑀 βˆ’ 1) Ramsey 𝐺))
3212, 31breqtrrd 5109 . . 3 (πœ‘ β†’ ((𝑀 βˆ’ 1) Ramsey 𝐺) ≀ (β™―β€˜(𝑆 βˆ– {𝑋})))
33 ramub1.6 . . . . . 6 (πœ‘ β†’ 𝐾:(𝑆𝐢𝑀)βŸΆπ‘…)
3433adantr 482 . . . . 5 ((πœ‘ ∧ 𝑒 ∈ ((𝑆 βˆ– {𝑋})𝐢(𝑀 βˆ’ 1))) β†’ 𝐾:(𝑆𝐢𝑀)βŸΆπ‘…)
35 fveqeq2 6809 . . . . . . 7 (π‘₯ = (𝑒 βˆͺ {𝑋}) β†’ ((β™―β€˜π‘₯) = 𝑀 ↔ (β™―β€˜(𝑒 βˆͺ {𝑋})) = 𝑀))
361hashbcval 16744 . . . . . . . . . . . . . . 15 (((𝑆 βˆ– {𝑋}) ∈ Fin ∧ (𝑀 βˆ’ 1) ∈ β„•0) β†’ ((𝑆 βˆ– {𝑋})𝐢(𝑀 βˆ’ 1)) = {π‘₯ ∈ 𝒫 (𝑆 βˆ– {𝑋}) ∣ (β™―β€˜π‘₯) = (𝑀 βˆ’ 1)})
3710, 4, 36syl2anc 585 . . . . . . . . . . . . . 14 (πœ‘ β†’ ((𝑆 βˆ– {𝑋})𝐢(𝑀 βˆ’ 1)) = {π‘₯ ∈ 𝒫 (𝑆 βˆ– {𝑋}) ∣ (β™―β€˜π‘₯) = (𝑀 βˆ’ 1)})
3837eleq2d 2822 . . . . . . . . . . . . 13 (πœ‘ β†’ (𝑒 ∈ ((𝑆 βˆ– {𝑋})𝐢(𝑀 βˆ’ 1)) ↔ 𝑒 ∈ {π‘₯ ∈ 𝒫 (𝑆 βˆ– {𝑋}) ∣ (β™―β€˜π‘₯) = (𝑀 βˆ’ 1)}))
39 fveqeq2 6809 . . . . . . . . . . . . . 14 (π‘₯ = 𝑒 β†’ ((β™―β€˜π‘₯) = (𝑀 βˆ’ 1) ↔ (β™―β€˜π‘’) = (𝑀 βˆ’ 1)))
4039elrab 3629 . . . . . . . . . . . . 13 (𝑒 ∈ {π‘₯ ∈ 𝒫 (𝑆 βˆ– {𝑋}) ∣ (β™―β€˜π‘₯) = (𝑀 βˆ’ 1)} ↔ (𝑒 ∈ 𝒫 (𝑆 βˆ– {𝑋}) ∧ (β™―β€˜π‘’) = (𝑀 βˆ’ 1)))
4138, 40bitrdi 288 . . . . . . . . . . . 12 (πœ‘ β†’ (𝑒 ∈ ((𝑆 βˆ– {𝑋})𝐢(𝑀 βˆ’ 1)) ↔ (𝑒 ∈ 𝒫 (𝑆 βˆ– {𝑋}) ∧ (β™―β€˜π‘’) = (𝑀 βˆ’ 1))))
4241simprbda 500 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑒 ∈ ((𝑆 βˆ– {𝑋})𝐢(𝑀 βˆ’ 1))) β†’ 𝑒 ∈ 𝒫 (𝑆 βˆ– {𝑋}))
4342elpwid 4548 . . . . . . . . . 10 ((πœ‘ ∧ 𝑒 ∈ ((𝑆 βˆ– {𝑋})𝐢(𝑀 βˆ’ 1))) β†’ 𝑒 βŠ† (𝑆 βˆ– {𝑋}))
4443difss2d 4075 . . . . . . . . 9 ((πœ‘ ∧ 𝑒 ∈ ((𝑆 βˆ– {𝑋})𝐢(𝑀 βˆ’ 1))) β†’ 𝑒 βŠ† 𝑆)
4520adantr 482 . . . . . . . . 9 ((πœ‘ ∧ 𝑒 ∈ ((𝑆 βˆ– {𝑋})𝐢(𝑀 βˆ’ 1))) β†’ {𝑋} βŠ† 𝑆)
4644, 45unssd 4126 . . . . . . . 8 ((πœ‘ ∧ 𝑒 ∈ ((𝑆 βˆ– {𝑋})𝐢(𝑀 βˆ’ 1))) β†’ (𝑒 βˆͺ {𝑋}) βŠ† 𝑆)
47 vex 3441 . . . . . . . . . 10 𝑒 ∈ V
48 snex 5363 . . . . . . . . . 10 {𝑋} ∈ V
4947, 48unex 7624 . . . . . . . . 9 (𝑒 βˆͺ {𝑋}) ∈ V
5049elpw 4543 . . . . . . . 8 ((𝑒 βˆͺ {𝑋}) ∈ 𝒫 𝑆 ↔ (𝑒 βˆͺ {𝑋}) βŠ† 𝑆)
5146, 50sylibr 234 . . . . . . 7 ((πœ‘ ∧ 𝑒 ∈ ((𝑆 βˆ– {𝑋})𝐢(𝑀 βˆ’ 1))) β†’ (𝑒 βˆͺ {𝑋}) ∈ 𝒫 𝑆)
5210adantr 482 . . . . . . . . . 10 ((πœ‘ ∧ 𝑒 ∈ ((𝑆 βˆ– {𝑋})𝐢(𝑀 βˆ’ 1))) β†’ (𝑆 βˆ– {𝑋}) ∈ Fin)
5352, 43ssfid 9082 . . . . . . . . 9 ((πœ‘ ∧ 𝑒 ∈ ((𝑆 βˆ– {𝑋})𝐢(𝑀 βˆ’ 1))) β†’ 𝑒 ∈ Fin)
54 neldifsnd 4732 . . . . . . . . . 10 ((πœ‘ ∧ 𝑒 ∈ ((𝑆 βˆ– {𝑋})𝐢(𝑀 βˆ’ 1))) β†’ Β¬ 𝑋 ∈ (𝑆 βˆ– {𝑋}))
5543, 54ssneldd 3929 . . . . . . . . 9 ((πœ‘ ∧ 𝑒 ∈ ((𝑆 βˆ– {𝑋})𝐢(𝑀 βˆ’ 1))) β†’ Β¬ 𝑋 ∈ 𝑒)
5619adantr 482 . . . . . . . . . 10 ((πœ‘ ∧ 𝑒 ∈ ((𝑆 βˆ– {𝑋})𝐢(𝑀 βˆ’ 1))) β†’ 𝑋 ∈ 𝑆)
57 hashunsng 14148 . . . . . . . . . 10 (𝑋 ∈ 𝑆 β†’ ((𝑒 ∈ Fin ∧ Β¬ 𝑋 ∈ 𝑒) β†’ (β™―β€˜(𝑒 βˆͺ {𝑋})) = ((β™―β€˜π‘’) + 1)))
5856, 57syl 17 . . . . . . . . 9 ((πœ‘ ∧ 𝑒 ∈ ((𝑆 βˆ– {𝑋})𝐢(𝑀 βˆ’ 1))) β†’ ((𝑒 ∈ Fin ∧ Β¬ 𝑋 ∈ 𝑒) β†’ (β™―β€˜(𝑒 βˆͺ {𝑋})) = ((β™―β€˜π‘’) + 1)))
5953, 55, 58mp2and 697 . . . . . . . 8 ((πœ‘ ∧ 𝑒 ∈ ((𝑆 βˆ– {𝑋})𝐢(𝑀 βˆ’ 1))) β†’ (β™―β€˜(𝑒 βˆͺ {𝑋})) = ((β™―β€˜π‘’) + 1))
6041simplbda 501 . . . . . . . . 9 ((πœ‘ ∧ 𝑒 ∈ ((𝑆 βˆ– {𝑋})𝐢(𝑀 βˆ’ 1))) β†’ (β™―β€˜π‘’) = (𝑀 βˆ’ 1))
6160oveq1d 7318 . . . . . . . 8 ((πœ‘ ∧ 𝑒 ∈ ((𝑆 βˆ– {𝑋})𝐢(𝑀 βˆ’ 1))) β†’ ((β™―β€˜π‘’) + 1) = ((𝑀 βˆ’ 1) + 1))
622nncnd 12031 . . . . . . . . . 10 (πœ‘ β†’ 𝑀 ∈ β„‚)
63 ax-1cn 10971 . . . . . . . . . 10 1 ∈ β„‚
64 npcan 11272 . . . . . . . . . 10 ((𝑀 ∈ β„‚ ∧ 1 ∈ β„‚) β†’ ((𝑀 βˆ’ 1) + 1) = 𝑀)
6562, 63, 64sylancl 587 . . . . . . . . 9 (πœ‘ β†’ ((𝑀 βˆ’ 1) + 1) = 𝑀)
6665adantr 482 . . . . . . . 8 ((πœ‘ ∧ 𝑒 ∈ ((𝑆 βˆ– {𝑋})𝐢(𝑀 βˆ’ 1))) β†’ ((𝑀 βˆ’ 1) + 1) = 𝑀)
6759, 61, 663eqtrd 2780 . . . . . . 7 ((πœ‘ ∧ 𝑒 ∈ ((𝑆 βˆ– {𝑋})𝐢(𝑀 βˆ’ 1))) β†’ (β™―β€˜(𝑒 βˆͺ {𝑋})) = 𝑀)
6835, 51, 67elrabd 3631 . . . . . 6 ((πœ‘ ∧ 𝑒 ∈ ((𝑆 βˆ– {𝑋})𝐢(𝑀 βˆ’ 1))) β†’ (𝑒 βˆͺ {𝑋}) ∈ {π‘₯ ∈ 𝒫 𝑆 ∣ (β™―β€˜π‘₯) = 𝑀})
692nnnn0d 12335 . . . . . . . 8 (πœ‘ β†’ 𝑀 ∈ β„•0)
701hashbcval 16744 . . . . . . . 8 ((𝑆 ∈ Fin ∧ 𝑀 ∈ β„•0) β†’ (𝑆𝐢𝑀) = {π‘₯ ∈ 𝒫 𝑆 ∣ (β™―β€˜π‘₯) = 𝑀})
718, 69, 70syl2anc 585 . . . . . . 7 (πœ‘ β†’ (𝑆𝐢𝑀) = {π‘₯ ∈ 𝒫 𝑆 ∣ (β™―β€˜π‘₯) = 𝑀})
7271adantr 482 . . . . . 6 ((πœ‘ ∧ 𝑒 ∈ ((𝑆 βˆ– {𝑋})𝐢(𝑀 βˆ’ 1))) β†’ (𝑆𝐢𝑀) = {π‘₯ ∈ 𝒫 𝑆 ∣ (β™―β€˜π‘₯) = 𝑀})
7368, 72eleqtrrd 2840 . . . . 5 ((πœ‘ ∧ 𝑒 ∈ ((𝑆 βˆ– {𝑋})𝐢(𝑀 βˆ’ 1))) β†’ (𝑒 βˆͺ {𝑋}) ∈ (𝑆𝐢𝑀))
7434, 73ffvelcdmd 6990 . . . 4 ((πœ‘ ∧ 𝑒 ∈ ((𝑆 βˆ– {𝑋})𝐢(𝑀 βˆ’ 1))) β†’ (πΎβ€˜(𝑒 βˆͺ {𝑋})) ∈ 𝑅)
75 ramub1.h . . . 4 𝐻 = (𝑒 ∈ ((𝑆 βˆ– {𝑋})𝐢(𝑀 βˆ’ 1)) ↦ (πΎβ€˜(𝑒 βˆͺ {𝑋})))
7674, 75fmptd 7016 . . 3 (πœ‘ β†’ 𝐻:((𝑆 βˆ– {𝑋})𝐢(𝑀 βˆ’ 1))βŸΆπ‘…)
771, 4, 5, 6, 7, 10, 32, 76rami 16757 . 2 (πœ‘ β†’ βˆƒπ‘‘ ∈ 𝑅 βˆƒπ‘€ ∈ 𝒫 (𝑆 βˆ– {𝑋})((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))
7869adantr 482 . . . . . 6 ((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) β†’ 𝑀 ∈ β„•0)
795adantr 482 . . . . . 6 ((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) β†’ 𝑅 ∈ Fin)
80 ramub1.f . . . . . . . . . . . 12 (πœ‘ β†’ 𝐹:π‘…βŸΆβ„•)
8180adantr 482 . . . . . . . . . . 11 ((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) β†’ 𝐹:π‘…βŸΆβ„•)
82 simprll 777 . . . . . . . . . . 11 ((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) β†’ 𝑑 ∈ 𝑅)
8381, 82ffvelcdmd 6990 . . . . . . . . . 10 ((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) β†’ (πΉβ€˜π‘‘) ∈ β„•)
84 nnm1nn0 12316 . . . . . . . . . 10 ((πΉβ€˜π‘‘) ∈ β„• β†’ ((πΉβ€˜π‘‘) βˆ’ 1) ∈ β„•0)
8583, 84syl 17 . . . . . . . . 9 ((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) β†’ ((πΉβ€˜π‘‘) βˆ’ 1) ∈ β„•0)
8685adantr 482 . . . . . . . 8 (((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) ∧ 𝑦 ∈ 𝑅) β†’ ((πΉβ€˜π‘‘) βˆ’ 1) ∈ β„•0)
8781ffvelcdmda 6989 . . . . . . . . 9 (((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) ∧ 𝑦 ∈ 𝑅) β†’ (πΉβ€˜π‘¦) ∈ β„•)
8887nnnn0d 12335 . . . . . . . 8 (((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) ∧ 𝑦 ∈ 𝑅) β†’ (πΉβ€˜π‘¦) ∈ β„•0)
8986, 88ifcld 4511 . . . . . . 7 (((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) ∧ 𝑦 ∈ 𝑅) β†’ if(𝑦 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘¦)) ∈ β„•0)
90 eqid 2736 . . . . . . 7 (𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘¦))) = (𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘¦)))
9189, 90fmptd 7016 . . . . . 6 ((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) β†’ (𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘¦))):π‘…βŸΆβ„•0)
92 equequ2 2027 . . . . . . . . . . . 12 (π‘₯ = 𝑑 β†’ (𝑦 = π‘₯ ↔ 𝑦 = 𝑑))
93 fveq2 6800 . . . . . . . . . . . . 13 (π‘₯ = 𝑑 β†’ (πΉβ€˜π‘₯) = (πΉβ€˜π‘‘))
9493oveq1d 7318 . . . . . . . . . . . 12 (π‘₯ = 𝑑 β†’ ((πΉβ€˜π‘₯) βˆ’ 1) = ((πΉβ€˜π‘‘) βˆ’ 1))
9592, 94ifbieq1d 4489 . . . . . . . . . . 11 (π‘₯ = 𝑑 β†’ if(𝑦 = π‘₯, ((πΉβ€˜π‘₯) βˆ’ 1), (πΉβ€˜π‘¦)) = if(𝑦 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘¦)))
9695mpteq2dv 5183 . . . . . . . . . 10 (π‘₯ = 𝑑 β†’ (𝑦 ∈ 𝑅 ↦ if(𝑦 = π‘₯, ((πΉβ€˜π‘₯) βˆ’ 1), (πΉβ€˜π‘¦))) = (𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘¦))))
9796oveq2d 7319 . . . . . . . . 9 (π‘₯ = 𝑑 β†’ (𝑀 Ramsey (𝑦 ∈ 𝑅 ↦ if(𝑦 = π‘₯, ((πΉβ€˜π‘₯) βˆ’ 1), (πΉβ€˜π‘¦)))) = (𝑀 Ramsey (𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘¦)))))
98 ramub1.g . . . . . . . . 9 𝐺 = (π‘₯ ∈ 𝑅 ↦ (𝑀 Ramsey (𝑦 ∈ 𝑅 ↦ if(𝑦 = π‘₯, ((πΉβ€˜π‘₯) βˆ’ 1), (πΉβ€˜π‘¦)))))
99 ovex 7336 . . . . . . . . 9 (𝑀 Ramsey (𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘¦)))) ∈ V
10097, 98, 99fvmpt 6903 . . . . . . . 8 (𝑑 ∈ 𝑅 β†’ (πΊβ€˜π‘‘) = (𝑀 Ramsey (𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘¦)))))
10182, 100syl 17 . . . . . . 7 ((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) β†’ (πΊβ€˜π‘‘) = (𝑀 Ramsey (𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘¦)))))
1026adantr 482 . . . . . . . 8 ((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) β†’ 𝐺:π‘…βŸΆβ„•0)
103102, 82ffvelcdmd 6990 . . . . . . 7 ((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) β†’ (πΊβ€˜π‘‘) ∈ β„•0)
104101, 103eqeltrrd 2838 . . . . . 6 ((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) β†’ (𝑀 Ramsey (𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘¦)))) ∈ β„•0)
105 simprlr 778 . . . . . 6 ((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) β†’ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋}))
106 simprrl 779 . . . . . . 7 ((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) β†’ (πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€))
107101, 106eqbrtrrd 5105 . . . . . 6 ((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) β†’ (𝑀 Ramsey (𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘¦)))) ≀ (β™―β€˜π‘€))
10833adantr 482 . . . . . . 7 ((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) β†’ 𝐾:(𝑆𝐢𝑀)βŸΆπ‘…)
1098adantr 482 . . . . . . . 8 ((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) β†’ 𝑆 ∈ Fin)
110105elpwid 4548 . . . . . . . . 9 ((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) β†’ 𝑀 βŠ† (𝑆 βˆ– {𝑋}))
111110difss2d 4075 . . . . . . . 8 ((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) β†’ 𝑀 βŠ† 𝑆)
1121hashbcss 16746 . . . . . . . 8 ((𝑆 ∈ Fin ∧ 𝑀 βŠ† 𝑆 ∧ 𝑀 ∈ β„•0) β†’ (𝑀𝐢𝑀) βŠ† (𝑆𝐢𝑀))
113109, 111, 78, 112syl3anc 1371 . . . . . . 7 ((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) β†’ (𝑀𝐢𝑀) βŠ† (𝑆𝐢𝑀))
114108, 113fssresd 6667 . . . . . 6 ((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) β†’ (𝐾 β†Ύ (𝑀𝐢𝑀)):(𝑀𝐢𝑀)βŸΆπ‘…)
1151, 78, 79, 91, 104, 105, 107, 114rami 16757 . . . . 5 ((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) β†’ βˆƒπ‘ ∈ 𝑅 βˆƒπ‘£ ∈ 𝒫 𝑀(((𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘¦)))β€˜π‘) ≀ (β™―β€˜π‘£) ∧ (𝑣𝐢𝑀) βŠ† (β—‘(𝐾 β†Ύ (𝑀𝐢𝑀)) β€œ {𝑐})))
116 equequ1 2026 . . . . . . . . . . . . . 14 (𝑦 = 𝑐 β†’ (𝑦 = 𝑑 ↔ 𝑐 = 𝑑))
117 fveq2 6800 . . . . . . . . . . . . . 14 (𝑦 = 𝑐 β†’ (πΉβ€˜π‘¦) = (πΉβ€˜π‘))
118116, 117ifbieq2d 4491 . . . . . . . . . . . . 13 (𝑦 = 𝑐 β†’ if(𝑦 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘¦)) = if(𝑐 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘)))
119 ovex 7336 . . . . . . . . . . . . . 14 ((πΉβ€˜π‘‘) βˆ’ 1) ∈ V
120 fvex 6813 . . . . . . . . . . . . . 14 (πΉβ€˜π‘) ∈ V
121119, 120ifex 4515 . . . . . . . . . . . . 13 if(𝑐 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘)) ∈ V
122118, 90, 121fvmpt 6903 . . . . . . . . . . . 12 (𝑐 ∈ 𝑅 β†’ ((𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘¦)))β€˜π‘) = if(𝑐 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘)))
123122ad2antrl 726 . . . . . . . . . . 11 (((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) ∧ (𝑐 ∈ 𝑅 ∧ 𝑣 ∈ 𝒫 𝑀)) β†’ ((𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘¦)))β€˜π‘) = if(𝑐 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘)))
124123breq1d 5091 . . . . . . . . . 10 (((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) ∧ (𝑐 ∈ 𝑅 ∧ 𝑣 ∈ 𝒫 𝑀)) β†’ (((𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘¦)))β€˜π‘) ≀ (β™―β€˜π‘£) ↔ if(𝑐 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘)) ≀ (β™―β€˜π‘£)))
125124anbi1d 631 . . . . . . . . 9 (((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) ∧ (𝑐 ∈ 𝑅 ∧ 𝑣 ∈ 𝒫 𝑀)) β†’ ((((𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘¦)))β€˜π‘) ≀ (β™―β€˜π‘£) ∧ (𝑣𝐢𝑀) βŠ† (β—‘(𝐾 β†Ύ (𝑀𝐢𝑀)) β€œ {𝑐})) ↔ (if(𝑐 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘)) ≀ (β™―β€˜π‘£) ∧ (𝑣𝐢𝑀) βŠ† (β—‘(𝐾 β†Ύ (𝑀𝐢𝑀)) β€œ {𝑐}))))
1262ad2antrr 724 . . . . . . . . . . 11 (((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) ∧ ((𝑐 ∈ 𝑅 ∧ 𝑣 ∈ 𝒫 𝑀) ∧ (if(𝑐 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘)) ≀ (β™―β€˜π‘£) ∧ (𝑣𝐢𝑀) βŠ† (β—‘(𝐾 β†Ύ (𝑀𝐢𝑀)) β€œ {𝑐})))) β†’ 𝑀 ∈ β„•)
1275ad2antrr 724 . . . . . . . . . . 11 (((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) ∧ ((𝑐 ∈ 𝑅 ∧ 𝑣 ∈ 𝒫 𝑀) ∧ (if(𝑐 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘)) ≀ (β™―β€˜π‘£) ∧ (𝑣𝐢𝑀) βŠ† (β—‘(𝐾 β†Ύ (𝑀𝐢𝑀)) β€œ {𝑐})))) β†’ 𝑅 ∈ Fin)
12880ad2antrr 724 . . . . . . . . . . 11 (((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) ∧ ((𝑐 ∈ 𝑅 ∧ 𝑣 ∈ 𝒫 𝑀) ∧ (if(𝑐 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘)) ≀ (β™―β€˜π‘£) ∧ (𝑣𝐢𝑀) βŠ† (β—‘(𝐾 β†Ύ (𝑀𝐢𝑀)) β€œ {𝑐})))) β†’ 𝐹:π‘…βŸΆβ„•)
1296ad2antrr 724 . . . . . . . . . . 11 (((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) ∧ ((𝑐 ∈ 𝑅 ∧ 𝑣 ∈ 𝒫 𝑀) ∧ (if(𝑐 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘)) ≀ (β™―β€˜π‘£) ∧ (𝑣𝐢𝑀) βŠ† (β—‘(𝐾 β†Ύ (𝑀𝐢𝑀)) β€œ {𝑐})))) β†’ 𝐺:π‘…βŸΆβ„•0)
1307ad2antrr 724 . . . . . . . . . . 11 (((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) ∧ ((𝑐 ∈ 𝑅 ∧ 𝑣 ∈ 𝒫 𝑀) ∧ (if(𝑐 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘)) ≀ (β™―β€˜π‘£) ∧ (𝑣𝐢𝑀) βŠ† (β—‘(𝐾 β†Ύ (𝑀𝐢𝑀)) β€œ {𝑐})))) β†’ ((𝑀 βˆ’ 1) Ramsey 𝐺) ∈ β„•0)
1318ad2antrr 724 . . . . . . . . . . 11 (((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) ∧ ((𝑐 ∈ 𝑅 ∧ 𝑣 ∈ 𝒫 𝑀) ∧ (if(𝑐 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘)) ≀ (β™―β€˜π‘£) ∧ (𝑣𝐢𝑀) βŠ† (β—‘(𝐾 β†Ύ (𝑀𝐢𝑀)) β€œ {𝑐})))) β†’ 𝑆 ∈ Fin)
13229ad2antrr 724 . . . . . . . . . . 11 (((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) ∧ ((𝑐 ∈ 𝑅 ∧ 𝑣 ∈ 𝒫 𝑀) ∧ (if(𝑐 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘)) ≀ (β™―β€˜π‘£) ∧ (𝑣𝐢𝑀) βŠ† (β—‘(𝐾 β†Ύ (𝑀𝐢𝑀)) β€œ {𝑐})))) β†’ (β™―β€˜π‘†) = (((𝑀 βˆ’ 1) Ramsey 𝐺) + 1))
13333ad2antrr 724 . . . . . . . . . . 11 (((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) ∧ ((𝑐 ∈ 𝑅 ∧ 𝑣 ∈ 𝒫 𝑀) ∧ (if(𝑐 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘)) ≀ (β™―β€˜π‘£) ∧ (𝑣𝐢𝑀) βŠ† (β—‘(𝐾 β†Ύ (𝑀𝐢𝑀)) β€œ {𝑐})))) β†’ 𝐾:(𝑆𝐢𝑀)βŸΆπ‘…)
13419ad2antrr 724 . . . . . . . . . . 11 (((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) ∧ ((𝑐 ∈ 𝑅 ∧ 𝑣 ∈ 𝒫 𝑀) ∧ (if(𝑐 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘)) ≀ (β™―β€˜π‘£) ∧ (𝑣𝐢𝑀) βŠ† (β—‘(𝐾 β†Ύ (𝑀𝐢𝑀)) β€œ {𝑐})))) β†’ 𝑋 ∈ 𝑆)
13582adantr 482 . . . . . . . . . . 11 (((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) ∧ ((𝑐 ∈ 𝑅 ∧ 𝑣 ∈ 𝒫 𝑀) ∧ (if(𝑐 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘)) ≀ (β™―β€˜π‘£) ∧ (𝑣𝐢𝑀) βŠ† (β—‘(𝐾 β†Ύ (𝑀𝐢𝑀)) β€œ {𝑐})))) β†’ 𝑑 ∈ 𝑅)
136110adantr 482 . . . . . . . . . . 11 (((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) ∧ ((𝑐 ∈ 𝑅 ∧ 𝑣 ∈ 𝒫 𝑀) ∧ (if(𝑐 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘)) ≀ (β™―β€˜π‘£) ∧ (𝑣𝐢𝑀) βŠ† (β—‘(𝐾 β†Ύ (𝑀𝐢𝑀)) β€œ {𝑐})))) β†’ 𝑀 βŠ† (𝑆 βˆ– {𝑋}))
137106adantr 482 . . . . . . . . . . 11 (((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) ∧ ((𝑐 ∈ 𝑅 ∧ 𝑣 ∈ 𝒫 𝑀) ∧ (if(𝑐 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘)) ≀ (β™―β€˜π‘£) ∧ (𝑣𝐢𝑀) βŠ† (β—‘(𝐾 β†Ύ (𝑀𝐢𝑀)) β€œ {𝑐})))) β†’ (πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€))
138 simprrr 780 . . . . . . . . . . . 12 ((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) β†’ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑}))
139138adantr 482 . . . . . . . . . . 11 (((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) ∧ ((𝑐 ∈ 𝑅 ∧ 𝑣 ∈ 𝒫 𝑀) ∧ (if(𝑐 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘)) ≀ (β™―β€˜π‘£) ∧ (𝑣𝐢𝑀) βŠ† (β—‘(𝐾 β†Ύ (𝑀𝐢𝑀)) β€œ {𝑐})))) β†’ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑}))
140 simprll 777 . . . . . . . . . . 11 (((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) ∧ ((𝑐 ∈ 𝑅 ∧ 𝑣 ∈ 𝒫 𝑀) ∧ (if(𝑐 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘)) ≀ (β™―β€˜π‘£) ∧ (𝑣𝐢𝑀) βŠ† (β—‘(𝐾 β†Ύ (𝑀𝐢𝑀)) β€œ {𝑐})))) β†’ 𝑐 ∈ 𝑅)
141 simprlr 778 . . . . . . . . . . . 12 (((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) ∧ ((𝑐 ∈ 𝑅 ∧ 𝑣 ∈ 𝒫 𝑀) ∧ (if(𝑐 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘)) ≀ (β™―β€˜π‘£) ∧ (𝑣𝐢𝑀) βŠ† (β—‘(𝐾 β†Ύ (𝑀𝐢𝑀)) β€œ {𝑐})))) β†’ 𝑣 ∈ 𝒫 𝑀)
142141elpwid 4548 . . . . . . . . . . 11 (((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) ∧ ((𝑐 ∈ 𝑅 ∧ 𝑣 ∈ 𝒫 𝑀) ∧ (if(𝑐 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘)) ≀ (β™―β€˜π‘£) ∧ (𝑣𝐢𝑀) βŠ† (β—‘(𝐾 β†Ύ (𝑀𝐢𝑀)) β€œ {𝑐})))) β†’ 𝑣 βŠ† 𝑀)
143 simprrl 779 . . . . . . . . . . 11 (((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) ∧ ((𝑐 ∈ 𝑅 ∧ 𝑣 ∈ 𝒫 𝑀) ∧ (if(𝑐 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘)) ≀ (β™―β€˜π‘£) ∧ (𝑣𝐢𝑀) βŠ† (β—‘(𝐾 β†Ύ (𝑀𝐢𝑀)) β€œ {𝑐})))) β†’ if(𝑐 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘)) ≀ (β™―β€˜π‘£))
144 simprrr 780 . . . . . . . . . . . 12 (((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) ∧ ((𝑐 ∈ 𝑅 ∧ 𝑣 ∈ 𝒫 𝑀) ∧ (if(𝑐 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘)) ≀ (β™―β€˜π‘£) ∧ (𝑣𝐢𝑀) βŠ† (β—‘(𝐾 β†Ύ (𝑀𝐢𝑀)) β€œ {𝑐})))) β†’ (𝑣𝐢𝑀) βŠ† (β—‘(𝐾 β†Ύ (𝑀𝐢𝑀)) β€œ {𝑐}))
145 cnvresima 6144 . . . . . . . . . . . . 13 (β—‘(𝐾 β†Ύ (𝑀𝐢𝑀)) β€œ {𝑐}) = ((◑𝐾 β€œ {𝑐}) ∩ (𝑀𝐢𝑀))
146 inss1 4168 . . . . . . . . . . . . 13 ((◑𝐾 β€œ {𝑐}) ∩ (𝑀𝐢𝑀)) βŠ† (◑𝐾 β€œ {𝑐})
147145, 146eqsstri 3960 . . . . . . . . . . . 12 (β—‘(𝐾 β†Ύ (𝑀𝐢𝑀)) β€œ {𝑐}) βŠ† (◑𝐾 β€œ {𝑐})
148144, 147sstrdi 3938 . . . . . . . . . . 11 (((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) ∧ ((𝑐 ∈ 𝑅 ∧ 𝑣 ∈ 𝒫 𝑀) ∧ (if(𝑐 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘)) ≀ (β™―β€˜π‘£) ∧ (𝑣𝐢𝑀) βŠ† (β—‘(𝐾 β†Ύ (𝑀𝐢𝑀)) β€œ {𝑐})))) β†’ (𝑣𝐢𝑀) βŠ† (◑𝐾 β€œ {𝑐}))
149126, 127, 128, 98, 129, 130, 1, 131, 132, 133, 134, 75, 135, 136, 137, 139, 140, 142, 143, 148ramub1lem1 16768 . . . . . . . . . 10 (((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) ∧ ((𝑐 ∈ 𝑅 ∧ 𝑣 ∈ 𝒫 𝑀) ∧ (if(𝑐 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘)) ≀ (β™―β€˜π‘£) ∧ (𝑣𝐢𝑀) βŠ† (β—‘(𝐾 β†Ύ (𝑀𝐢𝑀)) β€œ {𝑐})))) β†’ βˆƒπ‘§ ∈ 𝒫 𝑆((πΉβ€˜π‘) ≀ (β™―β€˜π‘§) ∧ (𝑧𝐢𝑀) βŠ† (◑𝐾 β€œ {𝑐})))
150149expr 458 . . . . . . . . 9 (((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) ∧ (𝑐 ∈ 𝑅 ∧ 𝑣 ∈ 𝒫 𝑀)) β†’ ((if(𝑐 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘)) ≀ (β™―β€˜π‘£) ∧ (𝑣𝐢𝑀) βŠ† (β—‘(𝐾 β†Ύ (𝑀𝐢𝑀)) β€œ {𝑐})) β†’ βˆƒπ‘§ ∈ 𝒫 𝑆((πΉβ€˜π‘) ≀ (β™―β€˜π‘§) ∧ (𝑧𝐢𝑀) βŠ† (◑𝐾 β€œ {𝑐}))))
151125, 150sylbid 240 . . . . . . . 8 (((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) ∧ (𝑐 ∈ 𝑅 ∧ 𝑣 ∈ 𝒫 𝑀)) β†’ ((((𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘¦)))β€˜π‘) ≀ (β™―β€˜π‘£) ∧ (𝑣𝐢𝑀) βŠ† (β—‘(𝐾 β†Ύ (𝑀𝐢𝑀)) β€œ {𝑐})) β†’ βˆƒπ‘§ ∈ 𝒫 𝑆((πΉβ€˜π‘) ≀ (β™―β€˜π‘§) ∧ (𝑧𝐢𝑀) βŠ† (◑𝐾 β€œ {𝑐}))))
152151anassrs 469 . . . . . . 7 ((((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) ∧ 𝑐 ∈ 𝑅) ∧ 𝑣 ∈ 𝒫 𝑀) β†’ ((((𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘¦)))β€˜π‘) ≀ (β™―β€˜π‘£) ∧ (𝑣𝐢𝑀) βŠ† (β—‘(𝐾 β†Ύ (𝑀𝐢𝑀)) β€œ {𝑐})) β†’ βˆƒπ‘§ ∈ 𝒫 𝑆((πΉβ€˜π‘) ≀ (β™―β€˜π‘§) ∧ (𝑧𝐢𝑀) βŠ† (◑𝐾 β€œ {𝑐}))))
153152rexlimdva 3149 . . . . . 6 (((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) ∧ 𝑐 ∈ 𝑅) β†’ (βˆƒπ‘£ ∈ 𝒫 𝑀(((𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘¦)))β€˜π‘) ≀ (β™―β€˜π‘£) ∧ (𝑣𝐢𝑀) βŠ† (β—‘(𝐾 β†Ύ (𝑀𝐢𝑀)) β€œ {𝑐})) β†’ βˆƒπ‘§ ∈ 𝒫 𝑆((πΉβ€˜π‘) ≀ (β™―β€˜π‘§) ∧ (𝑧𝐢𝑀) βŠ† (◑𝐾 β€œ {𝑐}))))
154153reximdva 3162 . . . . 5 ((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) β†’ (βˆƒπ‘ ∈ 𝑅 βˆƒπ‘£ ∈ 𝒫 𝑀(((𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘¦)))β€˜π‘) ≀ (β™―β€˜π‘£) ∧ (𝑣𝐢𝑀) βŠ† (β—‘(𝐾 β†Ύ (𝑀𝐢𝑀)) β€œ {𝑐})) β†’ βˆƒπ‘ ∈ 𝑅 βˆƒπ‘§ ∈ 𝒫 𝑆((πΉβ€˜π‘) ≀ (β™―β€˜π‘§) ∧ (𝑧𝐢𝑀) βŠ† (◑𝐾 β€œ {𝑐}))))
155115, 154mpd 15 . . . 4 ((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) β†’ βˆƒπ‘ ∈ 𝑅 βˆƒπ‘§ ∈ 𝒫 𝑆((πΉβ€˜π‘) ≀ (β™―β€˜π‘§) ∧ (𝑧𝐢𝑀) βŠ† (◑𝐾 β€œ {𝑐})))
156155expr 458 . . 3 ((πœ‘ ∧ (𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋}))) β†’ (((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})) β†’ βˆƒπ‘ ∈ 𝑅 βˆƒπ‘§ ∈ 𝒫 𝑆((πΉβ€˜π‘) ≀ (β™―β€˜π‘§) ∧ (𝑧𝐢𝑀) βŠ† (◑𝐾 β€œ {𝑐}))))
157156rexlimdvva 3202 . 2 (πœ‘ β†’ (βˆƒπ‘‘ ∈ 𝑅 βˆƒπ‘€ ∈ 𝒫 (𝑆 βˆ– {𝑋})((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})) β†’ βˆƒπ‘ ∈ 𝑅 βˆƒπ‘§ ∈ 𝒫 𝑆((πΉβ€˜π‘) ≀ (β™―β€˜π‘§) ∧ (𝑧𝐢𝑀) βŠ† (◑𝐾 β€œ {𝑐}))))
15877, 157mpd 15 1 (πœ‘ β†’ βˆƒπ‘ ∈ 𝑅 βˆƒπ‘§ ∈ 𝒫 𝑆((πΉβ€˜π‘) ≀ (β™―β€˜π‘§) ∧ (𝑧𝐢𝑀) βŠ† (◑𝐾 β€œ {𝑐})))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ∧ wa 397   = wceq 1539   ∈ wcel 2104  βˆƒwrex 3071  {crab 3284  Vcvv 3437   βˆ– cdif 3889   βˆͺ cun 3890   ∩ cin 3891   βŠ† wss 3892  ifcif 4465  π’« cpw 4539  {csn 4565   class class class wbr 5081   ↦ cmpt 5164  β—‘ccnv 5595   β†Ύ cres 5598   β€œ cima 5599  βŸΆwf 6450  β€˜cfv 6454  (class class class)co 7303   ∈ cmpo 7305  Fincfn 8760  β„‚cc 10911  1c1 10914   + caddc 10916   ≀ cle 11052   βˆ’ cmin 11247  β„•cn 12015  β„•0cn0 12275  β™―chash 14086   Ramsey cram 16741
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 2707  ax-rep 5218  ax-sep 5232  ax-nul 5239  ax-pow 5297  ax-pr 5361  ax-un 7616  ax-cnex 10969  ax-resscn 10970  ax-1cn 10971  ax-icn 10972  ax-addcl 10973  ax-addrcl 10974  ax-mulcl 10975  ax-mulrcl 10976  ax-mulcom 10977  ax-addass 10978  ax-mulass 10979  ax-distr 10980  ax-i2m1 10981  ax-1ne0 10982  ax-1rid 10983  ax-rnegex 10984  ax-rrecex 10985  ax-cnre 10986  ax-pre-lttri 10987  ax-pre-lttrn 10988  ax-pre-ltadd 10989  ax-pre-mulgt0 10990
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3or 1088  df-3an 1089  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3285  df-reu 3286  df-rab 3287  df-v 3439  df-sbc 3722  df-csb 3838  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-pss 3911  df-nul 4263  df-if 4466  df-pw 4541  df-sn 4566  df-pr 4568  df-op 4572  df-uni 4845  df-int 4887  df-iun 4933  df-br 5082  df-opab 5144  df-mpt 5165  df-tr 5199  df-id 5496  df-eprel 5502  df-po 5510  df-so 5511  df-fr 5551  df-we 5553  df-xp 5602  df-rel 5603  df-cnv 5604  df-co 5605  df-dm 5606  df-rn 5607  df-res 5608  df-ima 5609  df-pred 6213  df-ord 6280  df-on 6281  df-lim 6282  df-suc 6283  df-iota 6406  df-fun 6456  df-fn 6457  df-f 6458  df-f1 6459  df-fo 6460  df-f1o 6461  df-fv 6462  df-riota 7260  df-ov 7306  df-oprab 7307  df-mpo 7308  df-om 7741  df-1st 7859  df-2nd 7860  df-frecs 8124  df-wrecs 8155  df-recs 8229  df-rdg 8268  df-1o 8324  df-oadd 8328  df-er 8525  df-map 8644  df-en 8761  df-dom 8762  df-sdom 8763  df-fin 8764  df-sup 9241  df-inf 9242  df-dju 9699  df-card 9737  df-pnf 11053  df-mnf 11054  df-xr 11055  df-ltxr 11056  df-le 11057  df-sub 11249  df-neg 11250  df-nn 12016  df-n0 12276  df-z 12362  df-uz 12625  df-fz 13282  df-hash 14087  df-ram 16743
This theorem is referenced by:  ramub1  16770
  Copyright terms: Public domain W3C validator