Metamath Proof Explorer

Theorem ramub1lem2

Description: Lemma for ramub1 . (Contributed by Mario Carneiro, 23-Apr-2015)

Ref Expression
Hypotheses ramub1.m ⊢φ→M∈ℕ
ramub1.r ⊢φ→R∈Fin
ramub1.f ⊢φ→F:R⟶ℕ
ramub1.g ⊢G=x∈R⟼MRamseyy∈R⟼ify=xF⁡x−1F⁡y
ramub1.1 ⊢φ→G:R⟶ℕ0
ramub1.2 ⊢φ→M−1RamseyG∈ℕ0
ramub1.3 ⊢C=a∈V,i∈ℕ0⟼b∈𝒫a|b=i
ramub1.4 ⊢φ→S∈Fin
ramub1.5 ⊢φ→S=M−1RamseyG+1
ramub1.6 ⊢φ→K:SCM⟶R
ramub1.x ⊢φ→X∈S
ramub1.h ⊢H=u∈S∖XCM−1⟼K⁡u∪X
Assertion ramub1lem2 ⊢φ→∃c∈R∃z∈𝒫SF⁡c≤z∧zCM⊆K-1c

Proof

Step Hyp Ref Expression
1 ramub1.m ⊢φ→M∈ℕ
2 ramub1.r ⊢φ→R∈Fin
3 ramub1.f ⊢φ→F:R⟶ℕ
4 ramub1.g ⊢G=x∈R⟼MRamseyy∈R⟼ify=xF⁡x−1F⁡y
5 ramub1.1 ⊢φ→G:R⟶ℕ0
6 ramub1.2 ⊢φ→M−1RamseyG∈ℕ0
7 ramub1.3 ⊢C=a∈V,i∈ℕ0⟼b∈𝒫a|b=i
8 ramub1.4 ⊢φ→S∈Fin
9 ramub1.5 ⊢φ→S=M−1RamseyG+1
10 ramub1.6 ⊢φ→K:SCM⟶R
11 ramub1.x ⊢φ→X∈S
12 ramub1.h ⊢H=u∈S∖XCM−1⟼K⁡u∪X
13 nnm1nn0 ⊢M∈ℕ→M−1∈ℕ0
14 1 13 syl ⊢φ→M−1∈ℕ0
15 diffi ⊢S∈Fin→S∖X∈Fin
16 8 15 syl ⊢φ→S∖X∈Fin
17 6 nn0red ⊢φ→M−1RamseyG∈ℝ
18 17 leidd ⊢φ→M−1RamseyG≤M−1RamseyG
19 hashcl ⊢S∖X∈Fin→S∖X∈ℕ0
20 16 19 syl ⊢φ→S∖X∈ℕ0
21 20 nn0cnd ⊢φ→S∖X∈ℂ
22 6 nn0cnd ⊢φ→M−1RamseyG∈ℂ
23 1cnd ⊢φ→1∈ℂ
24 undif1 ⊢S∖X∪X=S∪X
25 11 snssd ⊢φ→X⊆S
26 ssequn2 ⊢X⊆S↔S∪X=S
27 25 26 sylib ⊢φ→S∪X=S
28 24 27 eqtrid ⊢φ→S∖X∪X=S
29 28 fveq2d ⊢φ→S∖X∪X=S
30 neldifsnd ⊢φ→¬X∈S∖X
31 hashunsng ⊢X∈S→S∖X∈Fin∧¬X∈S∖X→S∖X∪X=S∖X+1
32 11 31 syl ⊢φ→S∖X∈Fin∧¬X∈S∖X→S∖X∪X=S∖X+1
33 16 30 32 mp2and ⊢φ→S∖X∪X=S∖X+1
34 29 33 9 3eqtr3d ⊢φ→S∖X+1=M−1RamseyG+1
35 21 22 23 34 addcan2ad ⊢φ→S∖X=M−1RamseyG
36 18 35 breqtrrd ⊢φ→M−1RamseyG≤S∖X
37 10 adantr ⊢φ∧u∈S∖XCM−1→K:SCM⟶R
38 fveqeq2 ⊢x=u∪X→x=M↔u∪X=M
39 7 hashbcval ⊢S∖X∈Fin∧M−1∈ℕ0→S∖XCM−1=x∈𝒫S∖X|x=M−1
40 16 14 39 syl2anc ⊢φ→S∖XCM−1=x∈𝒫S∖X|x=M−1
41 40 eleq2d ⊢φ→u∈S∖XCM−1↔u∈x∈𝒫S∖X|x=M−1
42 fveqeq2 ⊢x=u→x=M−1↔u=M−1
43 42 elrab ⊢u∈x∈𝒫S∖X|x=M−1↔u∈𝒫S∖X∧u=M−1
44 41 43 bitrdi ⊢φ→u∈S∖XCM−1↔u∈𝒫S∖X∧u=M−1
45 44 simprbda ⊢φ∧u∈S∖XCM−1→u∈𝒫S∖X
46 45 elpwid ⊢φ∧u∈S∖XCM−1→u⊆S∖X
47 46 difss2d ⊢φ∧u∈S∖XCM−1→u⊆S
48 25 adantr ⊢φ∧u∈S∖XCM−1→X⊆S
49 47 48 unssd ⊢φ∧u∈S∖XCM−1→u∪X⊆S
50 vex ⊢u∈V
51 snex ⊢X∈V
52 50 51 unex ⊢u∪X∈V
53 52 elpw ⊢u∪X∈𝒫S↔u∪X⊆S
54 49 53 sylibr ⊢φ∧u∈S∖XCM−1→u∪X∈𝒫S
55 16 adantr ⊢φ∧u∈S∖XCM−1→S∖X∈Fin
56 55 46 ssfid ⊢φ∧u∈S∖XCM−1→u∈Fin
57 neldifsnd ⊢φ∧u∈S∖XCM−1→¬X∈S∖X
58 46 57 ssneldd ⊢φ∧u∈S∖XCM−1→¬X∈u
59 11 adantr ⊢φ∧u∈S∖XCM−1→X∈S
60 hashunsng ⊢X∈S→u∈Fin∧¬X∈u→u∪X=u+1
61 59 60 syl ⊢φ∧u∈S∖XCM−1→u∈Fin∧¬X∈u→u∪X=u+1
62 56 58 61 mp2and ⊢φ∧u∈S∖XCM−1→u∪X=u+1
63 44 simplbda ⊢φ∧u∈S∖XCM−1→u=M−1
64 63 oveq1d ⊢φ∧u∈S∖XCM−1→u+1=M-1+1
65 1 nncnd ⊢φ→M∈ℂ
66 ax-1cn ⊢1∈ℂ
67 npcan ⊢M∈ℂ∧1∈ℂ→M-1+1=M
68 65 66 67 sylancl ⊢φ→M-1+1=M
69 68 adantr ⊢φ∧u∈S∖XCM−1→M-1+1=M
70 62 64 69 3eqtrd ⊢φ∧u∈S∖XCM−1→u∪X=M
71 38 54 70 elrabd ⊢φ∧u∈S∖XCM−1→u∪X∈x∈𝒫S|x=M
72 1 nnnn0d ⊢φ→M∈ℕ0
73 7 hashbcval ⊢S∈Fin∧M∈ℕ0→SCM=x∈𝒫S|x=M
74 8 72 73 syl2anc ⊢φ→SCM=x∈𝒫S|x=M
75 74 adantr ⊢φ∧u∈S∖XCM−1→SCM=x∈𝒫S|x=M
76 71 75 eleqtrrd ⊢φ∧u∈S∖XCM−1→u∪X∈SCM
77 37 76 ffvelcdmd ⊢φ∧u∈S∖XCM−1→K⁡u∪X∈R
78 77 12 fmptd ⊢φ→H:S∖XCM−1⟶R
79 7 14 2 5 6 16 36 78 rami ⊢φ→∃d∈R∃w∈𝒫S∖XG⁡d≤w∧wCM−1⊆H-1d
80 72 adantr ⊢φ∧d∈R∧w∈𝒫S∖X∧G⁡d≤w∧wCM−1⊆H-1d→M∈ℕ0
81 2 adantr ⊢φ∧d∈R∧w∈𝒫S∖X∧G⁡d≤w∧wCM−1⊆H-1d→R∈Fin
82 3 adantr ⊢φ∧d∈R∧w∈𝒫S∖X∧G⁡d≤w∧wCM−1⊆H-1d→F:R⟶ℕ
83 simprll ⊢φ∧d∈R∧w∈𝒫S∖X∧G⁡d≤w∧wCM−1⊆H-1d→d∈R
84 82 83 ffvelcdmd ⊢φ∧d∈R∧w∈𝒫S∖X∧G⁡d≤w∧wCM−1⊆H-1d→F⁡d∈ℕ
85 nnm1nn0 ⊢F⁡d∈ℕ→F⁡d−1∈ℕ0
86 84 85 syl ⊢φ∧d∈R∧w∈𝒫S∖X∧G⁡d≤w∧wCM−1⊆H-1d→F⁡d−1∈ℕ0
87 86 adantr ⊢φ∧d∈R∧w∈𝒫S∖X∧G⁡d≤w∧wCM−1⊆H-1d∧y∈R→F⁡d−1∈ℕ0
88 82 ffvelcdmda ⊢φ∧d∈R∧w∈𝒫S∖X∧G⁡d≤w∧wCM−1⊆H-1d∧y∈R→F⁡y∈ℕ
89 88 nnnn0d ⊢φ∧d∈R∧w∈𝒫S∖X∧G⁡d≤w∧wCM−1⊆H-1d∧y∈R→F⁡y∈ℕ0
90 87 89 ifcld ⊢φ∧d∈R∧w∈𝒫S∖X∧G⁡d≤w∧wCM−1⊆H-1d∧y∈R→ify=dF⁡d−1F⁡y∈ℕ0
91 eqid ⊢y∈R⟼ify=dF⁡d−1F⁡y=y∈R⟼ify=dF⁡d−1F⁡y
92 90 91 fmptd ⊢φ∧d∈R∧w∈𝒫S∖X∧G⁡d≤w∧wCM−1⊆H-1d→y∈R⟼ify=dF⁡d−1F⁡y:R⟶ℕ0
93 equequ2 ⊢x=d→y=x↔y=d
94 fveq2 ⊢x=d→F⁡x=F⁡d
95 94 oveq1d ⊢x=d→F⁡x−1=F⁡d−1
96 93 95 ifbieq1d ⊢x=d→ify=xF⁡x−1F⁡y=ify=dF⁡d−1F⁡y
97 96 mpteq2dv ⊢x=d→y∈R⟼ify=xF⁡x−1F⁡y=y∈R⟼ify=dF⁡d−1F⁡y
98 97 oveq2d ⊢x=d→MRamseyy∈R⟼ify=xF⁡x−1F⁡y=MRamseyy∈R⟼ify=dF⁡d−1F⁡y
99 ovex ⊢MRamseyy∈R⟼ify=dF⁡d−1F⁡y∈V
100 98 4 99 fvmpt ⊢d∈R→G⁡d=MRamseyy∈R⟼ify=dF⁡d−1F⁡y
101 83 100 syl ⊢φ∧d∈R∧w∈𝒫S∖X∧G⁡d≤w∧wCM−1⊆H-1d→G⁡d=MRamseyy∈R⟼ify=dF⁡d−1F⁡y
102 5 adantr ⊢φ∧d∈R∧w∈𝒫S∖X∧G⁡d≤w∧wCM−1⊆H-1d→G:R⟶ℕ0
103 102 83 ffvelcdmd ⊢φ∧d∈R∧w∈𝒫S∖X∧G⁡d≤w∧wCM−1⊆H-1d→G⁡d∈ℕ0
104 101 103 eqeltrrd ⊢φ∧d∈R∧w∈𝒫S∖X∧G⁡d≤w∧wCM−1⊆H-1d→MRamseyy∈R⟼ify=dF⁡d−1F⁡y∈ℕ0
105 simprlr ⊢φ∧d∈R∧w∈𝒫S∖X∧G⁡d≤w∧wCM−1⊆H-1d→w∈𝒫S∖X
106 simprrl ⊢φ∧d∈R∧w∈𝒫S∖X∧G⁡d≤w∧wCM−1⊆H-1d→G⁡d≤w
107 101 106 eqbrtrrd ⊢φ∧d∈R∧w∈𝒫S∖X∧G⁡d≤w∧wCM−1⊆H-1d→MRamseyy∈R⟼ify=dF⁡d−1F⁡y≤w
108 10 adantr ⊢φ∧d∈R∧w∈𝒫S∖X∧G⁡d≤w∧wCM−1⊆H-1d→K:SCM⟶R
109 8 adantr ⊢φ∧d∈R∧w∈𝒫S∖X∧G⁡d≤w∧wCM−1⊆H-1d→S∈Fin
110 105 elpwid ⊢φ∧d∈R∧w∈𝒫S∖X∧G⁡d≤w∧wCM−1⊆H-1d→w⊆S∖X
111 110 difss2d ⊢φ∧d∈R∧w∈𝒫S∖X∧G⁡d≤w∧wCM−1⊆H-1d→w⊆S
112 7 hashbcss ⊢S∈Fin∧w⊆S∧M∈ℕ0→wCM⊆SCM
113 109 111 80 112 syl3anc ⊢φ∧d∈R∧w∈𝒫S∖X∧G⁡d≤w∧wCM−1⊆H-1d→wCM⊆SCM
114 108 113 fssresd ⊢φ∧d∈R∧w∈𝒫S∖X∧G⁡d≤w∧wCM−1⊆H-1d→K↾wCM:wCM⟶R
115 7 80 81 92 104 105 107 114 rami ⊢φ∧d∈R∧w∈𝒫S∖X∧G⁡d≤w∧wCM−1⊆H-1d→∃c∈R∃v∈𝒫wy∈R⟼ify=dF⁡d−1F⁡y⁡c≤v∧vCM⊆K↾wCM-1c
116 equequ1 ⊢y=c→y=d↔c=d
117 fveq2 ⊢y=c→F⁡y=F⁡c
118 116 117 ifbieq2d ⊢y=c→ify=dF⁡d−1F⁡y=ifc=dF⁡d−1F⁡c
119 ovex ⊢F⁡d−1∈V
120 fvex ⊢F⁡c∈V
121 119 120 ifex ⊢ifc=dF⁡d−1F⁡c∈V
122 118 91 121 fvmpt ⊢c∈R→y∈R⟼ify=dF⁡d−1F⁡y⁡c=ifc=dF⁡d−1F⁡c
123 122 ad2antrl ⊢φ∧d∈R∧w∈𝒫S∖X∧G⁡d≤w∧wCM−1⊆H-1d∧c∈R∧v∈𝒫w→y∈R⟼ify=dF⁡d−1F⁡y⁡c=ifc=dF⁡d−1F⁡c
124 123 breq1d ⊢φ∧d∈R∧w∈𝒫S∖X∧G⁡d≤w∧wCM−1⊆H-1d∧c∈R∧v∈𝒫w→y∈R⟼ify=dF⁡d−1F⁡y⁡c≤v↔ifc=dF⁡d−1F⁡c≤v
125 124 anbi1d ⊢φ∧d∈R∧w∈𝒫S∖X∧G⁡d≤w∧wCM−1⊆H-1d∧c∈R∧v∈𝒫w→y∈R⟼ify=dF⁡d−1F⁡y⁡c≤v∧vCM⊆K↾wCM-1c↔ifc=dF⁡d−1F⁡c≤v∧vCM⊆K↾wCM-1c
126 1 ad2antrr ⊢φ∧d∈R∧w∈𝒫S∖X∧G⁡d≤w∧wCM−1⊆H-1d∧c∈R∧v∈𝒫w∧ifc=dF⁡d−1F⁡c≤v∧vCM⊆K↾wCM-1c→M∈ℕ
127 2 ad2antrr ⊢φ∧d∈R∧w∈𝒫S∖X∧G⁡d≤w∧wCM−1⊆H-1d∧c∈R∧v∈𝒫w∧ifc=dF⁡d−1F⁡c≤v∧vCM⊆K↾wCM-1c→R∈Fin
128 3 ad2antrr ⊢φ∧d∈R∧w∈𝒫S∖X∧G⁡d≤w∧wCM−1⊆H-1d∧c∈R∧v∈𝒫w∧ifc=dF⁡d−1F⁡c≤v∧vCM⊆K↾wCM-1c→F:R⟶ℕ
129 5 ad2antrr ⊢φ∧d∈R∧w∈𝒫S∖X∧G⁡d≤w∧wCM−1⊆H-1d∧c∈R∧v∈𝒫w∧ifc=dF⁡d−1F⁡c≤v∧vCM⊆K↾wCM-1c→G:R⟶ℕ0
130 6 ad2antrr ⊢φ∧d∈R∧w∈𝒫S∖X∧G⁡d≤w∧wCM−1⊆H-1d∧c∈R∧v∈𝒫w∧ifc=dF⁡d−1F⁡c≤v∧vCM⊆K↾wCM-1c→M−1RamseyG∈ℕ0
131 8 ad2antrr ⊢φ∧d∈R∧w∈𝒫S∖X∧G⁡d≤w∧wCM−1⊆H-1d∧c∈R∧v∈𝒫w∧ifc=dF⁡d−1F⁡c≤v∧vCM⊆K↾wCM-1c→S∈Fin
132 9 ad2antrr ⊢φ∧d∈R∧w∈𝒫S∖X∧G⁡d≤w∧wCM−1⊆H-1d∧c∈R∧v∈𝒫w∧ifc=dF⁡d−1F⁡c≤v∧vCM⊆K↾wCM-1c→S=M−1RamseyG+1
133 10 ad2antrr ⊢φ∧d∈R∧w∈𝒫S∖X∧G⁡d≤w∧wCM−1⊆H-1d∧c∈R∧v∈𝒫w∧ifc=dF⁡d−1F⁡c≤v∧vCM⊆K↾wCM-1c→K:SCM⟶R
134 11 ad2antrr ⊢φ∧d∈R∧w∈𝒫S∖X∧G⁡d≤w∧wCM−1⊆H-1d∧c∈R∧v∈𝒫w∧ifc=dF⁡d−1F⁡c≤v∧vCM⊆K↾wCM-1c→X∈S
135 83 adantr ⊢φ∧d∈R∧w∈𝒫S∖X∧G⁡d≤w∧wCM−1⊆H-1d∧c∈R∧v∈𝒫w∧ifc=dF⁡d−1F⁡c≤v∧vCM⊆K↾wCM-1c→d∈R
136 110 adantr ⊢φ∧d∈R∧w∈𝒫S∖X∧G⁡d≤w∧wCM−1⊆H-1d∧c∈R∧v∈𝒫w∧ifc=dF⁡d−1F⁡c≤v∧vCM⊆K↾wCM-1c→w⊆S∖X
137 106 adantr ⊢φ∧d∈R∧w∈𝒫S∖X∧G⁡d≤w∧wCM−1⊆H-1d∧c∈R∧v∈𝒫w∧ifc=dF⁡d−1F⁡c≤v∧vCM⊆K↾wCM-1c→G⁡d≤w
138 simprrr ⊢φ∧d∈R∧w∈𝒫S∖X∧G⁡d≤w∧wCM−1⊆H-1d→wCM−1⊆H-1d
139 138 adantr ⊢φ∧d∈R∧w∈𝒫S∖X∧G⁡d≤w∧wCM−1⊆H-1d∧c∈R∧v∈𝒫w∧ifc=dF⁡d−1F⁡c≤v∧vCM⊆K↾wCM-1c→wCM−1⊆H-1d
140 simprll ⊢φ∧d∈R∧w∈𝒫S∖X∧G⁡d≤w∧wCM−1⊆H-1d∧c∈R∧v∈𝒫w∧ifc=dF⁡d−1F⁡c≤v∧vCM⊆K↾wCM-1c→c∈R
141 simprlr ⊢φ∧d∈R∧w∈𝒫S∖X∧G⁡d≤w∧wCM−1⊆H-1d∧c∈R∧v∈𝒫w∧ifc=dF⁡d−1F⁡c≤v∧vCM⊆K↾wCM-1c→v∈𝒫w
142 141 elpwid ⊢φ∧d∈R∧w∈𝒫S∖X∧G⁡d≤w∧wCM−1⊆H-1d∧c∈R∧v∈𝒫w∧ifc=dF⁡d−1F⁡c≤v∧vCM⊆K↾wCM-1c→v⊆w
143 simprrl ⊢φ∧d∈R∧w∈𝒫S∖X∧G⁡d≤w∧wCM−1⊆H-1d∧c∈R∧v∈𝒫w∧ifc=dF⁡d−1F⁡c≤v∧vCM⊆K↾wCM-1c→ifc=dF⁡d−1F⁡c≤v
144 simprrr ⊢φ∧d∈R∧w∈𝒫S∖X∧G⁡d≤w∧wCM−1⊆H-1d∧c∈R∧v∈𝒫w∧ifc=dF⁡d−1F⁡c≤v∧vCM⊆K↾wCM-1c→vCM⊆K↾wCM-1c
145 cnvresima ⊢K↾wCM-1c=K-1c∩wCM
146 inss1 ⊢K-1c∩wCM⊆K-1c
147 145 146 eqsstri ⊢K↾wCM-1c⊆K-1c
148 144 147 sstrdi ⊢φ∧d∈R∧w∈𝒫S∖X∧G⁡d≤w∧wCM−1⊆H-1d∧c∈R∧v∈𝒫w∧ifc=dF⁡d−1F⁡c≤v∧vCM⊆K↾wCM-1c→vCM⊆K-1c
149 126 127 128 4 129 130 7 131 132 133 134 12 135 136 137 139 140 142 143 148 ramub1lem1 ⊢φ∧d∈R∧w∈𝒫S∖X∧G⁡d≤w∧wCM−1⊆H-1d∧c∈R∧v∈𝒫w∧ifc=dF⁡d−1F⁡c≤v∧vCM⊆K↾wCM-1c→∃z∈𝒫SF⁡c≤z∧zCM⊆K-1c
150 149 expr ⊢φ∧d∈R∧w∈𝒫S∖X∧G⁡d≤w∧wCM−1⊆H-1d∧c∈R∧v∈𝒫w→ifc=dF⁡d−1F⁡c≤v∧vCM⊆K↾wCM-1c→∃z∈𝒫SF⁡c≤z∧zCM⊆K-1c
151 125 150 sylbid ⊢φ∧d∈R∧w∈𝒫S∖X∧G⁡d≤w∧wCM−1⊆H-1d∧c∈R∧v∈𝒫w→y∈R⟼ify=dF⁡d−1F⁡y⁡c≤v∧vCM⊆K↾wCM-1c→∃z∈𝒫SF⁡c≤z∧zCM⊆K-1c
152 151 anassrs ⊢φ∧d∈R∧w∈𝒫S∖X∧G⁡d≤w∧wCM−1⊆H-1d∧c∈R∧v∈𝒫w→y∈R⟼ify=dF⁡d−1F⁡y⁡c≤v∧vCM⊆K↾wCM-1c→∃z∈𝒫SF⁡c≤z∧zCM⊆K-1c
153 152 rexlimdva ⊢φ∧d∈R∧w∈𝒫S∖X∧G⁡d≤w∧wCM−1⊆H-1d∧c∈R→∃v∈𝒫wy∈R⟼ify=dF⁡d−1F⁡y⁡c≤v∧vCM⊆K↾wCM-1c→∃z∈𝒫SF⁡c≤z∧zCM⊆K-1c
154 153 reximdva ⊢φ∧d∈R∧w∈𝒫S∖X∧G⁡d≤w∧wCM−1⊆H-1d→∃c∈R∃v∈𝒫wy∈R⟼ify=dF⁡d−1F⁡y⁡c≤v∧vCM⊆K↾wCM-1c→∃c∈R∃z∈𝒫SF⁡c≤z∧zCM⊆K-1c
155 115 154 mpd ⊢φ∧d∈R∧w∈𝒫S∖X∧G⁡d≤w∧wCM−1⊆H-1d→∃c∈R∃z∈𝒫SF⁡c≤z∧zCM⊆K-1c
156 155 expr ⊢φ∧d∈R∧w∈𝒫S∖X→G⁡d≤w∧wCM−1⊆H-1d→∃c∈R∃z∈𝒫SF⁡c≤z∧zCM⊆K-1c
157 156 rexlimdvva ⊢φ→∃d∈R∃w∈𝒫S∖XG⁡d≤w∧wCM−1⊆H-1d→∃c∈R∃z∈𝒫SF⁡c≤z∧zCM⊆K-1c
158 79 157 mpd ⊢φ→∃c∈R∃z∈𝒫SF⁡c≤z∧zCM⊆K-1c