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

Theorem ramub1lem2 16962
Description: Lemma for ramub1 16963. (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 12515 . . . 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 9181 . . . 4 (𝑆 ∈ Fin β†’ (𝑆 βˆ– {𝑋}) ∈ Fin)
108, 9syl 17 . . 3 (πœ‘ β†’ (𝑆 βˆ– {𝑋}) ∈ Fin)
117nn0red 12535 . . . . 5 (πœ‘ β†’ ((𝑀 βˆ’ 1) Ramsey 𝐺) ∈ ℝ)
1211leidd 11782 . . . 4 (πœ‘ β†’ ((𝑀 βˆ’ 1) Ramsey 𝐺) ≀ ((𝑀 βˆ’ 1) Ramsey 𝐺))
13 hashcl 14318 . . . . . . 7 ((𝑆 βˆ– {𝑋}) ∈ Fin β†’ (β™―β€˜(𝑆 βˆ– {𝑋})) ∈ β„•0)
1410, 13syl 17 . . . . . 6 (πœ‘ β†’ (β™―β€˜(𝑆 βˆ– {𝑋})) ∈ β„•0)
1514nn0cnd 12536 . . . . 5 (πœ‘ β†’ (β™―β€˜(𝑆 βˆ– {𝑋})) ∈ β„‚)
167nn0cnd 12536 . . . . 5 (πœ‘ β†’ ((𝑀 βˆ’ 1) Ramsey 𝐺) ∈ β„‚)
17 1cnd 11211 . . . . 5 (πœ‘ β†’ 1 ∈ β„‚)
18 undif1 4475 . . . . . . . 8 ((𝑆 βˆ– {𝑋}) βˆͺ {𝑋}) = (𝑆 βˆͺ {𝑋})
19 ramub1.x . . . . . . . . . 10 (πœ‘ β†’ 𝑋 ∈ 𝑆)
2019snssd 4812 . . . . . . . . 9 (πœ‘ β†’ {𝑋} βŠ† 𝑆)
21 ssequn2 4183 . . . . . . . . 9 ({𝑋} βŠ† 𝑆 ↔ (𝑆 βˆͺ {𝑋}) = 𝑆)
2220, 21sylib 217 . . . . . . . 8 (πœ‘ β†’ (𝑆 βˆͺ {𝑋}) = 𝑆)
2318, 22eqtrid 2784 . . . . . . 7 (πœ‘ β†’ ((𝑆 βˆ– {𝑋}) βˆͺ {𝑋}) = 𝑆)
2423fveq2d 6895 . . . . . 6 (πœ‘ β†’ (β™―β€˜((𝑆 βˆ– {𝑋}) βˆͺ {𝑋})) = (β™―β€˜π‘†))
25 neldifsnd 4796 . . . . . . 7 (πœ‘ β†’ Β¬ 𝑋 ∈ (𝑆 βˆ– {𝑋}))
26 hashunsng 14354 . . . . . . . 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 2780 . . . . 5 (πœ‘ β†’ ((β™―β€˜(𝑆 βˆ– {𝑋})) + 1) = (((𝑀 βˆ’ 1) Ramsey 𝐺) + 1))
3115, 16, 17, 30addcan2ad 11422 . . . 4 (πœ‘ β†’ (β™―β€˜(𝑆 βˆ– {𝑋})) = ((𝑀 βˆ’ 1) Ramsey 𝐺))
3212, 31breqtrrd 5176 . . 3 (πœ‘ β†’ ((𝑀 βˆ’ 1) Ramsey 𝐺) ≀ (β™―β€˜(𝑆 βˆ– {𝑋})))
33 ramub1.6 . . . . . 6 (πœ‘ β†’ 𝐾:(𝑆𝐢𝑀)βŸΆπ‘…)
3433adantr 481 . . . . 5 ((πœ‘ ∧ 𝑒 ∈ ((𝑆 βˆ– {𝑋})𝐢(𝑀 βˆ’ 1))) β†’ 𝐾:(𝑆𝐢𝑀)βŸΆπ‘…)
35 fveqeq2 6900 . . . . . . 7 (π‘₯ = (𝑒 βˆͺ {𝑋}) β†’ ((β™―β€˜π‘₯) = 𝑀 ↔ (β™―β€˜(𝑒 βˆͺ {𝑋})) = 𝑀))
361hashbcval 16937 . . . . . . . . . . . . . . 15 (((𝑆 βˆ– {𝑋}) ∈ Fin ∧ (𝑀 βˆ’ 1) ∈ β„•0) β†’ ((𝑆 βˆ– {𝑋})𝐢(𝑀 βˆ’ 1)) = {π‘₯ ∈ 𝒫 (𝑆 βˆ– {𝑋}) ∣ (β™―β€˜π‘₯) = (𝑀 βˆ’ 1)})
3710, 4, 36syl2anc 584 . . . . . . . . . . . . . 14 (πœ‘ β†’ ((𝑆 βˆ– {𝑋})𝐢(𝑀 βˆ’ 1)) = {π‘₯ ∈ 𝒫 (𝑆 βˆ– {𝑋}) ∣ (β™―β€˜π‘₯) = (𝑀 βˆ’ 1)})
3837eleq2d 2819 . . . . . . . . . . . . 13 (πœ‘ β†’ (𝑒 ∈ ((𝑆 βˆ– {𝑋})𝐢(𝑀 βˆ’ 1)) ↔ 𝑒 ∈ {π‘₯ ∈ 𝒫 (𝑆 βˆ– {𝑋}) ∣ (β™―β€˜π‘₯) = (𝑀 βˆ’ 1)}))
39 fveqeq2 6900 . . . . . . . . . . . . . 14 (π‘₯ = 𝑒 β†’ ((β™―β€˜π‘₯) = (𝑀 βˆ’ 1) ↔ (β™―β€˜π‘’) = (𝑀 βˆ’ 1)))
4039elrab 3683 . . . . . . . . . . . . 13 (𝑒 ∈ {π‘₯ ∈ 𝒫 (𝑆 βˆ– {𝑋}) ∣ (β™―β€˜π‘₯) = (𝑀 βˆ’ 1)} ↔ (𝑒 ∈ 𝒫 (𝑆 βˆ– {𝑋}) ∧ (β™―β€˜π‘’) = (𝑀 βˆ’ 1)))
4138, 40bitrdi 286 . . . . . . . . . . . 12 (πœ‘ β†’ (𝑒 ∈ ((𝑆 βˆ– {𝑋})𝐢(𝑀 βˆ’ 1)) ↔ (𝑒 ∈ 𝒫 (𝑆 βˆ– {𝑋}) ∧ (β™―β€˜π‘’) = (𝑀 βˆ’ 1))))
4241simprbda 499 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑒 ∈ ((𝑆 βˆ– {𝑋})𝐢(𝑀 βˆ’ 1))) β†’ 𝑒 ∈ 𝒫 (𝑆 βˆ– {𝑋}))
4342elpwid 4611 . . . . . . . . . 10 ((πœ‘ ∧ 𝑒 ∈ ((𝑆 βˆ– {𝑋})𝐢(𝑀 βˆ’ 1))) β†’ 𝑒 βŠ† (𝑆 βˆ– {𝑋}))
4443difss2d 4134 . . . . . . . . 9 ((πœ‘ ∧ 𝑒 ∈ ((𝑆 βˆ– {𝑋})𝐢(𝑀 βˆ’ 1))) β†’ 𝑒 βŠ† 𝑆)
4520adantr 481 . . . . . . . . 9 ((πœ‘ ∧ 𝑒 ∈ ((𝑆 βˆ– {𝑋})𝐢(𝑀 βˆ’ 1))) β†’ {𝑋} βŠ† 𝑆)
4644, 45unssd 4186 . . . . . . . 8 ((πœ‘ ∧ 𝑒 ∈ ((𝑆 βˆ– {𝑋})𝐢(𝑀 βˆ’ 1))) β†’ (𝑒 βˆͺ {𝑋}) βŠ† 𝑆)
47 vex 3478 . . . . . . . . . 10 𝑒 ∈ V
48 snex 5431 . . . . . . . . . 10 {𝑋} ∈ V
4947, 48unex 7735 . . . . . . . . 9 (𝑒 βˆͺ {𝑋}) ∈ V
5049elpw 4606 . . . . . . . 8 ((𝑒 βˆͺ {𝑋}) ∈ 𝒫 𝑆 ↔ (𝑒 βˆͺ {𝑋}) βŠ† 𝑆)
5146, 50sylibr 233 . . . . . . 7 ((πœ‘ ∧ 𝑒 ∈ ((𝑆 βˆ– {𝑋})𝐢(𝑀 βˆ’ 1))) β†’ (𝑒 βˆͺ {𝑋}) ∈ 𝒫 𝑆)
5210adantr 481 . . . . . . . . . 10 ((πœ‘ ∧ 𝑒 ∈ ((𝑆 βˆ– {𝑋})𝐢(𝑀 βˆ’ 1))) β†’ (𝑆 βˆ– {𝑋}) ∈ Fin)
5352, 43ssfid 9269 . . . . . . . . 9 ((πœ‘ ∧ 𝑒 ∈ ((𝑆 βˆ– {𝑋})𝐢(𝑀 βˆ’ 1))) β†’ 𝑒 ∈ Fin)
54 neldifsnd 4796 . . . . . . . . . 10 ((πœ‘ ∧ 𝑒 ∈ ((𝑆 βˆ– {𝑋})𝐢(𝑀 βˆ’ 1))) β†’ Β¬ 𝑋 ∈ (𝑆 βˆ– {𝑋}))
5543, 54ssneldd 3985 . . . . . . . . 9 ((πœ‘ ∧ 𝑒 ∈ ((𝑆 βˆ– {𝑋})𝐢(𝑀 βˆ’ 1))) β†’ Β¬ 𝑋 ∈ 𝑒)
5619adantr 481 . . . . . . . . . 10 ((πœ‘ ∧ 𝑒 ∈ ((𝑆 βˆ– {𝑋})𝐢(𝑀 βˆ’ 1))) β†’ 𝑋 ∈ 𝑆)
57 hashunsng 14354 . . . . . . . . . 10 (𝑋 ∈ 𝑆 β†’ ((𝑒 ∈ Fin ∧ Β¬ 𝑋 ∈ 𝑒) β†’ (β™―β€˜(𝑒 βˆͺ {𝑋})) = ((β™―β€˜π‘’) + 1)))
5856, 57syl 17 . . . . . . . . 9 ((πœ‘ ∧ 𝑒 ∈ ((𝑆 βˆ– {𝑋})𝐢(𝑀 βˆ’ 1))) β†’ ((𝑒 ∈ Fin ∧ Β¬ 𝑋 ∈ 𝑒) β†’ (β™―β€˜(𝑒 βˆͺ {𝑋})) = ((β™―β€˜π‘’) + 1)))
5953, 55, 58mp2and 697 . . . . . . . 8 ((πœ‘ ∧ 𝑒 ∈ ((𝑆 βˆ– {𝑋})𝐢(𝑀 βˆ’ 1))) β†’ (β™―β€˜(𝑒 βˆͺ {𝑋})) = ((β™―β€˜π‘’) + 1))
6041simplbda 500 . . . . . . . . 9 ((πœ‘ ∧ 𝑒 ∈ ((𝑆 βˆ– {𝑋})𝐢(𝑀 βˆ’ 1))) β†’ (β™―β€˜π‘’) = (𝑀 βˆ’ 1))
6160oveq1d 7426 . . . . . . . 8 ((πœ‘ ∧ 𝑒 ∈ ((𝑆 βˆ– {𝑋})𝐢(𝑀 βˆ’ 1))) β†’ ((β™―β€˜π‘’) + 1) = ((𝑀 βˆ’ 1) + 1))
622nncnd 12230 . . . . . . . . . 10 (πœ‘ β†’ 𝑀 ∈ β„‚)
63 ax-1cn 11170 . . . . . . . . . 10 1 ∈ β„‚
64 npcan 11471 . . . . . . . . . 10 ((𝑀 ∈ β„‚ ∧ 1 ∈ β„‚) β†’ ((𝑀 βˆ’ 1) + 1) = 𝑀)
6562, 63, 64sylancl 586 . . . . . . . . 9 (πœ‘ β†’ ((𝑀 βˆ’ 1) + 1) = 𝑀)
6665adantr 481 . . . . . . . 8 ((πœ‘ ∧ 𝑒 ∈ ((𝑆 βˆ– {𝑋})𝐢(𝑀 βˆ’ 1))) β†’ ((𝑀 βˆ’ 1) + 1) = 𝑀)
6759, 61, 663eqtrd 2776 . . . . . . 7 ((πœ‘ ∧ 𝑒 ∈ ((𝑆 βˆ– {𝑋})𝐢(𝑀 βˆ’ 1))) β†’ (β™―β€˜(𝑒 βˆͺ {𝑋})) = 𝑀)
6835, 51, 67elrabd 3685 . . . . . 6 ((πœ‘ ∧ 𝑒 ∈ ((𝑆 βˆ– {𝑋})𝐢(𝑀 βˆ’ 1))) β†’ (𝑒 βˆͺ {𝑋}) ∈ {π‘₯ ∈ 𝒫 𝑆 ∣ (β™―β€˜π‘₯) = 𝑀})
692nnnn0d 12534 . . . . . . . 8 (πœ‘ β†’ 𝑀 ∈ β„•0)
701hashbcval 16937 . . . . . . . 8 ((𝑆 ∈ Fin ∧ 𝑀 ∈ β„•0) β†’ (𝑆𝐢𝑀) = {π‘₯ ∈ 𝒫 𝑆 ∣ (β™―β€˜π‘₯) = 𝑀})
718, 69, 70syl2anc 584 . . . . . . 7 (πœ‘ β†’ (𝑆𝐢𝑀) = {π‘₯ ∈ 𝒫 𝑆 ∣ (β™―β€˜π‘₯) = 𝑀})
7271adantr 481 . . . . . 6 ((πœ‘ ∧ 𝑒 ∈ ((𝑆 βˆ– {𝑋})𝐢(𝑀 βˆ’ 1))) β†’ (𝑆𝐢𝑀) = {π‘₯ ∈ 𝒫 𝑆 ∣ (β™―β€˜π‘₯) = 𝑀})
7368, 72eleqtrrd 2836 . . . . 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 16950 . 2 (πœ‘ β†’ βˆƒπ‘‘ ∈ 𝑅 βˆƒπ‘€ ∈ 𝒫 (𝑆 βˆ– {𝑋})((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))
7869adantr 481 . . . . . 6 ((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) β†’ 𝑀 ∈ β„•0)
795adantr 481 . . . . . 6 ((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) β†’ 𝑅 ∈ Fin)
80 ramub1.f . . . . . . . . . . . 12 (πœ‘ β†’ 𝐹:π‘…βŸΆβ„•)
8180adantr 481 . . . . . . . . . . 11 ((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) β†’ 𝐹:π‘…βŸΆβ„•)
82 simprll 777 . . . . . . . . . . 11 ((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) β†’ 𝑑 ∈ 𝑅)
8381, 82ffvelcdmd 7087 . . . . . . . . . 10 ((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) β†’ (πΉβ€˜π‘‘) ∈ β„•)
84 nnm1nn0 12515 . . . . . . . . . 10 ((πΉβ€˜π‘‘) ∈ β„• β†’ ((πΉβ€˜π‘‘) βˆ’ 1) ∈ β„•0)
8583, 84syl 17 . . . . . . . . 9 ((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) β†’ ((πΉβ€˜π‘‘) βˆ’ 1) ∈ β„•0)
8685adantr 481 . . . . . . . 8 (((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) ∧ 𝑦 ∈ 𝑅) β†’ ((πΉβ€˜π‘‘) βˆ’ 1) ∈ β„•0)
8781ffvelcdmda 7086 . . . . . . . . 9 (((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) ∧ 𝑦 ∈ 𝑅) β†’ (πΉβ€˜π‘¦) ∈ β„•)
8887nnnn0d 12534 . . . . . . . 8 (((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) ∧ 𝑦 ∈ 𝑅) β†’ (πΉβ€˜π‘¦) ∈ β„•0)
8986, 88ifcld 4574 . . . . . . 7 (((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) ∧ 𝑦 ∈ 𝑅) β†’ if(𝑦 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘¦)) ∈ β„•0)
90 eqid 2732 . . . . . . 7 (𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘¦))) = (𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘¦)))
9189, 90fmptd 7115 . . . . . 6 ((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) β†’ (𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘¦))):π‘…βŸΆβ„•0)
92 equequ2 2029 . . . . . . . . . . . 12 (π‘₯ = 𝑑 β†’ (𝑦 = π‘₯ ↔ 𝑦 = 𝑑))
93 fveq2 6891 . . . . . . . . . . . . 13 (π‘₯ = 𝑑 β†’ (πΉβ€˜π‘₯) = (πΉβ€˜π‘‘))
9493oveq1d 7426 . . . . . . . . . . . 12 (π‘₯ = 𝑑 β†’ ((πΉβ€˜π‘₯) βˆ’ 1) = ((πΉβ€˜π‘‘) βˆ’ 1))
9592, 94ifbieq1d 4552 . . . . . . . . . . 11 (π‘₯ = 𝑑 β†’ if(𝑦 = π‘₯, ((πΉβ€˜π‘₯) βˆ’ 1), (πΉβ€˜π‘¦)) = if(𝑦 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘¦)))
9695mpteq2dv 5250 . . . . . . . . . 10 (π‘₯ = 𝑑 β†’ (𝑦 ∈ 𝑅 ↦ if(𝑦 = π‘₯, ((πΉβ€˜π‘₯) βˆ’ 1), (πΉβ€˜π‘¦))) = (𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘¦))))
9796oveq2d 7427 . . . . . . . . 9 (π‘₯ = 𝑑 β†’ (𝑀 Ramsey (𝑦 ∈ 𝑅 ↦ if(𝑦 = π‘₯, ((πΉβ€˜π‘₯) βˆ’ 1), (πΉβ€˜π‘¦)))) = (𝑀 Ramsey (𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘¦)))))
98 ramub1.g . . . . . . . . 9 𝐺 = (π‘₯ ∈ 𝑅 ↦ (𝑀 Ramsey (𝑦 ∈ 𝑅 ↦ if(𝑦 = π‘₯, ((πΉβ€˜π‘₯) βˆ’ 1), (πΉβ€˜π‘¦)))))
99 ovex 7444 . . . . . . . . 9 (𝑀 Ramsey (𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘¦)))) ∈ V
10097, 98, 99fvmpt 6998 . . . . . . . 8 (𝑑 ∈ 𝑅 β†’ (πΊβ€˜π‘‘) = (𝑀 Ramsey (𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘¦)))))
10182, 100syl 17 . . . . . . 7 ((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) β†’ (πΊβ€˜π‘‘) = (𝑀 Ramsey (𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘¦)))))
1026adantr 481 . . . . . . . 8 ((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) β†’ 𝐺:π‘…βŸΆβ„•0)
103102, 82ffvelcdmd 7087 . . . . . . 7 ((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) β†’ (πΊβ€˜π‘‘) ∈ β„•0)
104101, 103eqeltrrd 2834 . . . . . 6 ((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) β†’ (𝑀 Ramsey (𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘¦)))) ∈ β„•0)
105 simprlr 778 . . . . . 6 ((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) β†’ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋}))
106 simprrl 779 . . . . . . 7 ((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) β†’ (πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€))
107101, 106eqbrtrrd 5172 . . . . . 6 ((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) β†’ (𝑀 Ramsey (𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘¦)))) ≀ (β™―β€˜π‘€))
10833adantr 481 . . . . . . 7 ((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) β†’ 𝐾:(𝑆𝐢𝑀)βŸΆπ‘…)
1098adantr 481 . . . . . . . 8 ((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) β†’ 𝑆 ∈ Fin)
110105elpwid 4611 . . . . . . . . 9 ((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) β†’ 𝑀 βŠ† (𝑆 βˆ– {𝑋}))
111110difss2d 4134 . . . . . . . 8 ((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) β†’ 𝑀 βŠ† 𝑆)
1121hashbcss 16939 . . . . . . . 8 ((𝑆 ∈ Fin ∧ 𝑀 βŠ† 𝑆 ∧ 𝑀 ∈ β„•0) β†’ (𝑀𝐢𝑀) βŠ† (𝑆𝐢𝑀))
113109, 111, 78, 112syl3anc 1371 . . . . . . 7 ((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) β†’ (𝑀𝐢𝑀) βŠ† (𝑆𝐢𝑀))
114108, 113fssresd 6758 . . . . . 6 ((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) β†’ (𝐾 β†Ύ (𝑀𝐢𝑀)):(𝑀𝐢𝑀)βŸΆπ‘…)
1151, 78, 79, 91, 104, 105, 107, 114rami 16950 . . . . 5 ((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) β†’ βˆƒπ‘ ∈ 𝑅 βˆƒπ‘£ ∈ 𝒫 𝑀(((𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘¦)))β€˜π‘) ≀ (β™―β€˜π‘£) ∧ (𝑣𝐢𝑀) βŠ† (β—‘(𝐾 β†Ύ (𝑀𝐢𝑀)) β€œ {𝑐})))
116 equequ1 2028 . . . . . . . . . . . . . 14 (𝑦 = 𝑐 β†’ (𝑦 = 𝑑 ↔ 𝑐 = 𝑑))
117 fveq2 6891 . . . . . . . . . . . . . 14 (𝑦 = 𝑐 β†’ (πΉβ€˜π‘¦) = (πΉβ€˜π‘))
118116, 117ifbieq2d 4554 . . . . . . . . . . . . 13 (𝑦 = 𝑐 β†’ if(𝑦 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘¦)) = if(𝑐 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘)))
119 ovex 7444 . . . . . . . . . . . . . 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 726 . . . . . . . . . . 11 (((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) ∧ (𝑐 ∈ 𝑅 ∧ 𝑣 ∈ 𝒫 𝑀)) β†’ ((𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘¦)))β€˜π‘) = if(𝑐 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘)))
124123breq1d 5158 . . . . . . . . . 10 (((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) ∧ (𝑐 ∈ 𝑅 ∧ 𝑣 ∈ 𝒫 𝑀)) β†’ (((𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘¦)))β€˜π‘) ≀ (β™―β€˜π‘£) ↔ if(𝑐 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘)) ≀ (β™―β€˜π‘£)))
125124anbi1d 630 . . . . . . . . 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 481 . . . . . . . . . . 11 (((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) ∧ ((𝑐 ∈ 𝑅 ∧ 𝑣 ∈ 𝒫 𝑀) ∧ (if(𝑐 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘)) ≀ (β™―β€˜π‘£) ∧ (𝑣𝐢𝑀) βŠ† (β—‘(𝐾 β†Ύ (𝑀𝐢𝑀)) β€œ {𝑐})))) β†’ 𝑑 ∈ 𝑅)
136110adantr 481 . . . . . . . . . . 11 (((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) ∧ ((𝑐 ∈ 𝑅 ∧ 𝑣 ∈ 𝒫 𝑀) ∧ (if(𝑐 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘)) ≀ (β™―β€˜π‘£) ∧ (𝑣𝐢𝑀) βŠ† (β—‘(𝐾 β†Ύ (𝑀𝐢𝑀)) β€œ {𝑐})))) β†’ 𝑀 βŠ† (𝑆 βˆ– {𝑋}))
137106adantr 481 . . . . . . . . . . 11 (((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) ∧ ((𝑐 ∈ 𝑅 ∧ 𝑣 ∈ 𝒫 𝑀) ∧ (if(𝑐 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘)) ≀ (β™―β€˜π‘£) ∧ (𝑣𝐢𝑀) βŠ† (β—‘(𝐾 β†Ύ (𝑀𝐢𝑀)) β€œ {𝑐})))) β†’ (πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€))
138 simprrr 780 . . . . . . . . . . . 12 ((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) β†’ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑}))
139138adantr 481 . . . . . . . . . . 11 (((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) ∧ ((𝑐 ∈ 𝑅 ∧ 𝑣 ∈ 𝒫 𝑀) ∧ (if(𝑐 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘)) ≀ (β™―β€˜π‘£) ∧ (𝑣𝐢𝑀) βŠ† (β—‘(𝐾 β†Ύ (𝑀𝐢𝑀)) β€œ {𝑐})))) β†’ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑}))
140 simprll 777 . . . . . . . . . . 11 (((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) ∧ ((𝑐 ∈ 𝑅 ∧ 𝑣 ∈ 𝒫 𝑀) ∧ (if(𝑐 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘)) ≀ (β™―β€˜π‘£) ∧ (𝑣𝐢𝑀) βŠ† (β—‘(𝐾 β†Ύ (𝑀𝐢𝑀)) β€œ {𝑐})))) β†’ 𝑐 ∈ 𝑅)
141 simprlr 778 . . . . . . . . . . . 12 (((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) ∧ ((𝑐 ∈ 𝑅 ∧ 𝑣 ∈ 𝒫 𝑀) ∧ (if(𝑐 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘)) ≀ (β™―β€˜π‘£) ∧ (𝑣𝐢𝑀) βŠ† (β—‘(𝐾 β†Ύ (𝑀𝐢𝑀)) β€œ {𝑐})))) β†’ 𝑣 ∈ 𝒫 𝑀)
142141elpwid 4611 . . . . . . . . . . 11 (((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) ∧ ((𝑐 ∈ 𝑅 ∧ 𝑣 ∈ 𝒫 𝑀) ∧ (if(𝑐 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘)) ≀ (β™―β€˜π‘£) ∧ (𝑣𝐢𝑀) βŠ† (β—‘(𝐾 β†Ύ (𝑀𝐢𝑀)) β€œ {𝑐})))) β†’ 𝑣 βŠ† 𝑀)
143 simprrl 779 . . . . . . . . . . 11 (((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) ∧ ((𝑐 ∈ 𝑅 ∧ 𝑣 ∈ 𝒫 𝑀) ∧ (if(𝑐 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘)) ≀ (β™―β€˜π‘£) ∧ (𝑣𝐢𝑀) βŠ† (β—‘(𝐾 β†Ύ (𝑀𝐢𝑀)) β€œ {𝑐})))) β†’ if(𝑐 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘)) ≀ (β™―β€˜π‘£))
144 simprrr 780 . . . . . . . . . . . 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 16961 . . . . . . . . . 10 (((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) ∧ ((𝑐 ∈ 𝑅 ∧ 𝑣 ∈ 𝒫 𝑀) ∧ (if(𝑐 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘)) ≀ (β™―β€˜π‘£) ∧ (𝑣𝐢𝑀) βŠ† (β—‘(𝐾 β†Ύ (𝑀𝐢𝑀)) β€œ {𝑐})))) β†’ βˆƒπ‘§ ∈ 𝒫 𝑆((πΉβ€˜π‘) ≀ (β™―β€˜π‘§) ∧ (𝑧𝐢𝑀) βŠ† (◑𝐾 β€œ {𝑐})))
150149expr 457 . . . . . . . . 9 (((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) ∧ (𝑐 ∈ 𝑅 ∧ 𝑣 ∈ 𝒫 𝑀)) β†’ ((if(𝑐 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘)) ≀ (β™―β€˜π‘£) ∧ (𝑣𝐢𝑀) βŠ† (β—‘(𝐾 β†Ύ (𝑀𝐢𝑀)) β€œ {𝑐})) β†’ βˆƒπ‘§ ∈ 𝒫 𝑆((πΉβ€˜π‘) ≀ (β™―β€˜π‘§) ∧ (𝑧𝐢𝑀) βŠ† (◑𝐾 β€œ {𝑐}))))
151125, 150sylbid 239 . . . . . . . 8 (((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) ∧ (𝑐 ∈ 𝑅 ∧ 𝑣 ∈ 𝒫 𝑀)) β†’ ((((𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘¦)))β€˜π‘) ≀ (β™―β€˜π‘£) ∧ (𝑣𝐢𝑀) βŠ† (β—‘(𝐾 β†Ύ (𝑀𝐢𝑀)) β€œ {𝑐})) β†’ βˆƒπ‘§ ∈ 𝒫 𝑆((πΉβ€˜π‘) ≀ (β™―β€˜π‘§) ∧ (𝑧𝐢𝑀) βŠ† (◑𝐾 β€œ {𝑐}))))
152151anassrs 468 . . . . . . 7 ((((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) ∧ 𝑐 ∈ 𝑅) ∧ 𝑣 ∈ 𝒫 𝑀) β†’ ((((𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘¦)))β€˜π‘) ≀ (β™―β€˜π‘£) ∧ (𝑣𝐢𝑀) βŠ† (β—‘(𝐾 β†Ύ (𝑀𝐢𝑀)) β€œ {𝑐})) β†’ βˆƒπ‘§ ∈ 𝒫 𝑆((πΉβ€˜π‘) ≀ (β™―β€˜π‘§) ∧ (𝑧𝐢𝑀) βŠ† (◑𝐾 β€œ {𝑐}))))
153152rexlimdva 3155 . . . . . 6 (((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) ∧ 𝑐 ∈ 𝑅) β†’ (βˆƒπ‘£ ∈ 𝒫 𝑀(((𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘¦)))β€˜π‘) ≀ (β™―β€˜π‘£) ∧ (𝑣𝐢𝑀) βŠ† (β—‘(𝐾 β†Ύ (𝑀𝐢𝑀)) β€œ {𝑐})) β†’ βˆƒπ‘§ ∈ 𝒫 𝑆((πΉβ€˜π‘) ≀ (β™―β€˜π‘§) ∧ (𝑧𝐢𝑀) βŠ† (◑𝐾 β€œ {𝑐}))))
154153reximdva 3168 . . . . 5 ((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) β†’ (βˆƒπ‘ ∈ 𝑅 βˆƒπ‘£ ∈ 𝒫 𝑀(((𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑑, ((πΉβ€˜π‘‘) βˆ’ 1), (πΉβ€˜π‘¦)))β€˜π‘) ≀ (β™―β€˜π‘£) ∧ (𝑣𝐢𝑀) βŠ† (β—‘(𝐾 β†Ύ (𝑀𝐢𝑀)) β€œ {𝑐})) β†’ βˆƒπ‘ ∈ 𝑅 βˆƒπ‘§ ∈ 𝒫 𝑆((πΉβ€˜π‘) ≀ (β™―β€˜π‘§) ∧ (𝑧𝐢𝑀) βŠ† (◑𝐾 β€œ {𝑐}))))
155115, 154mpd 15 . . . 4 ((πœ‘ ∧ ((𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋})) ∧ ((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})))) β†’ βˆƒπ‘ ∈ 𝑅 βˆƒπ‘§ ∈ 𝒫 𝑆((πΉβ€˜π‘) ≀ (β™―β€˜π‘§) ∧ (𝑧𝐢𝑀) βŠ† (◑𝐾 β€œ {𝑐})))
156155expr 457 . . 3 ((πœ‘ ∧ (𝑑 ∈ 𝑅 ∧ 𝑀 ∈ 𝒫 (𝑆 βˆ– {𝑋}))) β†’ (((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})) β†’ βˆƒπ‘ ∈ 𝑅 βˆƒπ‘§ ∈ 𝒫 𝑆((πΉβ€˜π‘) ≀ (β™―β€˜π‘§) ∧ (𝑧𝐢𝑀) βŠ† (◑𝐾 β€œ {𝑐}))))
157156rexlimdvva 3211 . 2 (πœ‘ β†’ (βˆƒπ‘‘ ∈ 𝑅 βˆƒπ‘€ ∈ 𝒫 (𝑆 βˆ– {𝑋})((πΊβ€˜π‘‘) ≀ (β™―β€˜π‘€) ∧ (𝑀𝐢(𝑀 βˆ’ 1)) βŠ† (◑𝐻 β€œ {𝑑})) β†’ βˆƒπ‘ ∈ 𝑅 βˆƒπ‘§ ∈ 𝒫 𝑆((πΉβ€˜π‘) ≀ (β™―β€˜π‘§) ∧ (𝑧𝐢𝑀) βŠ† (◑𝐾 β€œ {𝑐}))))
15877, 157mpd 15 1 (πœ‘ β†’ βˆƒπ‘ ∈ 𝑅 βˆƒπ‘§ ∈ 𝒫 𝑆((πΉβ€˜π‘) ≀ (β™―β€˜π‘§) ∧ (𝑧𝐢𝑀) βŠ† (◑𝐾 β€œ {𝑐})))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ∧ wa 396   = wceq 1541   ∈ wcel 2106  βˆƒwrex 3070  {crab 3432  Vcvv 3474   βˆ– 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 7411   ∈ cmpo 7413  Fincfn 8941  β„‚cc 11110  1c1 11113   + caddc 11115   ≀ cle 11251   βˆ’ cmin 11446  β„•cn 12214  β„•0cn0 12474  β™―chash 14292   Ramsey cram 16934
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  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 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3476  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 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-map 8824  df-en 8942  df-dom 8943  df-sdom 8944  df-fin 8945  df-sup 9439  df-inf 9440  df-dju 9898  df-card 9936  df-pnf 11252  df-mnf 11253  df-xr 11254  df-ltxr 11255  df-le 11256  df-sub 11448  df-neg 11449  df-nn 12215  df-n0 12475  df-z 12561  df-uz 12825  df-fz 13487  df-hash 14293  df-ram 16936
This theorem is referenced by:  ramub1  16963
  Copyright terms: Public domain W3C validator