Metamath Proof Explorer


Theorem ramub1lem1

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

Ref Expression
Hypotheses ramub1.m φM
ramub1.r φRFin
ramub1.f φF:R
ramub1.g G=xRMRamseyyRify=xFx1Fy
ramub1.1 φG:R0
ramub1.2 φM1RamseyG0
ramub1.3 C=aV,i0b𝒫a|b=i
ramub1.4 φSFin
ramub1.5 φS=M1RamseyG+1
ramub1.6 φK:SCMR
ramub1.x φXS
ramub1.h H=uSXCM1KuX
ramub1.d φDR
ramub1.w φWSX
ramub1.7 φGDW
ramub1.8 φWCM1H-1D
ramub1.e φER
ramub1.v φVW
ramub1.9 φifE=DFD1FEV
ramub1.s φVCMK-1E
Assertion ramub1lem1 φz𝒫SFEzzCMK-1E

Proof

Step Hyp Ref Expression
1 ramub1.m φM
2 ramub1.r φRFin
3 ramub1.f φF:R
4 ramub1.g G=xRMRamseyyRify=xFx1Fy
5 ramub1.1 φG:R0
6 ramub1.2 φM1RamseyG0
7 ramub1.3 C=aV,i0b𝒫a|b=i
8 ramub1.4 φSFin
9 ramub1.5 φS=M1RamseyG+1
10 ramub1.6 φK:SCMR
11 ramub1.x φXS
12 ramub1.h H=uSXCM1KuX
13 ramub1.d φDR
14 ramub1.w φWSX
15 ramub1.7 φGDW
16 ramub1.8 φWCM1H-1D
17 ramub1.e φER
18 ramub1.v φVW
19 ramub1.9 φifE=DFD1FEV
20 ramub1.s φVCMK-1E
21 18 14 sstrd φVSX
22 21 difss2d φVS
23 11 snssd φXS
24 22 23 unssd φVXS
25 8 24 sselpwd φVX𝒫S
26 25 adantr φE=DVX𝒫S
27 iftrue E=DifE=DFD1FE=FD1
28 27 adantl φE=DifE=DFD1FE=FD1
29 19 adantr φE=DifE=DFD1FEV
30 28 29 eqbrtrrd φE=DFD1V
31 3 13 ffvelrnd φFD
32 31 adantr φE=DFD
33 32 nnred φE=DFD
34 1red φE=D1
35 8 22 ssfid φVFin
36 hashcl VFinV0
37 nn0re V0V
38 35 36 37 3syl φV
39 38 adantr φE=DV
40 33 34 39 lesubaddd φE=DFD1VFDV+1
41 30 40 mpbid φE=DFDV+1
42 fveq2 E=DFE=FD
43 snidg XSXX
44 11 43 syl φXX
45 21 sseld φXVXSX
46 eldifn XSX¬XX
47 45 46 syl6 φXV¬XX
48 44 47 mt2d φ¬XV
49 hashunsng XSVFin¬XVVX=V+1
50 11 49 syl φVFin¬XVVX=V+1
51 35 48 50 mp2and φVX=V+1
52 42 51 breqan12rd φE=DFEVXFDV+1
53 41 52 mpbird φE=DFEVX
54 snfi XFin
55 unfi VFinXFinVXFin
56 35 54 55 sylancl φVXFin
57 1 nnnn0d φM0
58 7 hashbcval VXFinM0VXCM=x𝒫VX|x=M
59 56 57 58 syl2anc φVXCM=x𝒫VX|x=M
60 59 adantr φE=DVXCM=x𝒫VX|x=M
61 simpl1l φE=Dx𝒫VXx=Mx𝒫Vφ
62 7 hashbcval VFinM0VCM=x𝒫V|x=M
63 35 57 62 syl2anc φVCM=x𝒫V|x=M
64 63 20 eqsstrrd φx𝒫V|x=MK-1E
65 61 64 syl φE=Dx𝒫VXx=Mx𝒫Vx𝒫V|x=MK-1E
66 simpr φE=Dx𝒫VXx=Mx𝒫Vx𝒫V
67 simpl3 φE=Dx𝒫VXx=Mx𝒫Vx=M
68 rabid xx𝒫V|x=Mx𝒫Vx=M
69 66 67 68 sylanbrc φE=Dx𝒫VXx=Mx𝒫Vxx𝒫V|x=M
70 65 69 sseldd φE=Dx𝒫VXx=Mx𝒫VxK-1E
71 simpl2 φE=Dx𝒫VXx=M¬x𝒫Vx𝒫VX
72 71 elpwid φE=Dx𝒫VXx=M¬x𝒫VxVX
73 simpl1l φE=Dx𝒫VXx=M¬x𝒫Vφ
74 73 24 syl φE=Dx𝒫VXx=M¬x𝒫VVXS
75 72 74 sstrd φE=Dx𝒫VXx=M¬x𝒫VxS
76 vex xV
77 76 elpw x𝒫SxS
78 75 77 sylibr φE=Dx𝒫VXx=M¬x𝒫Vx𝒫S
79 simpl3 φE=Dx𝒫VXx=M¬x𝒫Vx=M
80 rabid xx𝒫S|x=Mx𝒫Sx=M
81 78 79 80 sylanbrc φE=Dx𝒫VXx=M¬x𝒫Vxx𝒫S|x=M
82 7 hashbcval SFinM0SCM=x𝒫S|x=M
83 8 57 82 syl2anc φSCM=x𝒫S|x=M
84 73 83 syl φE=Dx𝒫VXx=M¬x𝒫VSCM=x𝒫S|x=M
85 81 84 eleqtrrd φE=Dx𝒫VXx=M¬x𝒫VxSCM
86 14 difss2d φWS
87 8 86 ssfid φWFin
88 nnm1nn0 MM10
89 1 88 syl φM10
90 7 hashbcval WFinM10WCM1=u𝒫W|u=M1
91 87 89 90 syl2anc φWCM1=u𝒫W|u=M1
92 91 16 eqsstrrd φu𝒫W|u=M1H-1D
93 73 92 syl φE=Dx𝒫VXx=M¬x𝒫Vu𝒫W|u=M1H-1D
94 fveqeq2 u=xXu=M1xX=M1
95 uncom VX=XV
96 72 95 sseqtrdi φE=Dx𝒫VXx=M¬x𝒫VxXV
97 ssundif xXVxXV
98 96 97 sylib φE=Dx𝒫VXx=M¬x𝒫VxXV
99 73 18 syl φE=Dx𝒫VXx=M¬x𝒫VVW
100 98 99 sstrd φE=Dx𝒫VXx=M¬x𝒫VxXW
101 76 difexi xXV
102 101 elpw xX𝒫WxXW
103 100 102 sylibr φE=Dx𝒫VXx=M¬x𝒫VxX𝒫W
104 73 8 syl φE=Dx𝒫VXx=M¬x𝒫VSFin
105 104 75 ssfid φE=Dx𝒫VXx=M¬x𝒫VxFin
106 diffi xFinxXFin
107 105 106 syl φE=Dx𝒫VXx=M¬x𝒫VxXFin
108 hashcl xXFinxX0
109 nn0cn xX0xX
110 107 108 109 3syl φE=Dx𝒫VXx=M¬x𝒫VxX
111 ax-1cn 1
112 pncan xX1xX+1-1=xX
113 110 111 112 sylancl φE=Dx𝒫VXx=M¬x𝒫VxX+1-1=xX
114 neldifsnd φE=Dx𝒫VXx=M¬x𝒫V¬XxX
115 hashunsng XSxXFin¬XxXxXX=xX+1
116 73 11 115 3syl φE=Dx𝒫VXx=M¬x𝒫VxXFin¬XxXxXX=xX+1
117 107 114 116 mp2and φE=Dx𝒫VXx=M¬x𝒫VxXX=xX+1
118 undif1 xXX=xX
119 simpr φE=Dx𝒫VXx=M¬x𝒫V¬x𝒫V
120 71 119 eldifd φE=Dx𝒫VXx=M¬x𝒫Vx𝒫VX𝒫V
121 elpwunsn x𝒫VX𝒫VXx
122 120 121 syl φE=Dx𝒫VXx=M¬x𝒫VXx
123 122 snssd φE=Dx𝒫VXx=M¬x𝒫VXx
124 ssequn2 XxxX=x
125 123 124 sylib φE=Dx𝒫VXx=M¬x𝒫VxX=x
126 118 125 eqtr2id φE=Dx𝒫VXx=M¬x𝒫Vx=xXX
127 126 fveq2d φE=Dx𝒫VXx=M¬x𝒫Vx=xXX
128 127 79 eqtr3d φE=Dx𝒫VXx=M¬x𝒫VxXX=M
129 117 128 eqtr3d φE=Dx𝒫VXx=M¬x𝒫VxX+1=M
130 129 oveq1d φE=Dx𝒫VXx=M¬x𝒫VxX+1-1=M1
131 113 130 eqtr3d φE=Dx𝒫VXx=M¬x𝒫VxX=M1
132 94 103 131 elrabd φE=Dx𝒫VXx=M¬x𝒫VxXu𝒫W|u=M1
133 93 132 sseldd φE=Dx𝒫VXx=M¬x𝒫VxXH-1D
134 12 mptiniseg DRH-1D=uSXCM1|KuX=D
135 73 13 134 3syl φE=Dx𝒫VXx=M¬x𝒫VH-1D=uSXCM1|KuX=D
136 133 135 eleqtrd φE=Dx𝒫VXx=M¬x𝒫VxXuSXCM1|KuX=D
137 uneq1 u=xXuX=xXX
138 137 fveqeq2d u=xXKuX=DKxXX=D
139 138 elrab xXuSXCM1|KuX=DxXSXCM1KxXX=D
140 139 simprbi xXuSXCM1|KuX=DKxXX=D
141 136 140 syl φE=Dx𝒫VXx=M¬x𝒫VKxXX=D
142 126 fveq2d φE=Dx𝒫VXx=M¬x𝒫VKx=KxXX
143 simpl1r φE=Dx𝒫VXx=M¬x𝒫VE=D
144 141 142 143 3eqtr4d φE=Dx𝒫VXx=M¬x𝒫VKx=E
145 10 ffnd φKFnSCM
146 fniniseg KFnSCMxK-1ExSCMKx=E
147 73 145 146 3syl φE=Dx𝒫VXx=M¬x𝒫VxK-1ExSCMKx=E
148 85 144 147 mpbir2and φE=Dx𝒫VXx=M¬x𝒫VxK-1E
149 70 148 pm2.61dan φE=Dx𝒫VXx=MxK-1E
150 149 rabssdv φE=Dx𝒫VX|x=MK-1E
151 60 150 eqsstrd φE=DVXCMK-1E
152 fveq2 z=VXz=VX
153 152 breq2d z=VXFEzFEVX
154 oveq1 z=VXzCM=VXCM
155 154 sseq1d z=VXzCMK-1EVXCMK-1E
156 153 155 anbi12d z=VXFEzzCMK-1EFEVXVXCMK-1E
157 156 rspcev VX𝒫SFEVXVXCMK-1Ez𝒫SFEzzCMK-1E
158 26 53 151 157 syl12anc φE=Dz𝒫SFEzzCMK-1E
159 8 22 sselpwd φV𝒫S
160 159 adantr φEDV𝒫S
161 ifnefalse EDifE=DFD1FE=FE
162 161 adantl φEDifE=DFD1FE=FE
163 19 adantr φEDifE=DFD1FEV
164 162 163 eqbrtrrd φEDFEV
165 20 adantr φEDVCMK-1E
166 fveq2 z=Vz=V
167 166 breq2d z=VFEzFEV
168 oveq1 z=VzCM=VCM
169 168 sseq1d z=VzCMK-1EVCMK-1E
170 167 169 anbi12d z=VFEzzCMK-1EFEVVCMK-1E
171 170 rspcev V𝒫SFEVVCMK-1Ez𝒫SFEzzCMK-1E
172 160 164 165 171 syl12anc φEDz𝒫SFEzzCMK-1E
173 158 172 pm2.61dane φz𝒫SFEzzCMK-1E