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

Theorem ramub1lem2 16965
Description: Lemma for ramub1 16966. (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 12518 . . . 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 9183 . . . 4 (𝑆 ∈ Fin β†’ (𝑆 βˆ– {𝑋}) ∈ Fin)
108, 9syl 17 . . 3 (πœ‘ β†’ (𝑆 βˆ– {𝑋}) ∈ Fin)
117nn0red 12538 . . . . 5 (πœ‘ β†’ ((𝑀 βˆ’ 1) Ramsey 𝐺) ∈ ℝ)
1211leidd 11785 . . . 4 (πœ‘ β†’ ((𝑀 βˆ’ 1) Ramsey 𝐺) ≀ ((𝑀 βˆ’ 1) Ramsey 𝐺))
13 hashcl 14321 . . . . . . 7 ((𝑆 βˆ– {𝑋}) ∈ Fin β†’ (β™―β€˜(𝑆 βˆ– {𝑋})) ∈ β„•0)
1410, 13syl 17 . . . . . 6 (πœ‘ β†’ (β™―β€˜(𝑆 βˆ– {𝑋})) ∈ β„•0)
1514nn0cnd 12539 . . . . 5 (πœ‘ β†’ (β™―β€˜(𝑆 βˆ– {𝑋})) ∈ β„‚)
167nn0cnd 12539 . . . . 5 (πœ‘ β†’ ((𝑀 βˆ’ 1) Ramsey 𝐺) ∈ β„‚)
17 1cnd 11214 . . . . 5 (πœ‘ β†’ 1 ∈ β„‚)
18 undif1 4475 . . . . . . . 8 ((𝑆 βˆ– {𝑋}) βˆͺ {𝑋}) = (𝑆 βˆͺ {𝑋})
19 ramub1.x . . . . . . . . . 10 (πœ‘ β†’ 𝑋 ∈ 𝑆)
2019snssd 4812 . . . . . . . . 9 (πœ‘ β†’ {𝑋} βŠ† 𝑆)
21 ssequn2 4183 . . . . . . . . 9 ({𝑋} βŠ† 𝑆 ↔ (𝑆 βˆͺ {𝑋}) = 𝑆)
2220, 21sylib 217 . . . . . . . 8 (πœ‘ β†’ (𝑆 βˆͺ {𝑋}) = 𝑆)
2318, 22eqtrid 2783 . . . . . . 7 (πœ‘ β†’ ((𝑆 βˆ– {𝑋}) βˆͺ {𝑋}) = 𝑆)
2423fveq2d 6895 . . . . . 6 (πœ‘ β†’ (β™―β€˜((𝑆 βˆ– {𝑋}) βˆͺ {𝑋})) = (β™―β€˜π‘†))
25 neldifsnd 4796 . . . . . . 7 (πœ‘ β†’ Β¬ 𝑋 ∈ (𝑆 βˆ– {𝑋}))
26 hashunsng 14357 . . . . . . . 8 (𝑋 ∈ 𝑆 β†’ (((𝑆 βˆ– {𝑋}) ∈ Fin ∧ Β¬ 𝑋 ∈ (𝑆 βˆ– {𝑋})) β†’ (β™―β€˜((𝑆 βˆ– {𝑋}) βˆͺ {𝑋})) = ((β™―β€˜(𝑆 βˆ– {𝑋})) + 1)))
2719, 26syl 17 . . . . . . 7 (πœ‘ β†’ (((𝑆 βˆ– {𝑋}) ∈ Fin ∧ Β¬ 𝑋 ∈ (𝑆 βˆ– {𝑋})) β†’ (β™―β€˜((𝑆 βˆ– {𝑋}) βˆͺ {𝑋})) = ((β™―β€˜(𝑆 βˆ– {𝑋})) + 1)))
2810, 25, 27mp2and 696 . . . . . 6 (πœ‘ β†’ (β™―β€˜((𝑆 βˆ– {𝑋}) βˆͺ {𝑋})) = ((β™―β€˜(𝑆 βˆ– {𝑋})) + 1))
29 ramub1.5 . . . . . 6 (πœ‘ β†’ (β™―β€˜π‘†) = (((𝑀 βˆ’ 1) Ramsey 𝐺) + 1))
3024, 28, 293eqtr3d 2779 . . . . 5 (πœ‘ β†’ ((β™―β€˜(𝑆 βˆ– {𝑋})) + 1) = (((𝑀 βˆ’ 1) Ramsey 𝐺) + 1))
3115, 16, 17, 30addcan2ad 11425 . . . 4 (πœ‘ β†’ (β™―β€˜(𝑆 βˆ– {𝑋})) = ((𝑀 βˆ’ 1) Ramsey 𝐺))
3212, 31breqtrrd 5176 . . 3 (πœ‘ β†’ ((𝑀 βˆ’ 1) Ramsey 𝐺) ≀ (β™―β€˜(𝑆 βˆ– {𝑋})))
33 ramub1.6 . . . . . 6 (πœ‘ β†’ 𝐾:(𝑆𝐢𝑀)βŸΆπ‘…)
3433adantr 480 . . . . 5 ((πœ‘ ∧ 𝑒 ∈ ((𝑆 βˆ– {𝑋})𝐢(𝑀 βˆ’ 1))) β†’ 𝐾:(𝑆𝐢𝑀)βŸΆπ‘…)
35 fveqeq2 6900 . . . . . . 7 (π‘₯ = (𝑒 βˆͺ {𝑋}) β†’ ((β™―β€˜π‘₯) = 𝑀 ↔ (β™―β€˜(𝑒 βˆͺ {𝑋})) = 𝑀))
361hashbcval 16940 . . . . . . . . . . . . . . 15 (((𝑆 βˆ– {𝑋}) ∈ Fin ∧ (𝑀 βˆ’ 1) ∈ β„•0) β†’ ((𝑆 βˆ– {𝑋})𝐢(𝑀 βˆ’ 1)) = {π‘₯ ∈ 𝒫 (𝑆 βˆ– {𝑋}) ∣ (β™―β€˜π‘₯) = (𝑀 βˆ’ 1)})
3710, 4, 36syl2anc 583 . . . . . . . . . . . . . 14 (πœ‘ β†’ ((𝑆 βˆ– {𝑋})𝐢(𝑀 βˆ’ 1)) = {π‘₯ ∈ 𝒫 (𝑆 βˆ– {𝑋}) ∣ (β™―β€˜π‘₯) = (𝑀 βˆ’ 1)})
3837eleq2d 2818 . . . . . . . . . . . . 13 (πœ‘ β†’ (𝑒 ∈ ((𝑆 βˆ– {𝑋})𝐢(𝑀 βˆ’ 1)) ↔ 𝑒 ∈ {π‘₯ ∈ 𝒫 (𝑆 βˆ– {𝑋}) ∣ (β™―β€˜π‘₯) = (𝑀 βˆ’ 1)}))
39 fveqeq2 6900 . . . . . . . . . . . . . 14 (π‘₯ = 𝑒 β†’ ((β™―β€˜π‘₯) = (𝑀 βˆ’ 1) ↔ (β™―β€˜π‘’) = (𝑀 βˆ’ 1)))
4039elrab 3683 . . . . . . . . . . . . 13 (𝑒 ∈ {π‘₯ ∈ 𝒫 (𝑆 βˆ– {𝑋}) ∣ (β™―β€˜π‘₯) = (𝑀 βˆ’ 1)} ↔ (𝑒 ∈ 𝒫 (𝑆 βˆ– {𝑋}) ∧ (β™―β€˜π‘’) = (𝑀 βˆ’ 1)))
4138, 40bitrdi 287 . . . . . . . . . . . 12 (πœ‘ β†’ (𝑒 ∈ ((𝑆 βˆ– {𝑋})𝐢(𝑀 βˆ’ 1)) ↔ (𝑒 ∈ 𝒫 (𝑆 βˆ– {𝑋}) ∧ (β™―β€˜π‘’) = (𝑀 βˆ’ 1))))
4241simprbda 498 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑒 ∈ ((𝑆 βˆ– {𝑋})𝐢(𝑀 βˆ’ 1))) β†’ 𝑒 ∈ 𝒫 (𝑆 βˆ– {𝑋}))
4342elpwid 4611 . . . . . . . . . 10 ((πœ‘ ∧ 𝑒 ∈ ((𝑆 βˆ– {𝑋})𝐢(𝑀 βˆ’ 1))) β†’ 𝑒 βŠ† (𝑆 βˆ– {𝑋}))
4443difss2d 4134 . . . . . . . . 9 ((πœ‘ ∧ 𝑒 ∈ ((𝑆 βˆ– {𝑋})𝐢(𝑀 βˆ’ 1))) β†’ 𝑒 βŠ† 𝑆)
4520adantr 480 . . . . . . . . 9 ((πœ‘ ∧ 𝑒 ∈ ((𝑆 βˆ– {𝑋})𝐢(𝑀 βˆ’ 1))) β†’ {𝑋} βŠ† 𝑆)
4644, 45unssd 4186 . . . . . . . 8 ((πœ‘ ∧ 𝑒 ∈ ((𝑆 βˆ– {𝑋})𝐢(𝑀 βˆ’ 1))) β†’ (𝑒 βˆͺ {𝑋}) βŠ† 𝑆)
47 vex 3477 . . . . . . . . . 10 𝑒 ∈ V
48 snex 5431 . . . . . . . . . 10 {𝑋} ∈ V
4947, 48unex 7737 . . . . . . . . 9 (𝑒 βˆͺ {𝑋}) ∈ V
5049elpw 4606 . . . . . . . 8 ((𝑒 βˆͺ {𝑋}) ∈ 𝒫 𝑆 ↔ (𝑒 βˆͺ {𝑋}) βŠ† 𝑆)
5146, 50sylibr 233 . . . . . . 7 ((πœ‘ ∧ 𝑒 ∈ ((𝑆 βˆ– {𝑋})𝐢(𝑀 βˆ’ 1))) β†’ (𝑒 βˆͺ {𝑋}) ∈ 𝒫 𝑆)
5210adantr 480 . . . . . . . . . 10 ((πœ‘ ∧ 𝑒 ∈ ((𝑆 βˆ– {𝑋})𝐢(𝑀 βˆ’ 1))) β†’ (𝑆 βˆ– {𝑋}) ∈ Fin)
5352, 43ssfid 9271 . . . . . . . . 9 ((πœ‘ ∧ 𝑒 ∈ ((𝑆 βˆ– {𝑋})𝐢(𝑀 βˆ’ 1))) β†’ 𝑒 ∈ Fin)
54 neldifsnd 4796 . . . . . . . . . 10 ((πœ‘ ∧ 𝑒 ∈ ((𝑆 βˆ– {𝑋})𝐢(𝑀 βˆ’ 1))) β†’ Β¬ 𝑋 ∈ (𝑆 βˆ– {𝑋}))
5543, 54ssneldd 3985 . . . . . . . . 9 ((πœ‘ ∧ 𝑒 ∈ ((𝑆 βˆ– {𝑋})𝐢(𝑀 βˆ’ 1))) β†’ Β¬ 𝑋 ∈ 𝑒)
5619adantr 480 . . . . . . . . . 10 ((πœ‘ ∧ 𝑒 ∈ ((𝑆 βˆ– {𝑋})𝐢(𝑀 βˆ’ 1))) β†’ 𝑋 ∈ 𝑆)
57 hashunsng 14357 . . . . . . . . . 10 (𝑋 ∈ 𝑆 β†’ ((𝑒 ∈ Fin ∧ Β¬ 𝑋 ∈ 𝑒) β†’ (β™―β€˜(𝑒 βˆͺ {𝑋})) = ((β™―β€˜π‘’) + 1)))
5856, 57syl 17 . . . . . . . . 9 ((πœ‘ ∧ 𝑒 ∈ ((𝑆 βˆ– {𝑋})𝐢(𝑀 βˆ’ 1))) β†’ ((𝑒 ∈ Fin ∧ Β¬ 𝑋 ∈ 𝑒) β†’ (β™―β€˜(𝑒 βˆͺ {𝑋})) = ((β™―β€˜π‘’) + 1)))
5953, 55, 58mp2and 696 . . . . . . . 8 ((πœ‘ ∧ 𝑒 ∈ ((𝑆 βˆ– {𝑋})𝐢(𝑀 βˆ’ 1))) β†’ (β™―β€˜(𝑒 βˆͺ {𝑋})) = ((β™―β€˜π‘’) + 1))
6041simplbda 499 . . . . . . . . 9 ((πœ‘ ∧ 𝑒 ∈ ((𝑆 βˆ– {𝑋})𝐢(𝑀 βˆ’ 1))) β†’ (β™―β€˜π‘’) = (𝑀 βˆ’ 1))
6160oveq1d 7427 . . . . . . . 8 ((πœ‘ ∧ 𝑒 ∈ ((𝑆 βˆ– {𝑋})𝐢(𝑀 βˆ’ 1))) β†’ ((β™―β€˜π‘’) + 1) = ((𝑀 βˆ’ 1) + 1))
622nncnd 12233 . . . . . . . . . 10 (πœ‘ β†’ 𝑀 ∈ β„‚)
63 ax-1cn 11172 . . . . . . . . . 10 1 ∈ β„‚
64 npcan 11474 . . . . . . . . . 10 ((𝑀 ∈ β„‚ ∧ 1 ∈ β„‚) β†’ ((𝑀 βˆ’ 1) + 1) = 𝑀)
6562, 63, 64sylancl 585 . . . . . . . . 9 (πœ‘ β†’ ((𝑀 βˆ’ 1) + 1) = 𝑀)
6665adantr 480 . . . . . . . 8 ((πœ‘ ∧ 𝑒 ∈ ((𝑆 βˆ– {𝑋})𝐢(𝑀 βˆ’ 1))) β†’ ((𝑀 βˆ’ 1) + 1) = 𝑀)
6759, 61, 663eqtrd 2775 . . . . . . 7 ((πœ‘ ∧ 𝑒 ∈ ((𝑆 βˆ– {𝑋})𝐢(𝑀 βˆ’ 1))) β†’ (β™―β€˜(𝑒 βˆͺ {𝑋})) = 𝑀)
6835, 51, 67elrabd 3685 . . . . . 6 ((πœ‘ ∧ 𝑒 ∈ ((𝑆 βˆ– {𝑋})𝐢(𝑀 βˆ’ 1))) β†’ (𝑒 βˆͺ {𝑋}) ∈ {π‘₯ ∈ 𝒫 𝑆 ∣ (β™―β€˜π‘₯) = 𝑀})
692nnnn0d 12537 . . . . . . . 8 (πœ‘ β†’ 𝑀 ∈ β„•0)
701hashbcval 16940 . . . . . . . 8 ((𝑆 ∈ Fin ∧ 𝑀 ∈ β„•0) β†’ (𝑆𝐢𝑀) = {π‘₯ ∈ 𝒫 𝑆 ∣ (β™―β€˜π‘₯) = 𝑀})
718, 69, 70syl2anc 583 . . . . . . 7 (πœ‘ β†’ (𝑆𝐢𝑀) = {π‘₯ ∈ 𝒫 𝑆 ∣ (β™―β€˜π‘₯) = 𝑀})
7271adantr 480 . . . . . 6 ((πœ‘ ∧ 𝑒 ∈ ((𝑆 βˆ– {𝑋})𝐢(𝑀 βˆ’ 1))) β†’ (𝑆𝐢𝑀) = {π‘₯ ∈ 𝒫 𝑆 ∣ (β™―β€˜π‘₯) = 𝑀})
7368, 72eleqtrrd 2835 . . . . 5 ((πœ‘ ∧ 𝑒 ∈ ((𝑆 βˆ– {𝑋})𝐢(𝑀 βˆ’ 1))) β†’ (𝑒 βˆͺ {𝑋}) ∈ (𝑆𝐢𝑀))
7434, 73ffvelcdmd 7087 . . . 4 ((πœ‘ ∧ 𝑒 ∈ ((𝑆 βˆ– {𝑋})𝐢(𝑀 βˆ’ 1))) β†’ (πΎβ€˜(𝑒 βˆͺ {𝑋})) ∈ 𝑅)
75 ramub1.h . . . 4 𝐻 = (𝑒 ∈ ((𝑆 βˆ– {𝑋})𝐢(𝑀 βˆ’ 1)) ↦ (πΎβ€˜(𝑒 βˆͺ {𝑋})))
7674, 75fmptd 7115 . . 3 (πœ‘ β†’ 𝐻:((𝑆 βˆ– {𝑋})𝐢(𝑀 βˆ’ 1))βŸΆπ‘…)
771, 4, 5, 6, 7, 10, 32, 76rami 16953 . 2 (πœ‘ β†’ βˆƒπ‘‘ ∈ 𝑅 βˆƒπ‘€ ∈ 𝒫 (𝑆 βˆ– {𝑋})((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))
7869adantr 480 . . . . . 6 ((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) β†’ 𝑀 ∈ β„•0)
795adantr 480 . . . . . 6 ((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) β†’ 𝑅 ∈ Fin)
80 ramub1.f . . . . . . . . . . . 12 (πœ‘ β†’ 𝐹:π‘…βŸΆβ„•)
8180adantr 480 . . . . . . . . . . 11 ((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) β†’ 𝐹:π‘…βŸΆβ„•)
82 simprll 776 . . . . . . . . . . 11 ((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) β†’ 𝑑 ∈ 𝑅)
8381, 82ffvelcdmd 7087 . . . . . . . . . 10 ((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) β†’ (πΉβ€˜π‘‘) ∈ β„•)
84 nnm1nn0 12518 . . . . . . . . . 10 ((πΉβ€˜π‘‘) ∈ β„• β†’ ((πΉβ€˜π‘‘) βˆ’ 1) ∈ β„•0)
8583, 84syl 17 . . . . . . . . 9 ((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) β†’ ((πΉβ€˜π‘‘) βˆ’ 1) ∈ β„•0)
8685adantr 480 . . . . . . . 8 (((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) ∧ 𝑦 ∈ 𝑅) β†’ ((πΉβ€˜π‘‘) βˆ’ 1) ∈ β„•0)
8781ffvelcdmda 7086 . . . . . . . . 9 (((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) ∧ 𝑦 ∈ 𝑅) β†’ (πΉβ€˜π‘¦) ∈ β„•)
8887nnnn0d 12537 . . . . . . . 8 (((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) ∧ 𝑦 ∈ 𝑅) β†’ (πΉβ€˜π‘¦) ∈ β„•0)
8986, 88ifcld 4574 . . . . . . 7 (((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) ∧ 𝑦 ∈ 𝑅) β†’ if(𝑦 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘¦)) ∈ β„•0)
90 eqid 2731 . . . . . . 7 (𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘¦))) = (𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘¦)))
9189, 90fmptd 7115 . . . . . 6 ((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) β†’ (𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘¦))):π‘…βŸΆβ„•0)
92 equequ2 2028 . . . . . . . . . . . 12 (π‘₯ = 𝑑 β†’ (𝑦 = π‘₯ ↔ 𝑦 = 𝑑))
93 fveq2 6891 . . . . . . . . . . . . 13 (π‘₯ = 𝑑 β†’ (πΉβ€˜π‘₯) = (πΉβ€˜π‘‘))
9493oveq1d 7427 . . . . . . . . . . . 12 (π‘₯ = 𝑑 β†’ ((πΉβ€˜π‘₯) βˆ’ 1) = ((πΉβ€˜π‘‘) βˆ’ 1))
9592, 94ifbieq1d 4552 . . . . . . . . . . 11 (π‘₯ = 𝑑 β†’ if(𝑦 = π‘₯, ((πΉβ€˜π‘₯) βˆ’ 1), (πΉβ€˜π‘¦)) = if(𝑦 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘¦)))
9695mpteq2dv 5250 . . . . . . . . . 10 (π‘₯ = 𝑑 β†’ (𝑦 ∈ 𝑅 ↦ if(𝑦 = π‘₯, ((πΉβ€˜π‘₯) βˆ’ 1), (πΉβ€˜π‘¦))) = (𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘¦))))
9796oveq2d 7428 . . . . . . . . 9 (π‘₯ = 𝑑 β†’ (𝑀 Ramsey (𝑦 ∈ 𝑅 ↦ if(𝑦 = π‘₯, ((πΉβ€˜π‘₯) βˆ’ 1), (πΉβ€˜π‘¦)))) = (𝑀 Ramsey (𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘¦)))))
98 ramub1.g . . . . . . . . 9 𝐺 = (π‘₯ ∈ 𝑅 ↦ (𝑀 Ramsey (𝑦 ∈ 𝑅 ↦ if(𝑦 = π‘₯, ((πΉβ€˜π‘₯) βˆ’ 1), (πΉβ€˜π‘¦)))))
99 ovex 7445 . . . . . . . . 9 (𝑀 Ramsey (𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘¦)))) ∈ V
10097, 98, 99fvmpt 6998 . . . . . . . 8 (𝑑 ∈ 𝑅 β†’ (πΊβ€˜π‘‘) = (𝑀 Ramsey (𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘¦)))))
10182, 100syl 17 . . . . . . 7 ((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) β†’ (πΊβ€˜π‘‘) = (𝑀 Ramsey (𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘¦)))))
1026adantr 480 . . . . . . . 8 ((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) β†’ 𝐺:π‘…βŸΆβ„•0)
103102, 82ffvelcdmd 7087 . . . . . . 7 ((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) β†’ (πΊβ€˜π‘‘) ∈ β„•0)
104101, 103eqeltrrd 2833 . . . . . 6 ((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) β†’ (𝑀 Ramsey (𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘¦)))) ∈ β„•0)
105 simprlr 777 . . . . . 6 ((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) β†’ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋}))
106 simprrl 778 . . . . . . 7 ((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) β†’ (πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€))
107101, 106eqbrtrrd 5172 . . . . . 6 ((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) β†’ (𝑀 Ramsey (𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘¦)))) ≀ (β™―β€˜π‘€))
10833adantr 480 . . . . . . 7 ((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) β†’ 𝐾:(𝑆𝐢𝑀)βŸΆπ‘…)
1098adantr 480 . . . . . . . 8 ((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) β†’ 𝑆 ∈ Fin)
110105elpwid 4611 . . . . . . . . 9 ((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) β†’ 𝑀 βŠ† (𝑆 βˆ– {𝑋}))
111110difss2d 4134 . . . . . . . 8 ((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) β†’ 𝑀 βŠ† 𝑆)
1121hashbcss 16942 . . . . . . . 8 ((𝑆 ∈ Fin ∧ 𝑀 βŠ† 𝑆 ∧ 𝑀 ∈ β„•0) β†’ (𝑀𝐢𝑀) βŠ† (𝑆𝐢𝑀))
113109, 111, 78, 112syl3anc 1370 . . . . . . 7 ((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) β†’ (𝑀𝐢𝑀) βŠ† (𝑆𝐢𝑀))
114108, 113fssresd 6758 . . . . . 6 ((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) β†’ (𝐾 β†Ύ (𝑀𝐢𝑀)):(𝑀𝐢𝑀)βŸΆπ‘…)
1151, 78, 79, 91, 104, 105, 107, 114rami 16953 . . . . 5 ((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) β†’ βˆƒπ‘ ∈ 𝑅 βˆƒπ‘£ ∈ 𝒫 𝑀(((𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘¦)))β€˜π‘) ≀ (β™―β€˜π‘£) ∧ (𝑣𝐢𝑀) βŠ† (β—‘(𝐾 β†Ύ (𝑀𝐢𝑀)) β€œ {𝑐})))
116 equequ1 2027 . . . . . . . . . . . . . 14 (𝑦 = 𝑐 β†’ (𝑦 = 𝑑 ↔ 𝑐 = 𝑑))
117 fveq2 6891 . . . . . . . . . . . . . 14 (𝑦 = 𝑐 β†’ (πΉβ€˜π‘¦) = (πΉβ€˜π‘))
118116, 117ifbieq2d 4554 . . . . . . . . . . . . 13 (𝑦 = 𝑐 β†’ if(𝑦 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘¦)) = if(𝑐 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘)))
119 ovex 7445 . . . . . . . . . . . . . 14 ((πΉβ€˜π‘‘) βˆ’ 1) ∈ V
120 fvex 6904 . . . . . . . . . . . . . 14 (πΉβ€˜π‘) ∈ V
121119, 120ifex 4578 . . . . . . . . . . . . 13 if(𝑐 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘)) ∈ V
122118, 90, 121fvmpt 6998 . . . . . . . . . . . 12 (𝑐 ∈ 𝑅 β†’ ((𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘¦)))β€˜π‘) = if(𝑐 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘)))
123122ad2antrl 725 . . . . . . . . . . 11 (((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) ∧ (𝑐 ∈ 𝑅 ∧ 𝑣 ∈ 𝒫 𝑀)) β†’ ((𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘¦)))β€˜π‘) = if(𝑐 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘)))
124123breq1d 5158 . . . . . . . . . 10 (((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) ∧ (𝑐 ∈ 𝑅 ∧ 𝑣 ∈ 𝒫 𝑀)) β†’ (((𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘¦)))β€˜π‘) ≀ (β™―β€˜π‘£) ↔ if(𝑐 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘)) ≀ (β™―β€˜π‘£)))
125124anbi1d 629 . . . . . . . . 9 (((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) ∧ (𝑐 ∈ 𝑅 ∧ 𝑣 ∈ 𝒫 𝑀)) β†’ ((((𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘¦)))β€˜π‘) ≀ (β™―β€˜π‘£) ∧ (𝑣𝐢𝑀) βŠ† (β—‘(𝐾 β†Ύ (𝑀𝐢𝑀)) β€œ {𝑐})) ↔ (if(𝑐 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘)) ≀ (β™―β€˜π‘£) ∧ (𝑣𝐢𝑀) βŠ† (β—‘(𝐾 β†Ύ (𝑀𝐢𝑀)) β€œ {𝑐}))))
1262ad2antrr 723 . . . . . . . . . . 11 (((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) ∧ ((𝑐 ∈ 𝑅 ∧ 𝑣 ∈ 𝒫 𝑀) ∧ (if(𝑐 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘)) ≀ (β™―β€˜π‘£) ∧ (𝑣𝐢𝑀) βŠ† (β—‘(𝐾 β†Ύ (𝑀𝐢𝑀)) β€œ {𝑐})))) β†’ 𝑀 ∈ β„•)
1275ad2antrr 723 . . . . . . . . . . 11 (((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) ∧ ((𝑐 ∈ 𝑅 ∧ 𝑣 ∈ 𝒫 𝑀) ∧ (if(𝑐 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘)) ≀ (β™―β€˜π‘£) ∧ (𝑣𝐢𝑀) βŠ† (β—‘(𝐾 β†Ύ (𝑀𝐢𝑀)) β€œ {𝑐})))) β†’ 𝑅 ∈ Fin)
12880ad2antrr 723 . . . . . . . . . . 11 (((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) ∧ ((𝑐 ∈ 𝑅 ∧ 𝑣 ∈ 𝒫 𝑀) ∧ (if(𝑐 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘)) ≀ (β™―β€˜π‘£) ∧ (𝑣𝐢𝑀) βŠ† (β—‘(𝐾 β†Ύ (𝑀𝐢𝑀)) β€œ {𝑐})))) β†’ 𝐹:π‘…βŸΆβ„•)
1296ad2antrr 723 . . . . . . . . . . 11 (((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) ∧ ((𝑐 ∈ 𝑅 ∧ 𝑣 ∈ 𝒫 𝑀) ∧ (if(𝑐 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘)) ≀ (β™―β€˜π‘£) ∧ (𝑣𝐢𝑀) βŠ† (β—‘(𝐾 β†Ύ (𝑀𝐢𝑀)) β€œ {𝑐})))) β†’ 𝐺:π‘…βŸΆβ„•0)
1307ad2antrr 723 . . . . . . . . . . 11 (((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) ∧ ((𝑐 ∈ 𝑅 ∧ 𝑣 ∈ 𝒫 𝑀) ∧ (if(𝑐 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘)) ≀ (β™―β€˜π‘£) ∧ (𝑣𝐢𝑀) βŠ† (β—‘(𝐾 β†Ύ (𝑀𝐢𝑀)) β€œ {𝑐})))) β†’ ((𝑀 βˆ’ 1) Ramsey 𝐺) ∈ β„•0)
1318ad2antrr 723 . . . . . . . . . . 11 (((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) ∧ ((𝑐 ∈ 𝑅 ∧ 𝑣 ∈ 𝒫 𝑀) ∧ (if(𝑐 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘)) ≀ (β™―β€˜π‘£) ∧ (𝑣𝐢𝑀) βŠ† (β—‘(𝐾 β†Ύ (𝑀𝐢𝑀)) β€œ {𝑐})))) β†’ 𝑆 ∈ Fin)
13229ad2antrr 723 . . . . . . . . . . 11 (((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) ∧ ((𝑐 ∈ 𝑅 ∧ 𝑣 ∈ 𝒫 𝑀) ∧ (if(𝑐 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘)) ≀ (β™―β€˜π‘£) ∧ (𝑣𝐢𝑀) βŠ† (β—‘(𝐾 β†Ύ (𝑀𝐢𝑀)) β€œ {𝑐})))) β†’ (β™―β€˜π‘†) = (((𝑀 βˆ’ 1) Ramsey 𝐺) + 1))
13333ad2antrr 723 . . . . . . . . . . 11 (((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) ∧ ((𝑐 ∈ 𝑅 ∧ 𝑣 ∈ 𝒫 𝑀) ∧ (if(𝑐 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘)) ≀ (β™―β€˜π‘£) ∧ (𝑣𝐢𝑀) βŠ† (β—‘(𝐾 β†Ύ (𝑀𝐢𝑀)) β€œ {𝑐})))) β†’ 𝐾:(𝑆𝐢𝑀)βŸΆπ‘…)
13419ad2antrr 723 . . . . . . . . . . 11 (((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) ∧ ((𝑐 ∈ 𝑅 ∧ 𝑣 ∈ 𝒫 𝑀) ∧ (if(𝑐 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘)) ≀ (β™―β€˜π‘£) ∧ (𝑣𝐢𝑀) βŠ† (β—‘(𝐾 β†Ύ (𝑀𝐢𝑀)) β€œ {𝑐})))) β†’ 𝑋 ∈ 𝑆)
13582adantr 480 . . . . . . . . . . 11 (((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) ∧ ((𝑐 ∈ 𝑅 ∧ 𝑣 ∈ 𝒫 𝑀) ∧ (if(𝑐 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘)) ≀ (β™―β€˜π‘£) ∧ (𝑣𝐢𝑀) βŠ† (β—‘(𝐾 β†Ύ (𝑀𝐢𝑀)) β€œ {𝑐})))) β†’ 𝑑 ∈ 𝑅)
136110adantr 480 . . . . . . . . . . 11 (((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) ∧ ((𝑐 ∈ 𝑅 ∧ 𝑣 ∈ 𝒫 𝑀) ∧ (if(𝑐 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘)) ≀ (β™―β€˜π‘£) ∧ (𝑣𝐢𝑀) βŠ† (β—‘(𝐾 β†Ύ (𝑀𝐢𝑀)) β€œ {𝑐})))) β†’ 𝑀 βŠ† (𝑆 βˆ– {𝑋}))
137106adantr 480 . . . . . . . . . . 11 (((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) ∧ ((𝑐 ∈ 𝑅 ∧ 𝑣 ∈ 𝒫 𝑀) ∧ (if(𝑐 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘)) ≀ (β™―β€˜π‘£) ∧ (𝑣𝐢𝑀) βŠ† (β—‘(𝐾 β†Ύ (𝑀𝐢𝑀)) β€œ {𝑐})))) β†’ (πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€))
138 simprrr 779 . . . . . . . . . . . 12 ((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) β†’ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑}))
139138adantr 480 . . . . . . . . . . 11 (((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) ∧ ((𝑐 ∈ 𝑅 ∧ 𝑣 ∈ 𝒫 𝑀) ∧ (if(𝑐 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘)) ≀ (β™―β€˜π‘£) ∧ (𝑣𝐢𝑀) βŠ† (β—‘(𝐾 β†Ύ (𝑀𝐢𝑀)) β€œ {𝑐})))) β†’ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑}))
140 simprll 776 . . . . . . . . . . 11 (((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) ∧ ((𝑐 ∈ 𝑅 ∧ 𝑣 ∈ 𝒫 𝑀) ∧ (if(𝑐 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘)) ≀ (β™―β€˜π‘£) ∧ (𝑣𝐢𝑀) βŠ† (β—‘(𝐾 β†Ύ (𝑀𝐢𝑀)) β€œ {𝑐})))) β†’ 𝑐 ∈ 𝑅)
141 simprlr 777 . . . . . . . . . . . 12 (((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) ∧ ((𝑐 ∈ 𝑅 ∧ 𝑣 ∈ 𝒫 𝑀) ∧ (if(𝑐 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘)) ≀ (β™―β€˜π‘£) ∧ (𝑣𝐢𝑀) βŠ† (β—‘(𝐾 β†Ύ (𝑀𝐢𝑀)) β€œ {𝑐})))) β†’ 𝑣 ∈ 𝒫 𝑀)
142141elpwid 4611 . . . . . . . . . . 11 (((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) ∧ ((𝑐 ∈ 𝑅 ∧ 𝑣 ∈ 𝒫 𝑀) ∧ (if(𝑐 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘)) ≀ (β™―β€˜π‘£) ∧ (𝑣𝐢𝑀) βŠ† (β—‘(𝐾 β†Ύ (𝑀𝐢𝑀)) β€œ {𝑐})))) β†’ 𝑣 βŠ† 𝑀)
143 simprrl 778 . . . . . . . . . . 11 (((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) ∧ ((𝑐 ∈ 𝑅 ∧ 𝑣 ∈ 𝒫 𝑀) ∧ (if(𝑐 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘)) ≀ (β™―β€˜π‘£) ∧ (𝑣𝐢𝑀) βŠ† (β—‘(𝐾 β†Ύ (𝑀𝐢𝑀)) β€œ {𝑐})))) β†’ if(𝑐 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘)) ≀ (β™―β€˜π‘£))
144 simprrr 779 . . . . . . . . . . . 12 (((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) ∧ ((𝑐 ∈ 𝑅 ∧ 𝑣 ∈ 𝒫 𝑀) ∧ (if(𝑐 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘)) ≀ (β™―β€˜π‘£) ∧ (𝑣𝐢𝑀) βŠ† (β—‘(𝐾 β†Ύ (𝑀𝐢𝑀)) β€œ {𝑐})))) β†’ (𝑣𝐢𝑀) βŠ† (β—‘(𝐾 β†Ύ (𝑀𝐢𝑀)) β€œ {𝑐}))
145 cnvresima 6229 . . . . . . . . . . . . 13 (β—‘(𝐾 β†Ύ (𝑀𝐢𝑀)) β€œ {𝑐}) = ((◑𝐾 β€œ {𝑐}) ∩ (𝑀𝐢𝑀))
146 inss1 4228 . . . . . . . . . . . . 13 ((◑𝐾 β€œ {𝑐}) ∩ (𝑀𝐢𝑀)) βŠ† (◑𝐾 β€œ {𝑐})
147145, 146eqsstri 4016 . . . . . . . . . . . 12 (β—‘(𝐾 β†Ύ (𝑀𝐢𝑀)) β€œ {𝑐}) βŠ† (◑𝐾 β€œ {𝑐})
148144, 147sstrdi 3994 . . . . . . . . . . 11 (((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) ∧ ((𝑐 ∈ 𝑅 ∧ 𝑣 ∈ 𝒫 𝑀) ∧ (if(𝑐 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘)) ≀ (β™―β€˜π‘£) ∧ (𝑣𝐢𝑀) βŠ† (β—‘(𝐾 β†Ύ (𝑀𝐢𝑀)) β€œ {𝑐})))) β†’ (𝑣𝐢𝑀) βŠ† (◑𝐾 β€œ {𝑐}))
149126, 127, 128, 98, 129, 130, 1, 131, 132, 133, 134, 75, 135, 136, 137, 139, 140, 142, 143, 148ramub1lem1 16964 . . . . . . . . . 10 (((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) ∧ ((𝑐 ∈ 𝑅 ∧ 𝑣 ∈ 𝒫 𝑀) ∧ (if(𝑐 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘)) ≀ (β™―β€˜π‘£) ∧ (𝑣𝐢𝑀) βŠ† (β—‘(𝐾 β†Ύ (𝑀𝐢𝑀)) β€œ {𝑐})))) β†’ βˆƒπ‘§ ∈ 𝒫 𝑆((πΉβ€˜π‘) ≀ (β™―β€˜π‘§) ∧ (𝑧𝐢𝑀) βŠ† (◑𝐾 β€œ {𝑐})))
150149expr 456 . . . . . . . . 9 (((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) ∧ (𝑐 ∈ 𝑅 ∧ 𝑣 ∈ 𝒫 𝑀)) β†’ ((if(𝑐 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘)) ≀ (β™―β€˜π‘£) ∧ (𝑣𝐢𝑀) βŠ† (β—‘(𝐾 β†Ύ (𝑀𝐢𝑀)) β€œ {𝑐})) β†’ βˆƒπ‘§ ∈ 𝒫 𝑆((πΉβ€˜π‘) ≀ (β™―β€˜π‘§) ∧ (𝑧𝐢𝑀) βŠ† (◑𝐾 β€œ {𝑐}))))
151125, 150sylbid 239 . . . . . . . 8 (((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) ∧ (𝑐 ∈ 𝑅 ∧ 𝑣 ∈ 𝒫 𝑀)) β†’ ((((𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘¦)))β€˜π‘) ≀ (β™―β€˜π‘£) ∧ (𝑣𝐢𝑀) βŠ† (β—‘(𝐾 β†Ύ (𝑀𝐢𝑀)) β€œ {𝑐})) β†’ βˆƒπ‘§ ∈ 𝒫 𝑆((πΉβ€˜π‘) ≀ (β™―β€˜π‘§) ∧ (𝑧𝐢𝑀) βŠ† (◑𝐾 β€œ {𝑐}))))
152151anassrs 467 . . . . . . 7 ((((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) ∧ 𝑐 ∈ 𝑅) ∧ 𝑣 ∈ 𝒫 𝑀) β†’ ((((𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘¦)))β€˜π‘) ≀ (β™―β€˜π‘£) ∧ (𝑣𝐢𝑀) βŠ† (β—‘(𝐾 β†Ύ (𝑀𝐢𝑀)) β€œ {𝑐})) β†’ βˆƒπ‘§ ∈ 𝒫 𝑆((πΉβ€˜π‘) ≀ (β™―β€˜π‘§) ∧ (𝑧𝐢𝑀) βŠ† (◑𝐾 β€œ {𝑐}))))
153152rexlimdva 3154 . . . . . 6 (((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) ∧ 𝑐 ∈ 𝑅) β†’ (βˆƒπ‘£ ∈ 𝒫 𝑀(((𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘¦)))β€˜π‘) ≀ (β™―β€˜π‘£) ∧ (𝑣𝐢𝑀) βŠ† (β—‘(𝐾 β†Ύ (𝑀𝐢𝑀)) β€œ {𝑐})) β†’ βˆƒπ‘§ ∈ 𝒫 𝑆((πΉβ€˜π‘) ≀ (β™―β€˜π‘§) ∧ (𝑧𝐢𝑀) βŠ† (◑𝐾 β€œ {𝑐}))))
154153reximdva 3167 . . . . 5 ((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) β†’ (βˆƒπ‘ ∈ 𝑅 βˆƒπ‘£ ∈ 𝒫 𝑀(((𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘¦)))β€˜π‘) ≀ (β™―β€˜π‘£) ∧ (𝑣𝐢𝑀) βŠ† (β—‘(𝐾 β†Ύ (𝑀𝐢𝑀)) β€œ {𝑐})) β†’ βˆƒπ‘ ∈ 𝑅 βˆƒπ‘§ ∈ 𝒫 𝑆((πΉβ€˜π‘) ≀ (β™―β€˜π‘§) ∧ (𝑧𝐢𝑀) βŠ† (◑𝐾 β€œ {𝑐}))))
155115, 154mpd 15 . . . 4 ((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) β†’ βˆƒπ‘ ∈ 𝑅 βˆƒπ‘§ ∈ 𝒫 𝑆((πΉβ€˜π‘) ≀ (β™―β€˜π‘§) ∧ (𝑧𝐢𝑀) βŠ† (◑𝐾 β€œ {𝑐})))
156155expr 456 . . 3 ((πœ‘ ∧ (𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋}))) β†’ (((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})) β†’ βˆƒπ‘ ∈ 𝑅 βˆƒπ‘§ ∈ 𝒫 𝑆((πΉβ€˜π‘) ≀ (β™―β€˜π‘§) ∧ (𝑧𝐢𝑀) βŠ† (◑𝐾 β€œ {𝑐}))))
157156rexlimdvva 3210 . 2 (πœ‘ β†’ (βˆƒπ‘‘ ∈ 𝑅 βˆƒπ‘€ ∈ 𝒫 (𝑆 βˆ– {𝑋})((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})) β†’ βˆƒπ‘ ∈ 𝑅 βˆƒπ‘§ ∈ 𝒫 𝑆((πΉβ€˜π‘) ≀ (β™―β€˜π‘§) ∧ (𝑧𝐢𝑀) βŠ† (◑𝐾 β€œ {𝑐}))))
15877, 157mpd 15 1 (πœ‘ β†’ βˆƒπ‘ ∈ 𝑅 βˆƒπ‘§ ∈ 𝒫 𝑆((πΉβ€˜π‘) ≀ (β™―β€˜π‘§) ∧ (𝑧𝐢𝑀) βŠ† (◑𝐾 β€œ {𝑐})))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2105  βˆƒwrex 3069  {crab 3431  Vcvv 3473   βˆ– cdif 3945   βˆͺ cun 3946   ∩ cin 3947   βŠ† wss 3948  ifcif 4528  π’« cpw 4602  {csn 4628   class class class wbr 5148   ↦ cmpt 5231  β—‘ccnv 5675   β†Ύ cres 5678   β€œ cima 5679  βŸΆwf 6539  β€˜cfv 6543  (class class class)co 7412   ∈ cmpo 7414  Fincfn 8943  β„‚cc 11112  1c1 11115   + caddc 11117   ≀ cle 11254   βˆ’ cmin 11449  β„•cn 12217  β„•0cn0 12477  β™―chash 14295   Ramsey cram 16937
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2702  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7729  ax-cnex 11170  ax-resscn 11171  ax-1cn 11172  ax-icn 11173  ax-addcl 11174  ax-addrcl 11175  ax-mulcl 11176  ax-mulrcl 11177  ax-mulcom 11178  ax-addass 11179  ax-mulass 11180  ax-distr 11181  ax-i2m1 11182  ax-1ne0 11183  ax-1rid 11184  ax-rnegex 11185  ax-rrecex 11186  ax-cnre 11187  ax-pre-lttri 11188  ax-pre-lttrn 11189  ax-pre-ltadd 11190  ax-pre-mulgt0 11191
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-rmo 3375  df-reu 3376  df-rab 3432  df-v 3475  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-int 4951  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-riota 7368  df-ov 7415  df-oprab 7416  df-mpo 7417  df-om 7860  df-1st 7979  df-2nd 7980  df-frecs 8270  df-wrecs 8301  df-recs 8375  df-rdg 8414  df-1o 8470  df-oadd 8474  df-er 8707  df-map 8826  df-en 8944  df-dom 8945  df-sdom 8946  df-fin 8947  df-sup 9441  df-inf 9442  df-dju 9900  df-card 9938  df-pnf 11255  df-mnf 11256  df-xr 11257  df-ltxr 11258  df-le 11259  df-sub 11451  df-neg 11452  df-nn 12218  df-n0 12478  df-z 12564  df-uz 12828  df-fz 13490  df-hash 14296  df-ram 16939
This theorem is referenced by:  ramub1  16966
  Copyright terms: Public domain W3C validator